From: Alex Ozdemir Date: Wed, 16 Jan 2019 07:55:29 +0000 (-0800) Subject: Extended Resolution Signature (#2788) X-Git-Tag: cvc5-1.0.0~4283 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1e6293daa3f6d61c9035e22ee76448b46dd83ce8;p=cvc5.git 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 * Removed references to RATs from the signature There are still a few references in the header comment. * Aside on continuations * Scrap the elision annotations --- diff --git a/proofs/signatures/drat.plf b/proofs/signatures/drat.plf index d52586bc9..b529ff893 100644 --- a/proofs/signatures/drat.plf +++ b/proofs/signatures/drat.plf @@ -13,17 +13,6 @@ ; ; This signature checks **Specified DRAT**. -(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 DRAT proof itself: a list of addition or deletion instructions. (declare DRATProof type) (declare DRATProofn DRATProof) diff --git a/proofs/signatures/er.plf b/proofs/signatures/er.plf new file mode 100644 index 000000000..8b559671e --- /dev/null +++ b/proofs/signatures/er.plf @@ -0,0 +1,125 @@ +; Depends on sat.plf + +; This file exists to support the **definition introduction** (or **extension**) +; rule in the paper: +; "Extended Resolution Simulates DRAT" +; which can be found at http://www.cs.utexas.edu/~marijn/publications/ijcar18.pdf +; +; The core idea of extended resolution is that given **any** formula f +; involving the variables from some SAT problem, one can introduce the +; constraint +; +; new <=> f +; +; without changing satisfiability, where "new" is a fresh variable. +; +; This signature does not provide axioms for facilitating full use of this +; idea. Instead, this signature facilitates use of one specific kind of +; extension, that of the form: +; +; new <=> old v (~l_1 ^ ~l_2 ^ ... ^ ~l_n) +; +; which translates into the clauses: +; +; new v l_1 v l_2 v ... v l_n +; new v ~old +; for each i <= n: l_i v ~new v old +; +; This kind of extension is (a) sufficient to simulate DRAT proofs and (b) easy +; to convert to clauses, which is why we use it. + +; A definition witness value for: +; new <=> old v (~others_1 ^ ~others_2 ^ ... ^ ~others_n) +; It witnesses the fact that new was fresh when it was defined by the above. +; +; Thus it witnesses that the above, when added to the formula consisting of the +; conjunction all the already-proven clauses, produces an equisatisfiable +; formula. +(declare definition (! new var (! old lit (! others clause type)))) + +; Given `old` and `others`, this takes a continuation which expects +; 1. a fresh variable `new` +; 2. a definition witness value for: +; new <=> old v (~others_1 ^ ~others_2 ^ ... ^ ~others_n) +; +; Aside: +; In programming a **continuation** of some computation is a function that +; takes the results of that computation as arguments to produce a final +; result. +; +; In proof-construction a **continuation** of some reasoning is a function +; that takes the results of that reasoning as arguments to proof a final +; result. +; +; That definition witness value can be clausified using the rule below. +; +; There need to be two different rules because the side-condition for +; clausification needs access to the new variable, which doesn't exist except +; inside the continuation, which is out-of-scope for any side-condition +; associated with this rule. +(declare decl_definition + (! old lit + (! others clause ; List of vars + (! pf_continuation (! new var (! def (definition new old others) + (holds cln))) + (holds cln))))) + +; Takes a `list` of literals and a clause, `suffix`, adds the suffix to each +; literal and returns a list of clauses as a `cnf`. +(program clause_add_suffix_all ((list clause) (suffix clause)) cnf + (match list + (cln cnfn) + ((clc l rest) (cnfc (clc l suffix) + (clause_add_suffix_all rest suffix))))) + +; This translates a definition witness value for the def: +; +; new <=> old v (~l_1 ^ ~l_2 ^ ... ^ ~l_n) +; +; into the clauses: +; +; new v l_1 v l_2 v ... v l_n +; new v ~old +; for each i <= n: l_i v ~new v old (encoded as (cnf_holds ...)) +(declare clausify_definition + (! new var + (! old lit + (! others clause + ; Given a definition { new <-> old v (~l_1 ^ ~l_2 ^ ... ^ ~l_n) } + (! def (definition new old others) + (! negOld lit + (! mkNegOld (^ (lit_flip old) negOld) + (! provenCnf cnf + (! mkProvenCnf (^ (clause_add_suffix_all + others + (clc (neg new) (clc old cln))) provenCnf) + ; If you can prove bottom from its clausal representation + (! pf_continuation + ; new v l_1 v l_2 v ... v l_n + (! pf_c1 (holds (clc (pos new) others)) + ; new v ~old + (! pf_c2 (holds (clc (pos new) (clc negOld cln))) + ; for each i <= n: l_i v ~new v old + (! pf_cs (cnf_holds provenCnf) + (holds cln)))) + ; Then you've proven bottom + (holds cln))))))))))) + +; This axiom is useful for converting a proof of some CNF formula (a value of +; type (cnf_holds ...)) into proofs of the constituent clauses (many values of +; type (holds ...)). +; Given +; 1. a proof of some cnf, first ^ rest, and +; 2. a proof continuation that +; a. takes in proofs of +; i. first and +; ii. rest and +; b. proceeds to prove bottom, +; proves bottom. +(declare cnfc_unroll_towards_bottom + (! first clause + (! rest cnf + (! pf (cnf_holds (cnfc first rest)) + (! pf_continuation (! r1 (holds first) (! r2 (cnf_holds rest) (holds cln))) + (holds cln)))))) + diff --git a/proofs/signatures/er_test.plf b/proofs/signatures/er_test.plf new file mode 100644 index 000000000..27c61de1f --- /dev/null +++ b/proofs/signatures/er_test.plf @@ -0,0 +1,116 @@ +; Depends on er.plf + +; Type for representing success when testing a side-condition +(declare TestSuccess type) + +; Test for clause_add_suffix_all +(declare test_clause_add_suffix_all + (! list clause + (! suffix clause + (! result cnf + (! (^ (clause_add_suffix_all list suffix) result) + TestSuccess))))) + +(check + (% a lit + (% b lit + (% c lit + (test_clause_add_suffix_all + (clc a (clc b cln)) + (clc c cln) + (cnfc (clc a (clc c cln)) + (cnfc (clc b (clc c cln)) + cnfn)) + ) + ))) +) + +; This is a circuitous proof that uses the definition introduction and +; unrolling rules +(check + (% v1 var + (% v2 var + (% pf_c1 (holds (clc (pos v1) (clc (pos v2) cln))) + (% pf_c2 (holds (clc (neg v1) (clc (pos v2) cln))) + (% pf_c3 (holds (clc (pos v1) (clc (neg v2) cln))) + (% pf_c4 (holds (clc (neg v1) (clc (neg v2) cln))) + (: (holds cln) + (decl_definition + (neg v1) + (clc (neg v2) cln) + (\ v3 + (\ def3 + (clausify_definition _ _ _ def3 _ _ + (\ pf_c5 ; type: (holds (clc (pos v3) (clc (neg v2) cln))) + (\ pf_c6 ; type: (holds (clc (pos v3) (clc (pos v1) cln))) + (\ pf_cnf3 ; type: (cnf_holds (cnfc (clc (neg v2) (clc (neg v3) (clc (neg v1) cln))) cnfn)) + (cnfc_unroll_towards_bottom _ _ pf_cnf3 + (\ pf_c7 ; type: (clc (neg v2) (clc (neg v3) (clc (neg v1) cln))) + (\ pf_cnfn + ; Clauses + (satlem_simplify _ _ _ (R _ _ pf_c1 pf_c2 v1) (\ pf_c8 ; v2 + (satlem_simplify _ _ _ (R _ _ pf_c8 pf_c5 v2) (\ pf_c9 ; v3 + (satlem_simplify _ _ _ (R _ _ pf_c9 pf_c7 v3) (\ pf_c10 ; ~v2 ~v1 + (satlem_simplify _ _ _ (Q _ _ pf_c10 pf_c8 v2) (\ pf_c11 ; ~v1 + (satlem_simplify _ _ _ (Q _ _ pf_c11 pf_c3 v1) (\ pf_c12 ; ~v2 + (satlem_simplify _ _ _ (Q _ _ pf_c12 pf_c8 v2) (\ pf_c13 ; empty + pf_c13 + )) + )) + )) + )) + )) + )) + ))) + ))) + ) + )) + ) + ) + )))) + )) +) + +; This is a test of ER proof produced by drat2er on Example 1 from: +; https://www.cs.utexas.edu/~marijn/drat-trim/ +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (% pf_c1 (holds (clc (pos v1) (clc (pos v2) (clc (neg v3) cln)))) + (% pf_c2 (holds (clc (neg v1) (clc (neg v2) (clc (pos v3) cln)))) + (% pf_c3 (holds (clc (pos v2) (clc (pos v3) (clc (neg v4) cln)))) + (% pf_c4 (holds (clc (neg v2) (clc (neg v3) (clc (pos v4) cln)))) + (% pf_c5 (holds (clc (neg v1) (clc (neg v3) (clc (neg v4) cln)))) + (% pf_c6 (holds (clc (pos v1) (clc (pos v3) (clc (pos v4) cln)))) + (% pf_c7 (holds (clc (neg v1) (clc (pos v2) (clc (pos v4) cln)))) + (% pf_c8 (holds (clc (pos v1) (clc (neg v2) (clc (neg v4) cln)))) + (: (holds cln) + (decl_definition + (neg v1) + cln + (\ v5 + (\ def1 + (clausify_definition _ _ _ def1 _ _ + (\ pf_c9 ; type: (holds (clc (pos def1v) cln)) + (\ pf_c10 ; type: (holds (clc (pos def1v) (clc (pos v1) cln))) + (\ idc0 ; type: (cnf_holds cnfn) + (satlem_simplify _ _ _ (R _ _ pf_c10 pf_c7 v1) (\ pf_c11 + (satlem_simplify _ _ _ (R _ _ pf_c10 pf_c5 v1) (\ pf_c12 + (satlem_simplify _ _ _ (R _ _ pf_c10 pf_c2 v1) (\ pf_c13 + (satlem_simplify _ _ _ (Q _ _ (R _ _ pf_c2 pf_c5 v3) pf_c8 v1) (\ pf_c14 + (satlem_simplify _ _ _ (Q _ _ (R _ _ pf_c7 pf_c2 v2) pf_c6 v1) (\ pf_c15 + (satlem_simplify _ _ _ (Q _ _ (R _ _ pf_c7 pf_c5 v4) pf_c1 v1) (\ pf_c16 + (satlem_simplify _ _ _ (R _ _ (Q _ _ pf_c3 pf_c15 v4) pf_c16 v3) (\ pf_c17 + (satlem_simplify _ _ _ (Q _ _ (R _ _ (Q _ _ pf_c4 pf_c15 v3) pf_c14 v4) pf_c17 v2) (\ pf_c18 + pf_c18 + )))))))))))))))) + ))) + ) + )) + ) + ) + )))))))) + )))) +) diff --git a/proofs/signatures/lrat.plf b/proofs/signatures/lrat.plf index 5224cf3ce..ae6cbd101 100644 --- a/proofs/signatures/lrat.plf +++ b/proofs/signatures/lrat.plf @@ -9,12 +9,6 @@ ; Some side-conditions make use of a _global assignment_ encoded in ; 0 (true) / 1 (false) marks on variables. -; 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))) - ; Unit (https://en.wikipedia.org/wiki/Unit_type) ; For functions that don't return anything (declare Unit type) ; The type with only one value (like `void` in C) @@ -89,12 +83,6 @@ ; Functional programs for manipulating types ; ; ========================================== ; -; Flip the polarity of the literal -(program lit_flip ((l lit)) lit - (match l - ((pos v) (neg v)) - ((neg v) (pos v)))) - ; Are two literal equal? (program lit_eq ((l1 lit) (l2 lit)) bool (match l1 @@ -130,28 +118,6 @@ (ff (clause_contains_lit c' l)))) (cln ff))) -; 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))))))))) - ; Append two traces (program Trace_concat ((t1 Trace) (t2 Trace)) Trace (match t1 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