# 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
- Alias Propagation

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