The following pages link to DRAT-trim (Q25228):
Displaying 23 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)
- (Q5875431) (← links)
- A proof system for graph (non)-isomorphism verification (Q5883756) (← links)
