The following pages link to DRAT-trim (Q25228):
Displaying 50 items.
- The reflective Milawa theorem prover is sound (down to the machine code that runs it) (Q286790) (← links)
- Fast formal proof of the Erdős-Szekeres conjecture for convex polygons with at most 6 points (Q670696) (← links)
- Conflict resolution: a first-order resolution calculus with decision literals and conflict-driven clause learning (Q682374) (← links)
- A nonexistence certificate for projective planes of order ten with weight 15 codewords (Q780361) (← links)
- Two disjoint 5-holes in point sets (Q827302) (← links)
- CoqQFBV: a scalable certified SMT quantifier-free bit-vector solver (Q832260) (← links)
- Machine learning-based restart policy for CDCL SAT solvers (Q1656568) (← links)
- A little blocked literal goes a long way (Q1680260) (← links)
- Efficient, verified checking of propositional proofs (Q1687744) (← links)
- A semantic framework for proof evidence (Q1701039) (← links)
- \({\textsf{QRAT}}^{+}\): generalizing QRAT by a more powerful QBF redundancy property (Q1799077) (← links)
- Investigating the existence of large sets of idempotent quasigroups via satisfiability testing (Q1799096) (← links)
- Extended resolution simulates \({\mathsf{DRAT}}\) (Q1799112) (← links)
- SAT competition 2020 (Q2060693) (← links)
- Flexible proof production in an industrial-strength SMT solver (Q2104495) (← links)
- Preprocessing of propagation redundant clauses (Q2104502) (← links)
- ProCount: weighted projected model counting with graded project-join trees (Q2118296) (← links)
- On crossing-families in planar point sets (Q2144455) (← links)
- DRAT-based bit-vector proofs in CVC4 (Q2181940) (← links)
- Guiding high-performance SAT solvers with unsat-core predictions (Q2181943) (← links)
- CrystalBall: gazing in the black box of SAT solving (Q2181946) (← links)
- Simulating strong practical proof systems with extended resolution (Q2209554) (← links)
- Strong extension-free proof systems (Q2303251) (← links)
- Combining SAT solvers with computer algebra systems to verify combinatorial conjectures (Q2360872) (← links)
- Solution validation and extraction for QBF preprocessing (Q2362496) (← links)
- Computing the Ramsey number \(R(4,3,3)\) using abstraction and symmetry breaking (Q2398438) (← links)
- Verifying integer programming results (Q2401153) (← links)
- Efficient certified RAT verification (Q2405252) (← links)
- Proof checking and logic programming (Q2628296) (← links)
- QMaxSATpb: a certified MaxSAT solver (Q2694600) (← links)
- Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer (Q2818017) (← links)
- DRAT Proofs for XOR Reasoning (Q2835888) (← links)
- An Expressive Model for Instance Decomposition Based Parallel SAT Solvers (Q2964456) (← links)
- Truth Assignments as Conditional Autarkies (Q3297584) (← links)
- Expressing Symmetry Breaking in DRAT Proofs (Q3454124) (← links)
- Compositional Propositional Proofs (Q3460074) (← links)
- (Q4553279) (← links)
- Local Negative Circuits and Cyclic Attractors in Boolean Networks with at most Five Components (Q4631519) (← links)
- (Q4989407) (← links)
- Nonexistence Certificates for Ovals in a Projective Plane of Order Ten (Q5041183) (← links)
- (Q5094131) (← links)
- Inconsistency Proofs for ASP: The ASP - DRUPE Format (Q5108508) (← links)
- Proof Checking and Logic Programming (Q5743582) (← links)
- (Q5875431) (← links)
- A Safe Computational Framework for Integer Programming Applied to Chvátal’s Conjecture (Q5883707) (← links)
- A proof system for graph (non)-isomorphism verification (Q5883756) (← links)
- A computational status update for exact rational mixed integer programming (Q5918427) (← links)
- The resolution of Keller's conjecture (Q5918545) (← links)
- Efficient verified (UN)SAT certificate checking (Q5919480) (← links)
- A computational status update for exact rational mixed integer programming (Q5925645) (← links)
