As a convenience the SAT solver provides a single solving
technique in two incarnations. We provide the following solving
technique when there is an attempt to label multiple variables at
once or to count the number of solutions:
Although variable rankings are found in the literature, we didn’t implement some special search strategy, since we did not yet find a solution to overcome the ranking overhead. The given variables are tried in the given input order. Counting further depends on labelling, since it is no yet able to use counts derived from a single BDD tree.Examples:
?- sat(X=<Y), sat(Y=<Z), sat(Z=<X), labeling([X,Y,Z]).
X = 0,
Y = 0,
Z = 0 ;
X = 1,
Y = 1,
Z = 1
?- sat(X=<Y), sat(Y=<Z), sat(Z=<X), sat_count([X,Y,Z], N).
N = 2,
The Boolean constraint can be used to define more complex conditions. A recurring problem is stating the cardinality of a couple of Boolean expressions. The predicate card/2 has been defined as a corresponding convenience.
The following satisfaction predicates are provided: