FDV encoding and constraint translations

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 = 3⟧ and ⟦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();
   store.impose(wrapper);

   wrapper.register(a);
   wrapper.register(b);
   wrapper.register(c);

   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 ≤ 10⟧∨⟦b = 3⟧) ∧ (⟦a ≤ 10⟧∨⟦c ≤ 7⟧). Then we encode this into JaCoP SAT solver.

   IntVec clause = new IntVec(wrapper.pool);

   // first clause
   clause.add(- aLiteral);
   clause.add(bLiteral);
   wrapper.addModelClause(clause.toArray());

   clause = new IntVec(wrapper.pool);

   // second clause
   clause.add(- aLiteral);
   clause.add(- cLiteral);
   wrapper.addModelClause(clause.toArray());

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 }.

[prev] [prev-tail] [front] [up]