Boolean and reified constraints

9.7 Boolean and reified constraints

Boolean FD expressions
fd_reified_in/4
(#\)/1 - constraint NOT, (#<=>)/2 - constraint equivalent,
(#\<=>)/2 - constraint different, (##)/2 - constraint XOR,
(#==>)/2 - constraint imply, (#\==>)/2 - constraint not imply,
(#/\)/2 - constraint AND, (#\/\)/2 - constraint NAND,
(#\/)/2 - constraint OR, (#\\/)/2 - constraint NOR
fd_cardinality/2, fd_cardinality/3, fd_at_least_one/1, fd_at_most_one/1,
fd_only_one/1

9.7.1 Boolean FD expressions

An boolean FD expression is a Prolog term built from integers (0 for false, 1 for true), variables (Prolog or FD variables), partial AC arithmetic constraints (section 9.6.2), full AC arithmetic constraints (section 9.6.3) and functors (or operators) that represent boolean functions. When a sub-expression of a boolean expression is an arithmetic constraint c, it is reified. Namely, as soon as the solver detects that c is true (i.e. entailed) the sub-expression has the value 1. Similarly when the solver detects that c is false (i.e. disentailed) the sub-expression evaluates as 0. While neither the entailment nor the disentailment can be detected the sub-expression is evaluated as a domain 0..1. The following table details the components of an FD boolean expression:

FD Expression Result

Prolog variable domain 0..1

FD variable X domain of X, X is constrained to be in 0..1

0 (integer) 0 (false)

1 (integer) 1 (true)

#\ E not E

E1 #<=> E2 E1 equivalent to E2

E1 #\<=> E2 E1 not equivalent to E2 (i.e. E1 different from E2)

E1 ## E2 E1 exclusive OR E2 (i.e. E1 not equivalent to E2)

E1 #==> E2 E1 implies E2

E1 #\==> E2 E1 does not imply E2

E1 #/\ E2 E1 AND E2

E1 #\/\ E2 E1 NAND E2

E1 #\/ E2 E1 OR E2

E1 #\\/ E2 E1 NOR E2

#<=>, #\<=>, ##, #==>, #\==>, #/\, #\/\, #\/ and #\\/ are predefined infix operators. #\ is a predefined prefix operator (section 8.14.10).

Errors

a sub-expression E is neither a variable nor an integer (0 or 1) nor an FD boolean functor nor reified constraint type_error(fd_bool_evaluable, E)

an expression is too complex resource_error(too_big_fd_constraint)

a sub-expression is an invalid reified constraint an arithmetic constraint error (section 9.6.1)

9.7.2 fd_reified_in/4

Templates

fd_reified_in(?fd_variable, +integer, +integer, ?fd_variable)

Description

fd_reified_in(X, Lower, Upper, B) captures the truth value of the constraint X ∈ [Lower..Upper] in the boolean variable B.

Errors

X is neither a variable nor an FD variable nor an integer type_error(fd_variable, X)

B is neither a variable nor an FD variable nor an integer type_error(fd_variable, B)

Lower is a variable instantiation_error

Lower is neither a variable nor an integer type_error(integer, Lower)

Upper is a variable instantiation_error

Upper is neither a variable nor an integer type_error(integer, Upper)

9.7.3 (#\)/1 - constraint NOT, (#<=>)/2 - constraint equivalent,
(#\<=>)/2 - constraint different, (##)/2 - constraint XOR,
(#==>)/2 - constraint imply, (#\==>)/2 - constraint not imply,
(#/\)/2 - constraint AND, (#\/\)/2 - constraint NAND,
(#\/)/2 - constraint OR, (#\\/)/2 - constraint NOR

Templates

#\(?fd_bool_evaluable)
#<=>(?fd_bool_evaluable, ?fd_bool_evaluable)
#\<=>(?fd_bool_evaluable, ?fd_bool_evaluable)
##(?fd_bool_evaluable, ?fd_bool_evaluable)
#==>(?fd_bool_evaluable, ?fd_bool_evaluable)
#\==>(?fd_bool_evaluable, ?fd_bool_evaluable)
#/\(?fd_bool_evaluable, ?fd_bool_evaluable)
#\/\(?fd_bool_evaluable, ?fd_bool_evaluable)
#\/(?fd_bool_evaluable, ?fd_bool_evaluable)
#\\/(?fd_bool_evaluable, ?fd_bool_evaluable)

Description

#\ FdBoolExpr1 constraints FdBoolExpr1 to be false.

FdBoolExpr1 #<=> FdBoolExpr2 constrains FdBoolExpr1 to be equivalent to FdBoolExpr2.

FdBoolExpr1 #\<=> FdBoolExpr2 constrains FdBoolExpr1 to be equivalent to not FdBoolExpr2.

FdBoolExpr1 ## FdBoolExpr2 constrains FdBoolExpr1 XOR FdBoolExpr2 to be true

FdBoolExpr1 #==> FdBoolExpr2 constrains FdBoolExpr1 to imply FdBoolExpr2.

FdBoolExpr1 #\==> FdBoolExpr2 constrains FdBoolExpr1 to not imply FdBoolExpr2.

FdBoolExpr1 #/\ FdBoolExpr2 constrains FdBoolExpr1 AND FdBoolExpr2 to be true.

FdBoolExpr1 #\/\ FdBoolExpr2 constrains FdBoolExpr1 AND FdBoolExpr2 to be false.

FdBoolExpr1 #\/ FdBoolExpr2 constrains FdBoolExpr1 OR FdBoolExpr2 to be true.

FdBoolExpr1 #\\/ FdBoolExpr2 constrains FdBoolExpr1 OR FdBoolExpr2 to be false.

FdBoolExpr1 and FdBoolExpr2 are boolean FD expressions (section 9.7.1).

Note that #\<=> (not equivalent) and ## (exclusive or) are synonymous.

These predicates post boolean constraints that are managed by the FD solver using a partial arc-consistency algorithm to reduce the domain of involved variables. The (dis)entailment of reified constraints is detected using either the bounds (for partial AC arithmetic constraints) or the full domain (for full AC arithmetic constraints).

#<=>, #\<=>, ##, #==>, #\==>, #/\, #\/\, #\/ and #\\/ are predefined infix operators. #\ is a predefined prefix operator (section 8.14.10).

Errors

Refer to the syntax of boolean FD expressions for possible errors (section 9.7.1).

Portability

GNU Prolog predicates.

9.7.4 fd_cardinality/2, fd_cardinality/3, fd_at_least_one/1, fd_at_most_one/1,
fd_only_one/1

Templates

fd_cardinality(+fd_bool_evaluable_list, ?fd_variable)
fd_cardinality(+integer, ?fd_variable, +integer)
fd_at_least_one(+fd_bool_evaluable_list)
fd_at_most_one(+fd_bool_evaluable_list)
fd_only_one(+fd_bool_evaluable_list)

Description

fd_cardinality(List, Count) unifies Count with the number of constraints that are true in List. This is equivalent to post the constraint B₁ + B₂ + …+ B_n #= Count where each variable Bi is a new variable defined by the constraint B_i #<=> C_i where C_i is the ith constraint of List. Each C_i must be a boolean FD expression (section 9.7.1).

fd_cardinality(Lower, List, Upper) is equivalent to fd_cardinality(List, Count), Lower #=< Count, Count #=< Upper

fd_at_least_one(List) is equivalent to fd_cardinality(List, Count), Count #>= 1.

fd_at_most_one(List) is equivalent to fd_cardinality(List, Count), Count #=< 1.

fd_only_one(List) is equivalent to fd_cardinality(List, 1).

Errors

List is a partial list instantiation_error

List is neither a partial list nor a list type_error(list, List)

Count is neither an FD variable nor an integer type_error(fd_variable, Count)

Lower is a variable instantiation_error

Lower is neither a variable nor an integer type_error(integer, Lower)

Upper is a variable instantiation_error

Upper is neither a variable nor an integer type_error(integer, Upper)

an element E of the List list is an invalid boolean expression an FD boolean constraint (section 9.7.1)

Portability

GNU Prolog predicates.

Previous Up Next

9.7 Boolean and reified constraints

9.7.1 Boolean FD expressions

9.7.2 fd_reified_in/4

9.7.3 (#\)/1 - constraint NOT, (#<=>)/2 - constraint equivalent, (#\<=>)/2 - constraint different, (##)/2 - constraint XOR, (#==>)/2 - constraint imply, (#\==>)/2 - constraint not imply, (#/\)/2 - constraint AND, (#\/\)/2 - constraint NAND, (#\/)/2 - constraint OR, (#\\/)/2 - constraint NOR

9.7.4 fd_cardinality/2, fd_cardinality/3, fd_at_least_one/1, fd_at_most_one/1, fd_only_one/1

9.7.3 (#\)/1 - constraint NOT, (#<=>)/2 - constraint equivalent,
(#\<=>)/2 - constraint different, (##)/2 - constraint XOR,
(#==>)/2 - constraint imply, (#\==>)/2 - constraint not imply,
(#/\)/2 - constraint AND, (#\/\)/2 - constraint NAND,
(#\/)/2 - constraint OR, (#\\/)/2 - constraint NOR

9.7.4 fd_cardinality/2, fd_cardinality/3, fd_at_least_one/1, fd_at_most_one/1,
fd_only_one/1