Stream: t-cargo/PubGrub

Topic: CDCL terminology


view this post on Zulip Matthieu Pizenberg (Oct 28 2020 at 22:49):

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

view this post on Zulip Matthieu Pizenberg (Oct 28 2020 at 22:50):

Do any of you know why PubGrub decided to work with incompatibilities instead of clauses like it's done in traditional CDCL?

view this post on Zulip Eh2406 (Oct 28 2020 at 23:16):

I think that reframing comes from the "Answer Set Solving" authors.

view this post on Zulip Matthieu Pizenberg (Oct 28 2020 at 23:17):

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