DRAT-trim
From MaRDI portal
Software:25228
swMATH13313MaRDI QIDQ25228FDOQ25228
Author name not available (Why is that?)
Cited In (51)
- Combining SAT solvers with computer algebra systems to verify combinatorial conjectures
- Flexible proof production in an industrial-strength SMT solver
- Two disjoint 5-holes in point sets
- CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver
- Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points
- A proof system for graph (non)-isomorphism verification
- Computing the Ramsey number \(R(4,3,3)\) using abstraction and symmetry breaking
- ProCount: weighted projected model counting with graded project-join trees
- Guiding high-performance SAT solvers with unsat-core predictions
- Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
- Efficient verified (UN)SAT certificate checking
- Inconsistency Proofs for ASP: The ASP - DRUPE Format
- Proof checking and logic programming
- Title not available (Why is that?)
- Local Negative Circuits and Cyclic Attractors in Boolean Networks with at most Five Components
- Simulating strong practical proof systems with extended resolution
- Preprocessing of propagation redundant clauses
- DRAT-based bit-vector proofs in CVC4
- Investigating the existence of large sets of idempotent quasigroups via satisfiability testing
- Efficient certified RAT verification
- Compositional Propositional Proofs
- Machine learning-based restart policy for CDCL SAT solvers
- Nonexistence Certificates for Ovals in a Projective Plane of Order Ten
- On crossing-families in planar point sets
- Title not available (Why is that?)
- A Safe Computational Framework for Integer Programming Applied to Chvátal’s Conjecture
- A computational status update for exact rational mixed integer programming
- Title not available (Why is that?)
- An Expressive Model for Instance Decomposition Based Parallel SAT Solvers
- Expressing Symmetry Breaking in DRAT Proofs
- The resolution of Keller's conjecture
- The resolution of Keller's conjecture
- The reflective Milawa theorem prover is sound (down to the machine code that runs it)
- A computational status update for exact rational mixed integer programming
- Title not available (Why is that?)
- \({\textsf{QRAT}}^{+}\): generalizing QRAT by a more powerful QBF redundancy property
- Extended resolution simulates \({\mathsf{DRAT}}\)
- Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning
- A nonexistence certificate for projective planes of order ten with weight 15 codewords
- Strong extension-free proof systems
- A little blocked literal goes a long way
- Solution validation and extraction for QBF preprocessing
- CrystalBall: gazing in the black box of SAT solving
- Verifying integer programming results
- Efficient, verified checking of propositional proofs
- Proof Checking and Logic Programming
- DRAT Proofs for XOR Reasoning
- QMaxSATpb: a certified MaxSAT solver
- A semantic framework for proof evidence
- Truth Assignments as Conditional Autarkies
- SAT competition 2020
This page was built for software: DRAT-trim
