Boolean Satisfaction

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:

sat(A):
If A is an expression then its satisfiability is posted.
labeling(L):
The predicate labels the variables in L.
random_labeling(L):
The predicate randomly labels the variables in L.
count(L, N):
The predicate silently labels the variables in L and succeeds in N with the count of the solutions.
pseudo(W, L, C, K):
The predicate succeeds in a new pseudo Boolean constraint with weights R, variables L, comparator C and value K.
weighted_maximum(W, L, O):
The predicate succeeds in O with the maximum of the weighted sum from the values L and the weights W, and then succeeds for all corresponding labelings of L.

Kommentare