Boolean variables and logical constraints

The Mosel module mmxprs defines the entity type boolvar for representing a pseudo boolean decision variable. This type supports the operators and, or and not for building logical expressions and can be combined with ordinary Boolean variables (type boolean). A logical constraint is specified either by associating a pseudo boolean variable to a logical expression or by forcing the truth value (i.e. true or false) of an expression as shown in the code example below. When a logical expression is used on its own as a statement it is implicitly turned into a constraint (forced to true) and added to the constraint store.

 uses "mmxprs"

 public declarations
   R=1..5
   bv: array(R) of boolvar
   LC1, LC2: logctr
 end-declarations

! Simple clause, same as:  bv(1) and not bv(5) = true
 bv(1) and not bv(5)

! Association of clauses
 bv(3)=(not bv(4))

! The opposite of 'bv(1) or bv(3)' must be false
 (not (bv(1) or bv(3)))=false

! Defining a logic expression (not recorded in the constraint store)
 LC1:= and(i in 1..3) bv(i) or and(i in 4..5) not bv(i)

! Turn expression into a constraint
 LC1:= LC1=true

! A named logic expression (this defines a constraint)
 LC2:= (or(i in 1..3) not bv(i)) = false

! Solve as feasibility (SAT) problem
 maximise(0)
 if getprobstat=XPRS_OPT then
   writeln("Problem is feasible")
 else
   writeln("Problem is unsatisfiable")
 end-if

Correspondence with MIP

Each boolvar is represented in the MIP problem by two binary variables (mpvar): one for the value itself and second one for its negation. These decision variables can be accessed from the model using the function getvar such that they can be used in linear constraints. The solution value of a boolvar is of type boolean and can be obtained using getsol.

! Retrieve associated binary variables for formulation of an objective function
 Obj:=sum(i in R) bv(i).var

! Solve as optimization problem
 maximise(Obj)
 if getprobstat=XPRS_OPT then
   writeln("Solution: ", getobjval)
   forall(i in R) writeln(i, ": ", bv(i).sol)
 end-if

The problem matrix can be output from the solver to inspect the resulting formulation: note that the logic relations are represented via general constraints by the MIP solver.

 loadprob(Obj)
 writeprob("testout.lp","l")