byLevel -
Variable in class org.sat4j.minisat.constraints.pb.ConflictMap
allows to access directly to all variables belonging to a particular
level At index 0, unassigned literals are stored (usually level -1); so
there is always a step between index and levels.
This class is a CSP to SAT translator that is able to read a CSP problem
using the First CSP solver competition input format and that translates it
into clausal and cardinality (equality) constraints.
Converter from the Extended Dimacs format proposed by Fahiem Bacchus and Toby
Walsh in array representation (without the terminating 0) to the Dimacs
format.
Luby series code taken from SATZ_rand 5.0 from Henry Kautz
http://www.cs.rochester.edu/u/kautz/satz-rand/satz-rand-v5.0.tgz
Luby's series
long luby_super(int i)
{
long power;
int k;
if (i<=0){
fprintf(stderr, "bad argument super(%d)\n", i);
exit(1);
}
/* let 2ˆk be the least power of 2 >= (i+1)
k = 1;
power = 2;
while (power < (i+1)){
k += 1;
power *= 2;
}
if (power == (i+1)) return (power/2);
return (luby_super(i - (power/2) + 1));
}
Perform some sanity check before constructing a clause a) if a literal is
assigned true, return null (the clause is satisfied) b) if a literal is
assigned false, remove it c) if a clause contains a literal and its
opposite (tautology) return null d) remove duplicate literals e) if the
clause is empty, return null f) if the clause if unit, transmit it to the
object responsible for unit propagation