List of all satisfied constraints at any step

[pg2...@columbia.edu]

Is there a way to print out all the satisfied constraints at any time in the decision process (e.g. decision level 1,2,3...)? 

I have some questions regarding clause representation:

1. What is a mapping from clause reference in the solver to the problem clause? Does clause.cref maps to the number of the constraint in the problem. 

2. How does this reference work in the case of learnt clauses? 

3. I was expecting to read the satisfied constraints through watches, but it seems to be not helping. Any pointers in this direction?

[Norbert Manthey]

Answers to your questions inline.

Am Dienstag, 15. Mai 2018 12:37:13 UTC+2 schrieb pg2...@columbia.edu:

Is there a way to print out all the satisfied constraints at any time in the decision process (e.g. decision level 1,2,3...)? 

The way clauses are maintained inside the solver, the only (simple) way is for iterate over the full formula and print the satisfied clauses, e.g.:

Clause& c = ca[cs[i]]; for (int i = 0; i < cs.size(); i++)

  if (satisfied(c))

    cout << c << endl; // <- this operator is not implemented in github minisat (yet)

However, keep in mind that the simplify() method removes satisfied clauses, so that over time you might lose some of them in your output. (there is a remove_satisfied member, that can be set to false, to prevent these situations).

I have some questions regarding clause representation:

1. What is a mapping from clause reference in the solver to the problem clause? Does clause.cref maps to the number of the constraint in the problem. 

There is no direct mapping. clause.cref is an offset into the clause allocator (member ca of the Solver class). During allocation, this value is assigned. During garbageCollection the value of cref can change. The best you can get is the order of the clauses in the clauses member, which stores the references to clauses in the input problem, but also there clauses might be missing after reading the input formula already (because they are tautologies or satisfied due to units in the input that have been propagated). Again, that vector is updated during simplify()+garbageCollect.

2. How does this reference work in the case of learnt clauses? 

The references work the same for learnt clauses. During allocation the value is created, and modified during garbageCollection.

3. I was expecting to read the satisfied constraints through watches, but it seems to be not helping. Any pointers in this direction?

Watches are not sufficient, as a watch for literal 1 stores a subset of all the clauses the might be falsified when assigning 1 to true, e.g. the clause (-1, -2, -3). Let -2 be the other watch for that clause, and no other literal will be watched, due to the way the 2 watched literal scheme works. If you assign 3 to false, this clause is satisfied. However, you will not find it in the watch list of -3. Checking the clauses in the watch list of 3 gives you a list of satisfied clauses, but this list might not be complete (see the example I just gave).

I hope this helps,

Best,
Norbert