A Boolean expression is one of:
0 | false |
1 | true |
| variable | unknown truth value |
| atom | universally quantified variable |
~ Expr | logical NOT |
| Expr + Expr | logical OR |
| Expr * Expr | logical AND |
| Expr # Expr | exclusive OR |
Var ^ Expr | existential
quantification |
Expr =:= Expr | equality |
Expr =\= Expr | disequality
(same as #) |
Expr =< Expr | less or
equal (implication) |
Expr >= Expr | greater or
equal |
| Expr < Expr | less than |
| Expr > Expr | greater than |
card(Is,Exprs) | cardinality constraint (see
below) |
+(Exprs) | n-fold disjunction (see below) |
*(Exprs) | n-fold conjunction (see below) |
where Expr again denotes a Boolean expression.
The Boolean expression card(Is,Exprs) is true iff the
number of true expressions in the list Exprs is a member of
the list Is of integers and integer ranges of the form From-To.
For example, to state that precisely two of the three variables X, Y
and Z are
true, you can use sat(card([2],[X,Y,Z])).
+(Exprs) and *(Exprs) denote, respectively,
the disjunction and conjunction of all elements in the list Exprs
of Boolean expressions.
Atoms denote parametric values that are universally quantified. All
universal quantifiers appear implicitly in front of the entire
expression. In residual goals, universally quantified variables always
appear on the right-hand side of equations. Therefore, they can be used
to express functional dependencies on input variables.
