DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
From MaRDI portal
Recommendations
- Efficient, verified checking of propositional proofs
- Efficiently checking propositional refutations in HOL theorem provers
- scientific article; zbMATH DE number 140415
- Towards Verifying Logic Programs in the Input Language of clingo
- A Sound and Complete Deductive System for CTL* Verification
- scientific article; zbMATH DE number 1770113
- Verifying and Reflecting Quantifier Elimination for Presburger Arithmetic
Cited in
(83)- Efficient, verified checking of propositional proofs
- A semantic framework for proof evidence
- A flexible proof format for SAT solver-elaborator communication
- Generating extended resolution proofs with a BDD-based SAT solver
- Non-clausal redundancy properties
- SAT competition 2020
- Preprocessing of propagation redundant clauses
- ProCount: weighted projected model counting with graded project-join trees
- The \textsc{MergeSat} solver
- On crossing-families in planar point sets
- Simulating strong practical proof systems with extended resolution
- \texttt{cake\_lpr}: verified propagation redundancy checking in CakeML
- Strong extension-free proof systems
- Combining SAT solvers with computer algebra systems to verify combinatorial conjectures
- Solution validation and extraction for QBF preprocessing
- Computing the Ramsey number \(R(4,3,3)\) using abstraction and symmetry breaking
- Efficient certified RAT verification
- DRAT-trim
- Proof checking and logic programming
- QMaxSATpb: a certified MaxSAT solver
- Functional encryption for inner product with full function privacy
- Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
- DRAT proofs for XOR reasoning
- The reflective Milawa theorem prover is sound (down to the machine code that runs it)
- An expressive model for instance decomposition based parallel SAT solvers
- Truth assignments as conditional autarkies
- Expressing symmetry breaking in DRAT proofs
- Local redundancy in SAT: generalizations of blocked clauses
- Local negative circuits and cyclic attractors in Boolean networks with at most five components
- Resolution proof transformation for compression and interpolation
- DRAT and propagation redundancy proofs without new variables
- Nonexistence Certificates for Ovals in a Projective Plane of Order Ten
- A flexible proof format for SAT solver-elaborator communication
- Inconsistency proofs for ASP: the ASP-DRUPE format
- Proof checking and logic programming
- scientific article; zbMATH DE number 7649971 (Why is no real title available?)
- A Safe Computational Framework for Integer Programming Applied to Chvátal’s Conjecture
- A proof system for graph (non)-isomorphism verification
- A computational status update for exact rational mixed integer programming
- The resolution of Keller's conjecture
- Efficient verified (UN)SAT certificate checking
- A computational status update for exact rational mixed integer programming
- The resolution of Keller's conjecture
- Preprocessing of propagation redundant clauses
- Generating Extended Resolution Proofs with a BDD-Based SAT Solver
- Towards Uniform Certification in QBF
- Formal methods for NFA equivalence: QBFs, witness extraction, and encoding verification
- A SAT attack on Erdős-Szekeres numbers in \(\mathbb{R}^d\) and the empty hexagon theorem
- Safe and Verified Gomory Mixed-Integer Cuts in a Rational Mixed-Integer Program Framework
- Certified dominance and symmetry breaking for combinatorial optimisation
- A More Pragmatic CDCL for IsaSAT and Targetting LLVM (Short Paper)
- Propositional proof skeletons
- Solving string constraints using SAT
- Clausal proofs for pseudo-Boolean reasoning
- Moving definition variables in quantified Boolean formulas
- Certified SAT solving with GPU accelerated inprocessing
- A SAT attack on higher dimensional Erdős-Szekeres numbers
- On disjoint holes in point sets
- 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
- Formal verification of the empty hexagon number
- A formal proof of R(4,5)=25
- The strength of the dominance rule
- Clausal congruence closure
- The relative strength of \#SAT proof systems
- Interoperability of proof systems with SC-TPTP
- Computing and certifying twin-width using logic
- Runtime vs. extracted proof size: an exponential gap for CDCL on QBFs
- ICCMA 2023: 5th international competition on computational models of argumentation
- RAT elimination
- Fast and verified UNSAT certificate checking
- Certified MaxSAT preprocessing
- Circuits, proofs and propositional model counting
- North-east lattice paths avoiding k collinear points via satisfiability
- The relative strength of \#SAT proof systems
- PLS-completeness of string permutations
- Swap Distance
- The Incompatibility of Strategy-Proofness and Representation in Party-Approval Multi-Winner Elections
- The Impossibility of Strategyproof Rank Aggregation
- A nonexistence certificate for projective planes of order ten with weight 15 codewords
- On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers
- Two disjoint 5-holes in point sets
- CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver
This page was built for publication: DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3192088)
