Boolean Values

The SAT solver allows denoting Boolean value expressions. These expressions can contain native Prolog variables. Boolean expressions constraints are posted to the SAT solver via the predicate sat/1. Internally the SAT constraint is normalized into a BDD tree. The resulting BDD tree is automatically shown by the top-level:

Example:
?- sat(X#Y).
sat((X->(Y->0;1);Y->1;0))

BDD tree reductions and attribute variable hooks guard the interaction between SAT constraints. Interval arithmetic is used in reducing pseudo Boolean constraints. Currently the following inference rules have been implemented for Boolean expressions constraints and pseudo Boolean constraints:

Unit propagation and alias propagation provide forward checking since they might lead to failure of subsequent constraints. Where permitted Boolean expression constraints are replaced by native Prolog unification =/2, thus leading to further forward checking. It is also allowed mix-ing native Prolog unification =/2 with constraints:

Examples:
?- X=Y, sat(X+Y).
X = 1,
Y = 1
?- sat(X+Y), X=Y.
X = 1,
Y = 1

The following Boolean value expressions are provided:

V (SAT):
A native Prolog variable V represents a Boolean variable.
0 (SAT):
1 (SAT):
The constant 0 or 1 represents a Boolean constant.
~ A (SAT):
If A is an expression then the negation ~A is also an expression.
A + B (SAT):
If A and B are expressions then the disjunction A+B is also an expression.
A * B (SAT):
If A and B are expressions then the conjunction A*B is also an expression.
A =< B (SAT):
If A and B are expressions then the implication A=<B is also an expression.
A >= B (SAT):
If A and B are expressions then the implication B=<A is also an expression.
A > B (SAT):
If A and B are expressions then the difference A>B is also an expression.
A < B (SAT):
If A and B are expressions then the difference B>A is also an expression.
A =:= B (SAT):
If A and B are expressions then the equality A=:=B is also an expression.
A # B (SAT):
If A and B are expressions then the xor A#B is also an expression.
A -> B; C (SAT):
If A, B and C are expressions then the if-then-else A->B;C is also an expression.
V^A (SAT):
If V is a native Prolog variable and A is an expression then the Boolean existential quantification V^A is also an expression.
card(P, L):
If P is a integer/integer-integer list and L is an expression list then the cardinality constraint card(P, L) is also an expression.

Kommentare