Theory Watched_Literals_Transition_System
theory Watched_Literals_Transition_System
imports More_Sepref.WB_More_Refinement CDCL.CDCL_W_Abstract_State
CDCL.CDCL_W_Restart CDCL.Pragmatic_CDCL
begin
chapter ‹Two-Watched Literals›
section ‹Rule-based system›
text ‹
We define the calculus and map it to the pragmatic CDCL in order to inherit termination and
correctness.
We initially inherited directly from CDCL, but this had two issues:
▪ First, there are inprocessing techniques we could not express (like subsumption-resolution, see
the comments on PCDCL)...
▪ ... however, we tried to (had to) still express some of them (mostly about handling unit
literals), leading to more complicated proofs. Additionally all of it was an afterthought (like
the idea that clauses containing a true literal can be removed) and was never properly
implemented (in that case, because there was no solution for clauses containing a false
literal).
On a slightly less important note, but related, we support tautologies in our calculus, but this
turned to be rather annoying in the generated code, because the length of clause does not fit in
32-bit native unsigned integers anymore (at least not with our encoding). We use 64-bit integer
instead, but this lead to other work arounds (like position saving that actually save the position
minus 2 to avoid overflow problems).
To overcome the issue, we decided to inherite not from CDCL, but from a different calculus devised
exactly to express a more realistic calculus for SAT solvers.
›
subsection ‹Types and Transitions System›
subsubsection ‹Types and accessing functions›