Boolean Satisfaction

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,
sat((X->1;Z->0;1)),
sat((X->(Y->1;0);1)),
sat((Y->(Z->1;0);1))

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:

labeling(L):
The predicate labels the variables in L.
random_labeling(L):
The predicate randomly labels the variables in L.
sat_count(L, N):
The predicate silently labels the variables in L and succeeds in N with the count of the solutions.
card(N, L):
If N is an integer and L is a variable list then the constraint that the number of true var-iables amounts exactly to N is posted.

Comments