diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2019-06-05 12:16:46 -0700 |
|---|---|---|
| committer | Andres Noetzli <noetzli@stanford.edu> | 2019-06-05 12:16:46 -0700 |
| commit | 9af5e9653582a18b1871dfc3774ab50dd24463ce (patch) | |
| tree | 9bbe5cd5708dbd3475626cabd4d2c9711f0ac133 /proofs/signatures | |
| parent | c587235d29d2e3e1cd52a9f76dde8f58c89ae37e (diff) | |
DRAT-Optimization (#2971)
This commit enables DRAT-optimization, which consists of two sub-processes:
1. removing unnecessary instructions from DRAT-proofs and
2. not proving clauses which are not needed by DRAT proofs.
These changes have the effect of dramatically shortening some some bit-vector proofs. Specifically, proofs using lemmas in the ER, DRAT, and LRAT formats, since proofs in any of these formats are derived from a (now optimized!) DRAT proof produced by CryptoMiniSat. What follows is a description of the main parts of this PR:
## DRAT Optimization
The DRAT-optimization is done by `drat-trim`, which is bundled with `drat2er`. The (new) function `ClausalBitVectorProof::optimizeDratProof` is our interface to the optimization machinery, and most of the new logic in this PR is in that function.
## CNF Representation
The ability to not prove unused clauses requires a slight architectural change as well. In particular, we need to be able to describe **which** subset of the original clause set actually needs to be proved. To facilitate this, when the clause set for CryptoMiniSat is first formed it is represented as a (a) map from clause indices to clauses and (b) a list of indices. Then, when the CNF is optimized, we temporarily store a new list of the clauses in the optimized formula. This change in representation requires a number of small tweaks throughout the code.
## Small Fixes to Signatures
When we decided to check and accept two different kinds of DRAT, some of our DRAT-checking broke. In particular, when supporting one kind of DRAT, it is okay to `fail` (crash) when a proof fails to check. If you're supporting two kinds of DRAT, crashing in response to the first checker rejecting the proof denies the second checker an opportunity to check the proof. This PR tweaks the signatures slightly (and soundly!) to do something else instead of `fail`ing.
Diffstat (limited to 'proofs/signatures')
| -rw-r--r-- | proofs/signatures/drat.plf | 9 | ||||
| -rw-r--r-- | proofs/signatures/lrat.plf | 4 |
2 files changed, 8 insertions, 5 deletions
diff --git a/proofs/signatures/drat.plf b/proofs/signatures/drat.plf index d0f647452..fa7ca3055 100644 --- a/proofs/signatures/drat.plf +++ b/proofs/signatures/drat.plf @@ -113,9 +113,10 @@ ((clc l c') (cnf_has_bottom rest)))))) ; Return a new cnf with one copy of this clause removed. +; If the clause is absent, returns the original cnf. (program cnf_remove_clause ((c clause) (cs cnf)) cnf (match cs - (cnfn (fail cnf)) + (cnfn cnfn) ((cnfc c' cs') (match (clause_eq c c') (tt cs') @@ -224,9 +225,11 @@ (tt tt) (ff (match (is_at cs c) (tt tt) - (ff (are_all_at + (ff (match c + (cln ff) + ((clc a b) (are_all_at ; dedent cs - (collect_pseudo_resolvents cs c))))))) + (collect_pseudo_resolvents cs c))))))))) ; Is this proof a valid DRAT proof of bottom? (program is_specified_drat_proof ((f cnf) (proof DRATProof)) bool diff --git a/proofs/signatures/lrat.plf b/proofs/signatures/lrat.plf index ea1d90537..d16791624 100644 --- a/proofs/signatures/lrat.plf +++ b/proofs/signatures/lrat.plf @@ -361,14 +361,14 @@ ; unit, it modifies the global assignment to satisfy the clause, and returns ; the literal that was made SAT by the new mark. ; -; Fails if `c` is a TAUT +; If `c` is a tautology, reports `MRSat`, since it is (trivially) satisfied. (program clause_check_unit_and_maybe_mark ((c clause)) MarkResult (match (clause_is_sat c) (tt MRSat) (ff (match (clause_is_unsat c) (tt MRUnsat) (ff (match (is_t c) - (tt (fail MarkResult)) + (tt MRSat) (ff ; Dedent (match (clause_has_floating c) (tt (let first (clause_first_floating c) |