Encoding equality of derived variables

[Jerome H]

Hello,

I am working on a prototype timetabling application and got started with SAT only recently. The app works like this:

1/ translate the constraints (overlapping, who can do what) to a satisfaction problem in CNF. These set of clauses involves my free variables x(i).

2/ create new boolean variables that are derived from the satisfaction variables x(i), e.g. there is a variable indicating whether somebody is busy on a specific day. For example for day j:
d(j) <=> x(1) \/ ... \/ x(n)
There are other variables for the first/last busy time slot in a day.
The relation shown for d(j) is translated to CNF exactly like the math book says.

3/ Finally I derive my objective from the derived variables (the d(j)'s, first slot, last slot) and convert the whole thing to OPB in the most straightforward way (not x(i) becomes 1 - x(i)). I feed the OPB to minisat+ or SCIP. (On a toy dataset minisat+ finds the optimum first but SCIP demonstrates optimality first).

My question concerns step 2/. Expressing the d(j)'s with an equivalence relation is mathematically sound, but conceptually, I looks overkill. Still a simple one way implication looks too weak either.
I am uncomfortable with that. The SAT solver is not expected to freely play with the d(i)'s. In my mind, this is an output of the model.

Does someone think my model can be lightened, especially when it comes to those equivalence relations between my core sat variables and the derived variables?

Best regards,
Jerome.

[keith....@bt.com]

Have you checked Knuth's new book on satisfiability, which has lots of material comparing the efficiency of various encodings?

Keith

--

---
You received this message because you are subscribed to the Google Groups "MiniSat" group.
To unsubscribe from this group and stop receiving emails from it, send an email to minisat+u...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Jerome H]

I have not checked that one nor the former one's. Read the synopsis. Sounds intriguing especially "phase changes in random processes" :)
I'll give it a go, maybe that will be the start of the collection.
Actually I realised yesterday I do not have to explicitly instantiate the d(j)'s. I can express my objective directly in terms of the x(i)'s. That would remove a number of clauses, but it is trickier to code.
BR,
Jerome.