First interactive protocol for Davis-Putnam resolution that is competitive with BDD methods for certifying UNSAT.
Title resolution pending
4 Pith papers cite this work. Polarity classification is still indexing.
4
Pith papers citing it
fields
cs.LO 4verdicts
UNVERDICTED 4representative citing papers
New ERCL algorithm using dual implication points in CDCL SAT solvers shows performance gains over baselines on Tseitin and XORified formulas.
The Confluence Framework provides a modular strategy to automatically prove and disprove confluence for a broad class of generalized term rewriting systems.
Extends decision procedure for L_|.| to L_[ ] with finite integer intervals, implemented in {log} and applied to discharge invariance lemmas in an elevator algorithm case study.
citing papers explorer
-
A Resolution-Based Interactive Proof System for UNSAT
First interactive protocol for Davis-Putnam resolution that is competitive with BDD methods for certifying UNSAT.
-
Extended Resolution Clause Learning via Dual Implication Points
New ERCL algorithm using dual implication points in CDCL SAT solvers shows performance gains over baselines on Tseitin and XORified formulas.
-
Proving Confluence in the Confluence Framework with CONFident
The Confluence Framework provides a modular strategy to automatically prove and disprove confluence for a broad class of generalized term rewriting systems.
-
A Decision Procedure for a Theory of Finite Sets with Finite Integer Intervals
Extends decision procedure for L_|.| to L_[ ] with finite integer intervals, implemented in {log} and applied to discharge invariance lemmas in an elevator algorithm case study.