From: Alex Ozdemir Date: Mon, 17 Dec 2018 01:49:34 +0000 (-0800) Subject: DRAT Signature (#2757) X-Git-Tag: cvc5-1.0.0~4315 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=bc40c176eb1205452e824ec9d89dc9a7c76cbd67;p=cvc5.git DRAT Signature (#2757) * DRAT signature Added the DRAT signature to CVC4. We'll need this in order to compare three BV proof pipelines: 1. DRAT -> Resolution -> Check 2. DRAT -> LRAT -> Check 3. DRAT -> Check (this one!) Tested the signature using the attached test file. i.e. running ``` lfscc sat.plf smt.plf lrat.plf drat.plf drat_test.plf ``` * Added type annotations for tests * Respond to Yoni's review * Apply Yoni's suggestions from code review Documentation polish Co-Authored-By: alex-ozdemir * Whoops, missed a spot or two --- diff --git a/proofs/signatures/drat.plf b/proofs/signatures/drat.plf new file mode 100644 index 000000000..d52586bc9 --- /dev/null +++ b/proofs/signatures/drat.plf @@ -0,0 +1,224 @@ +; Depends on lrat.plf +; +; Implementation of DRAT checking. +; +; Unfortunately, there are **two** different notions of DRAT floating around in +; the world: +; * Specified DRAT : This is a reasonable proof format +; * Operational DRAT : This is a variant of specified DRAT warped by the +; details of common SAT solver architectures. +; +; Both are detailed in this paper, along with their differences: +; http://fmv.jku.at/papers/RebolaPardoBiere-POS18.pdf +; +; 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) +(declare DRATProofa (! c clause (! p DRATProof DRATProof))) +(declare DRATProofd (! c clause (! p DRATProof DRATProof))) + +; ==================== ; +; Functional Programs ; +; ==================== ; + +; Are two clauses equal (in the set sense) +; +; Since clauses are sets, it is insufficient to do list equality +; We could sort them, but that would require defining an order on our variables, +; and incurring the cost of sorting. +; Instead, we do the following: +; 1. Sweep the first clause, marking variables with flags 1 (pos) and 2 (neg) +; 2. Sweep the second clause, erasing marks. +; 3. Unsweep the first clause, returning FALSE on marks. +; Also unmarking +; TODO(aozdemir) This implementation could be further optimized b/c once c1 is +; drained, we need not continue to pattern match on it. +(program clause_eq ((c1 clause) (c2 clause)) bool + (match + c1 + (cln (match + c2 + (cln tt) + ((clc c2h c2t) (match + c2h + ((pos v) (ifmarked1 + v + (do (markvar1 v) (clause_eq c1 c2t)) + ff)) + ((neg v) (ifmarked2 + v + (do (markvar2 v) (clause_eq c1 c2t)) + ff)))))) + ((clc c1h c1t) (match + c1h + ((pos v) (do + (markvar1 v) + (let res (clause_eq c1t c2) + (ifmarked1 + v + (do (markvar1 v) ff) + res)))) + ((neg v) (do + (markvar2 v) + (let res (clause_eq c1t c2) + (ifmarked2 + v + (do (markvar2 v) ff) + res)))))))) + +; Does this formula contain bottom as one of its clauses? +(program cnf_has_bottom ((cs cnf)) bool + (match cs + (cnfn ff) + ((cnfc c rest) (match c + (cln tt) + ((clc l c') (cnf_has_bottom rest)))))) + +; Return a new cnf with one copy of this clause removed. +(program cnf_remove_clause ((c clause) (cs cnf)) cnf + (match cs + (cnfn (fail cnf)) + ((cnfc c' cs') + (match (clause_eq c c') + (tt cs') + (ff (cnfc c' (cnf_remove_clause c cs'))))))) + +; return (c1 union (c2 \ ~l)) +; Significant for how a RAT is defined. +(program clause_pseudo_resolvent ((c1 clause) (c2 clause)) clause + (clause_dedup (clause_append c1 + (clause_remove_all + (lit_flip (clause_head c1)) c2)))) + +; Given a formula, `cs` and a clause `c`, return all pseudo resolvents, i.e. all +; (c union (c' \ ~head(c))) +; for c' in cs, where c' contains ~head(c) +(program collect_pseudo_resolvents ((cs cnf) (c clause)) cnf + (match cs + (cnfn cnfn) + ((cnfc c' cs') + (let rest_of_resolvents (collect_pseudo_resolvents cs' c) + (match (clause_contains_lit c' (lit_flip (clause_head c))) + (tt (cnfc (clause_pseudo_resolvent + c + c') + rest_of_resolvents)) + (ff rest_of_resolvents)))))) + +; =============================================================== ; +; Unit Propegation implementation (manipulates global assignment) ; +; =============================================================== ; +; See the lrat file for a description of the global assignment. + +; The result of search for a unit clause in +(declare UnitSearchResult type) +; There was a unit, and +; this is the (previously floating) literal that is now satisfied. +; this is a version of the input cnf with satisfied clauses removed. +(declare USRUnit (! l lit (! f cnf UnitSearchResult))) +; There was an unsat clause +(declare USRBottom UnitSearchResult) +; There was no unit. +(declare USRNoUnit UnitSearchResult) + +; If a UnitSearchResult is a Unit, containing a cnf, adds this clause to that +; cnf. Otherwise, returns the UnitSearchResult unmodified. +(program USR_add_clause ((c clause) (usr UnitSearchResult)) UnitSearchResult + (match usr + ((USRUnit l f) (USRUnit l (cnfc c f))) + (USRBottom USRBottom) + (USRNoUnit USRNoUnit))) + +; Searches through the clauses, looking for a unit clause. +; Reads the global assignment. Possibly assigns one variable. +; Returns +; USRBottom if there is an unsat clause +; (USRUnit l f) if there is a unit, with lit l, and +; f is the cnf with some SAT clauses removed. +; USRNoUnit if there is no unit +(program unit_search ((f cnf)) UnitSearchResult + (match f + (cnfn USRNoUnit) + ((cnfc c f') + (match (clause_check_unit_and_maybe_mark c) + (MRSat (unit_search f')) + ((MRUnit l) (USRUnit l f')) + (MRUnsat USRBottom) + (MRNotUnit (USR_add_clause c (unit_search f'))))))) + + +; Given the current global assignment, does the formula `f` imply bottom via +; unit propegation? Leaves the global assignment in the same state that it was +; initially. +(program unit_propegates_to_bottom ((f cnf)) bool + (match (unit_search f) + (USRBottom tt) + ((USRUnit l f') (let result (unit_propegates_to_bottom f') + (do (lit_un_mk_sat l) + result))) + (USRNoUnit ff))) + +; ================================== ; +; High-Level DRAT checking functions ; +; ================================== ; + +; Is this clause an AT? +(program is_at ((cs cnf) (c clause)) bool + (match (is_t c) + (tt tt) + (ff (do (clause_mk_all_unsat c) + (let r (unit_propegates_to_bottom cs) + (do (clause_un_mk_all_unsat c) + r)))))) + +; Are all of these clauses ATs? +(program are_all_at ((cs cnf) (clauses cnf)) bool + (match clauses + (cnfn tt) + ((cnfc c clauses') + (match (is_at cs c) + (tt (are_all_at cs clauses')) + (ff ff))))) + +; Is the clause `c` a RAT for the formula `cs`? +(program is_rat ((cs cnf) (c clause)) bool + (match (is_t c) + (tt tt) + (ff (match (is_at cs c) + (tt tt) + (ff (are_all_at + cs + (collect_pseudo_resolvents cs c))))))) + +; Is this proof a valid DRAT proof of bottom? +(program is_drat_proof_of_bottom ((f cnf) (proof DRATProof)) bool + (match proof + (DRATProofn (cnf_has_bottom f)) + ((DRATProofa c p) (match + (is_rat f c) + (tt (is_drat_proof_of_bottom (cnfc c f) p)) + (ff ff))) + ((DRATProofd c p) + (is_drat_proof_of_bottom (cnf_remove_clause c f) p)))) + + +(declare drat_proof_of_bottom + (! f cnf + (! proof_of_formula (cnf_holds f) + (! proof DRATProof + (! sc (^ (is_drat_proof_of_bottom f proof) tt) + bottom))))) + diff --git a/proofs/signatures/drat_test.plf b/proofs/signatures/drat_test.plf new file mode 100644 index 000000000..f2f2c7286 --- /dev/null +++ b/proofs/signatures/drat_test.plf @@ -0,0 +1,191 @@ +;depends on drat.plf +(declare check_rat + (! f cnf + (! c clause + (! b bool + (! sc (^ (is_rat f c) b) + bottom))))) + +(declare trust_cnf (! f cnf (cnf_holds f))) + +; RAT Test 1 +; Formula: (-p, -a) ^ (-p, b) ^( b, c) ^ (-c, a) +; Candidate RAT: (p, a) +; Answer: true +(check + (% va var + (% vb var + (% vc var + (% vp var + (check_rat + (cnfc (clc (neg vp) (clc (neg va) cln)) + (cnfc (clc (neg vp) (clc (pos vb) cln)) + (cnfc (clc (pos vb) (clc (pos vc) cln)) + (cnfc (clc (neg vc) (clc (pos va) cln)) cnfn)))) + (clc (pos vp) (clc (pos va) cln)) + tt)))))) + +; RAT Test 2 +; Formula: +; p cnf 4 8 +; 1 2 -3 0 +; -1 -2 3 0 +; 2 3 -4 0 +; -2 -3 4 0 +; -1 -3 -4 0 +; 1 3 4 0 +; -1 2 4 0 +; 1 -2 -4 0 +; Candidate RAT: -1 +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (check_rat + (cnfc (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) + (cnfc (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) + (cnfc (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) + (cnfc (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) + (cnfc (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) + (cnfc (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) + (cnfc (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) + (cnfc (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) + cnfn)))))))) + (clc (neg v1) cln) + tt)))))) + +; RAT Test 3 +; Formula: +; p cnf 4 9 +; 1 2 -3 0 +; -1 -2 3 0 +; 2 3 -4 0 +; -2 -3 4 0 +; -1 -3 -4 0 +; 1 3 4 0 +; -1 2 4 0 +; 1 -2 -4 0 +; -1 0 +; Candidate RAT: 2 +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (check_rat + (cnfc (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) + (cnfc (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) + (cnfc (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) + (cnfc (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) + (cnfc (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) + (cnfc (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) + (cnfc (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) + (cnfc (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) + (cnfc (clc (neg v1) cln) + cnfn))))))))) + (clc (pos v2) cln) + tt)))))) + +; RAT Test 4 +; Formula: +; p cnf 4 2 +; 2 -3 0 +; 1 -4 0 +; Candidate RAT: 3 +; Answer: false +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (check_rat + (cnfc (clc (pos v2) (clc (neg v3) cln)) + (cnfc (clc (pos v1) (clc (neg v4) cln)) cnfn)) + (clc (pos v3) cln) + ff)))))) + + +; DRAT Test 1 (from Example 1 @ https://www.cs.utexas.edu/~marijn/drat-trim/) +; without deletions +; Formula: +; p cnf 4 8 +; 1 2 -3 0 +; -1 -2 3 0 +; 2 3 -4 0 +; -2 -3 4 0 +; -1 -3 -4 0 +; 1 3 4 0 +; -1 2 4 0 +; 1 -2 -4 +; Proof: +; -1 0 +; 2 0 +; 0 +(check + (% v1 var + (% v2 var + (% v3 var + (% v4 var + (: + (holds cln) + (drat_proof_of_bottom _ + (trust_cnf (cnfc (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) + (cnfc (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) + (cnfc (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) + (cnfc (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) + (cnfc (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) + (cnfc (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) + (cnfc (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) + (cnfc (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) + cnfn))))))))) + (DRATProofa (clc (neg v1) cln) + (DRATProofa (clc (pos v2) cln) + (DRATProofa cln + DRATProofn)))))))))) + + +; DRAT Test 2 (from Example 1 @ https://www.cs.utexas.edu/~marijn/drat-trim/) +; with deletions +; Formula: +; p cnf 4 8 +; 1 2 -3 0 +; -1 -2 3 0 +; 2 3 -4 0 +; -2 -3 4 0 +; -1 -3 -4 0 +; 1 3 4 0 +; -1 2 4 0 +; 1 -2 -4 +; Proof: +; -1 0 +; d -1 -2 3 0 +; d -1 -3 -4 0 +; d -1 2 4 0 +; 2 0 +; d 1 2 -3 0 +; d 2 3 -4 0 +; 0 +(check + (% v1 var (% v2 var (% v3 var (% v4 var + (: (holds cln) + (drat_proof_of_bottom _ + (trust_cnf + (cnfc (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) + (cnfc (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) + (cnfc (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) + (cnfc (clc (neg v2) (clc (neg v3) (clc (pos v4) cln))) + (cnfc (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) + (cnfc (clc (pos v1) (clc (pos v3) (clc (pos v4) cln))) + (cnfc (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) + (cnfc (clc (pos v1) (clc (neg v2) (clc (neg v4) cln))) + cnfn))))))))) + (DRATProofa (clc (neg v1) cln) + (DRATProofd (clc (neg v1) (clc (neg v2) (clc (pos v3) cln))) + (DRATProofd (clc (neg v1) (clc (neg v3) (clc (neg v4) cln))) + (DRATProofd (clc (neg v1) (clc (pos v2) (clc (pos v4) cln))) + (DRATProofa (clc (pos v2) cln) + (DRATProofd (clc (pos v1) (clc (pos v2) (clc (neg v3) cln))) + (DRATProofd (clc (pos v2) (clc (pos v3) (clc (neg v4) cln))) + (DRATProofa cln + DRATProofn))))))))))))))) diff --git a/proofs/signatures/lrat.plf b/proofs/signatures/lrat.plf index 96cdd83b3..5224cf3ce 100644 --- a/proofs/signatures/lrat.plf +++ b/proofs/signatures/lrat.plf @@ -1,5 +1,6 @@ ; LRAT Proof signature ; LRAT format detailed in "Efficient Certified RAT Verification" +; Link: https://www.cs.utexas.edu/~marijn/publications/lrat.pdf ; Author: aozdemir ; Depends On: sat.plf, smt.plf @@ -504,7 +505,7 @@ ; Goes through a list of clause, trace pairs and verifies that each clause is ; an AT via that trace. ; Fails if any putative AT is a TAUT or contains duplicates -(program are_all_at ( +(program are_all_at_trace ( (cs CMap) (l CTPairs) ) UPResult @@ -514,12 +515,12 @@ (match (is_at_trace cs c t) (UPR_Ok UPR_Ok) (UPR_Broken UPR_Broken) - (UPR_Bottom (are_all_at cs l')))))) + (UPR_Bottom (are_all_at_trace cs l')))))) ; Is this trace, and list of hints, proof that `c` is an Resolution Assymeytic ; Tautology? -; Fails is the hints are empty (i.e. `c` should be AT, and c is TAUT or contains duplicates) -; Also fails if any of the pseudo-resolvants are TAUT or contain duplicates. +; Fails is the hints are empty (which means `c` should be AT) and `c` contains +; duplicates) (program is_rat_trace ((cs CMap) (c clause) (t Trace) (hints RATHints)) UPResult (match (RATHints_is_empty hints) @@ -529,10 +530,10 @@ (match (resolution_targets_match (collect_resolution_targets cs c) hints) - (ff ; Res targets are bad + (ff ; Resolution targets disagree with hints. UPR_Broken) (tt - (are_all_at cs (construct_ct_pairs cs c t hints))))))) + (are_all_at_trace cs (construct_ct_pairs cs c t hints))))))) ; Is this proof an LRAT proof of bottom? ; Fails if any added AT is a TAUT or contains duplicates OR if any added RAT