### 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();
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 10b = 3) (a 10c 7). Then we encode this into JaCoP SAT solver.

IntVec clause = new IntVec(wrapper.pool);

// first clause

clause = new IntVec(wrapper.pool);

// second clause

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