The SAT solver provides a couple solving technique in various
incarnations. We provide intelligent backtracking search when
there is an attempt to label multiple variables at once via the
predicate labeling/1 or to count the number of solutions via the
predicate count/2. The optimization predicate weighted_maximum/3
uses branch and bound search.:
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), count([X,Y,Z], N).
N = 2,
sat((X->1;Z->0;1)),
sat((X->(Y->1;0);1)),
sat((Y->(Z->1;0);1))
The backtracking is intelligent in as far as the Prolog interpreter eliminates choice points. The labelling variant random_labeling/1 uses a random order among each variable. The maximization predicate uses random labeling in its initial value and in its search. Since the weights can be negative, the predicate is also suitable to solve minimization problems.
The following satisfaction predicates are provided: