diff options
author | Alex Ozdemir <aozdemir@hmc.edu> | 2019-01-15 23:55:29 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-01-15 23:55:29 -0800 |
commit | 1e6293daa3f6d61c9035e22ee76448b46dd83ce8 (patch) | |
tree | 4e90bc4c0e4b303cf86020d917c8292544569171 /proofs/signatures/sat.plf | |
parent | 534a9b73dae2c0a3b6040f6a51f824ca69850c4b (diff) |
Extended Resolution Signature (#2788)
* Extended Resolution Signature
While extended resolution is a fairly general technique, the paper
"Extended Resolution Simulates DRAT" / the drat2er uses exactly one new
type of rule: definitions of the form
new <=> old v (~l_1 ^ ~l_2 ^ ... ^ ~l_n)
This PR adds axioms supporting this kind of definition, and adds a test
making use of those new axioms. The axioms support the following ideas:
1. Introducing a **fresh** variable, defined in the form above
2. Clausifying that definition to produce proofs of $$ n + 2 $$ new
clauses in the form of two clauses, and a cnf with $$ n $$ clauses
3. An axiom for unrolling the proof of the cnf into proofs of the
original clauses.
* Addressing Yoni's comments
1. Added a new (trivial) test
2. Improved a bunch of documentation
* Update proofs/signatures/er.plf
Co-Authored-By: alex-ozdemir <aozdemir@hmc.edu>
* Removed references to RATs from the signature
There are still a few references in the header comment.
* Aside on continuations
* Scrap the elision annotations
Diffstat (limited to 'proofs/signatures/sat.plf')
-rw-r--r-- | proofs/signatures/sat.plf | 46 |
1 files changed, 46 insertions, 0 deletions
diff --git a/proofs/signatures/sat.plf b/proofs/signatures/sat.plf index 8f40aa8bf..574191493 100644 --- a/proofs/signatures/sat.plf +++ b/proofs/signatures/sat.plf @@ -8,10 +8,22 @@ (declare pos (! x var lit)) (declare neg (! x var lit)) +; Flip the polarity of the literal +(program lit_flip ((l lit)) lit + (match l + ((pos v) (neg v)) + ((neg v) (pos v)))) + (declare clause type) (declare cln clause) (declare clc (! x lit (! c clause clause))) +; A list of clauses, CNF if interpretted as a formula, +; but also sometimes just a list +(declare cnf type) +(declare cnfn cnf) +(declare cnfc (! h clause (! t cnf cnf))) + ; constructs for general clauses for R, Q, satlem (declare concat_cl (! c1 clause (! c2 clause clause))) @@ -107,6 +119,40 @@ (! u2 (! v (holds c) (holds c2)) (holds c2)))))) + +; Returns a copy of `c` with any duplicate literals removed. +; Never fails. +; Uses marks 3 & 4. Expects them to be clear before hand, and leaves them clear +; afterwards. +(program clause_dedup ((c clause)) clause + (match c + (cln cln) + ((clc l rest) + (match l + ((pos v) (ifmarked3 + v + (clause_dedup rest) + (do (markvar3 v) + (let result (clc (pos v) (clause_dedup rest)) + (do (markvar3 v) result))))) + ((neg v) (ifmarked4 + v + (clause_dedup rest) + (do (markvar4 v) + (let result (clc (neg v) (clause_dedup rest)) + (do (markvar4 v) result))))))))) + +(declare cnf_holds (! c cnf type)) +(declare cnfn_proof (cnf_holds cnfn)) +(declare cnfc_proof + (! c clause + (! deduped_c clause + (! rest cnf + (! proof_c (holds c) + (! proof_rest (cnf_holds rest) + (! sc (^ (clause_dedup c) deduped_c) + (cnf_holds (cnfc c rest))))))))) + ; A little example to demonstrate simplify_clause. ; It can handle nested clr's of both polarities, ; and correctly cleans up marks when it leaves a |