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 MAXSAT objective
 Obj:=sum(i in R) bv(i).var

! Solve as optimization (MAXSAT) 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")