While writing the guide on internals, I want to make a clear link between PubGrub terminology and CDCL (conflict driven clause learning) terminology. It is clear that terms correspond to literals, but it's less clear what incompatibilities are. I would tend to say that they correspond to clauses, but clauses rather seems to be the opposite of incompatibilities. While a clause is a disjunction that should have at least one literal evaluated true, incompatibilities are conjunctions that must evaluate to false (have at least one literal that is false).
Do any of you know why PubGrub decided to work with incompatibilities instead of clauses like it's done in traditional CDCL?
I think that reframing comes from the "Answer Set Solving" authors.
Ah I think I found the reason. PubGrub is actually mostly inspired by Potassco (https://potassco.org/teaching/) and there, incompatibilities are called "nogoods" and the algorithm is called CDNL for conflict driven nogood learning instead of CDCL
Last updated: Oct 21 2021 at 21:46 UTC