A.8.2 Boolean expressions

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.