7.2 FDV encoding and constraint translations

SatWrapper offers a general way to define literals and clauses. The process is divided into two parts. First, each FDV and a inequality relation on it is bound to a literal. Then a clause is defined on the literals. We illustrate this process below.

Assume that we want to define a constraint (a 10) (b = 3 c > 7) with IntVar a, b and c. The literals for this constraint are defined as a 10, b = 3and c 7(negation of this literal is a > 7). This is encoded in JaCoP as follows.

   IntVar a = new IntVar(store, "a", 0, 100); 
   IntVar b = new IntVar(store, "b", 0, 100); 
   IntVar c = new IntVar(store, "c", 0, 100); 
   SatWrapper wrapper = new SatWrapper(); 
   int aLiteral = wrapper.cpVarToBoolVar(a, 10, false); 
   int bLiteral = wrapper.cpVarToBoolVar(b, 3, true); 
   int cLiteral = wrapper.cpVarToBoolVar(c, 7, false);

In the above method cpVarToBoolVar the first parameter is the FDV variable, the second is the rhs value and the third parameter defines type if relation (false for and true for =).

When literals are defined we can generate clauses using CNF format, as presented below. First, we translate the clause to CNF form as (a 10b = 3) (a 10c 7). Then we encode this into JaCoP SAT solver.

   IntVec clause = new IntVec(wrapper.pool); 
   // first clause 
   clause.add(- aLiteral); 
   clause = new IntVec(wrapper.pool); 
   // second clause 
   clause.add(- aLiteral); 
   clause.add(- cLiteral); 

In the above code minus in front of the literal in statement clause.add means that the negated literal is added to the clause.

A possible solution generated by JaCoP is {0, 3, 8 }.