DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
From MaRDI portal
Publication:3192088
DOI10.1007/978-3-319-09284-3_31zbMath1423.68475OpenAlexW134339645MaRDI QIDQ3192088
Marijn J. H. Heule, Warren A. jun. Hunt, Nathan D. Wetzler
Publication date: 26 September 2014
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-319-09284-3_31
Related Items
Combining SAT solvers with computer algebra systems to verify combinatorial conjectures ⋮ A Safe Computational Framework for Integer Programming Applied to Chvátal’s Conjecture ⋮ A proof system for graph (non)-isomorphism verification ⋮ On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers ⋮ Solution validation and extraction for QBF preprocessing ⋮ Two disjoint 5-holes in point sets ⋮ Nonexistence Certificates for Ovals in a Projective Plane of Order Ten ⋮ The reflective Milawa theorem prover is sound (down to the machine code that runs it) ⋮ CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver ⋮ Proof checking and logic programming ⋮ Expressing Symmetry Breaking in DRAT Proofs ⋮ On crossing-families in planar point sets ⋮ Computing the Ramsey number \(R(4,3,3)\) using abstraction and symmetry breaking ⋮ Unnamed Item ⋮ Efficient, verified checking of propositional proofs ⋮ Generating Extended Resolution Proofs with a BDD-Based SAT Solver ⋮ Inconsistency Proofs for ASP: The ASP - DRUPE Format ⋮ Towards Uniform Certification in QBF ⋮ Formal methods for NFA equivalence: QBFs, witness extraction, and encoding verification ⋮ Unnamed Item ⋮ An Expressive Model for Instance Decomposition Based Parallel SAT Solvers ⋮ Safe and Verified Gomory Mixed-Integer Cuts in a Rational Mixed-Integer Program Framework ⋮ A semantic framework for proof evidence ⋮ QMaxSATpb: a certified MaxSAT solver ⋮ Simulating strong practical proof systems with extended resolution ⋮ Unnamed Item ⋮ Resolution proof transformation for compression and interpolation ⋮ Local Negative Circuits and Cyclic Attractors in Boolean Networks with at most Five Components ⋮ Truth Assignments as Conditional Autarkies ⋮ \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML ⋮ Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points ⋮ Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning ⋮ Proof Checking and Logic Programming ⋮ Preprocessing of propagation redundant clauses ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Functional Encryption for Inner Product with Full Function Privacy ⋮ A computational status update for exact rational mixed integer programming ⋮ The resolution of Keller's conjecture ⋮ Generating extended resolution proofs with a BDD-based SAT solver ⋮ A computational status update for exact rational mixed integer programming ⋮ Efficient verified (UN)SAT certificate checking ⋮ Strong extension-free proof systems ⋮ Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer ⋮ Non-clausal redundancy properties ⋮ DRAT-trim ⋮ SAT competition 2020 ⋮ DRAT Proofs for XOR Reasoning ⋮ A nonexistence certificate for projective planes of order ten with weight 15 codewords ⋮ The resolution of Keller's conjecture ⋮ Preprocessing of propagation redundant clauses ⋮ ProCount: weighted projected model counting with graded project-join trees ⋮ The \textsc{MergeSat} solver
Uses Software
