ipasir2_redundancy and meaning

[m-fleury]

I think that it is important to mention in the meaning of ipasir2_redundancy what the answer of the solver is supposed to mean and not only how the solver is supposed to handle those cases.

Overall , as far as I understand, the state is along the lines of the following where the external state knows some clauses (called E for external):

|--------------|
|clauses  E    |                   |-------------------------------------|
|external      |-------------->    |sat solver with clauses N            |
|--------------|                   |-------------------------------------|

So the intended meaning is that all clauses are part of E+N

• IPASIR2_R_NONE: hard to derive again, the solver must keep them
• IPASIR2_R_FORGETTABLE: easy to derive again, will be added again if needed

Then there are two that are unclear to me:

• IPASIR2_R_EQUISATISFIABLE
• IPASIR2_R_EQUIVALENT
  Should they maintain satisfiability/equivalence of N? or of E+N? This is different when E is unsat und N is (still) sat.

EDIT: This kind of questions is important for symmetry breaking: it should be deterministic and you cannot add IPASIR2_R_FORGETTABLE in both directions…

[Udopia]

Thanks for pointing this out, I started to add pragmatics to the documentation with commit f2a9a11

To clarify: IPASIR2_R_EQUISATISFIABLE and IPASIR2_R_EQUIVALENT address only N. Pragmatics: Clause Sharing Parallel SAT Solver Frameworks exchanging Clauses deduced by Resolution (or Extended Resolution / Blocked Sets).