CLP(Boolean)

CLP(Boolean) can be considered as a special case of CLP(FD) where each variable has a domain of two values: 0 denotes false, and 1 denotes true. A Boolean expression is made from constants (0 or 1), Boolean domain variables, basic relational constraints, and operators as follows:

   <BooleanExpression> ::=  
        0 |                                           /* false */
        1 |                                           /* true */
        variable |
        <Expression> #= <Expression> |        
        <Expression> #\= <Expression> |       
        <Expression> #> <Expression> |        
        <Expression> #>= <Expression> |       
        <Expression> #< <Expression> |        
        <Expression> #=< <Expression> |       
        #\ <BooleanExpression> |                       /* not */
        <BooleanExpression> #/\ <BooleanExpression> |  /* and */
        <BooleanExpression> #\/ <BooleanExpression> |  /* or */
        <BooleanExpression> #=> <BooleanExpression> |  /* imply */
        <BooleanExpression> #<=> <BooleanExpression> | /* equivalent */
        <BooleanExpression> #\ <BooleanExpression>     /* xor */

 

A Boolean constraint is made of a constraint symbol and one or two Boolean expressions.

• E1 #= E2: True if E1 and E2 are equivalent. For example, (X #= 3) #= (Y #= 5) means that the finite-domain constraints (X #= 3) and (Y #= 5) have the same satisfibility. In other words, they are either both true or both false.

• E1 #\= E2: True if E1 and E2 are different. For example, (X #= 3) #\= (Y #= 5) means that the finite-domain constraints (X #= 3) and (Y #= 5) are mutually exclusive. In other words, if (X #= 3) is satisfied then (Y #= 5) cannot be satisfied, and similarly if (X #= 3) is not satisfied then (Y #= 5) must be satisfied.

• #\ E: Equivalent to E#=0.  

• E1 #/\ E2: Both E1 and E2 are 1.  

• E1 #\/ E2: Either E1 or E2 is 1.

   

• E1 #=> E2: If E1 is 1, then E2 must be also 1.  

• E1 #<=> E2: E1 and E2 are equivalent.  

• E1 #\ E2: Exactly one of E1 and E2 is 1.  

The following constraints restrict the values of Boolean variables.

• fd_at_least_one(L):
• at_least_one(L): Succeeds if at least one element in L is equal to 1, where L is a list of Boolean variables or constants.  

• fd_at_most_one(L):
• at_most_one(L): Succeeds if at most one element in L is equal to 1, where L is a list of Boolean variables or constants.  

• fd_only_one(L):
• only_one(L): Succeeds if exactly one element in L is equal to 1, where L is a list of Boolean variables or constants.