On CDCL-Based Proof Systems with the Ordered Decision Strategy

Complexity of proofs (03F20) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15) Computational aspects of satisfiability (68R07)

Uses Software

Chaff

Cites Work

Unnamed Item
Unnamed Item
Unnamed Item
On the power of clause-learning SAT solvers as resolution engines
Efficient SAT-based bounded model checking for software verification
On CDCL-based proof systems with the ordered decision strategy
Towards a complexity-theoretic understanding of restarts in SAT solvers
On the Relative Complexity of Resolution Refinements and Cutting Planes Proof Systems
The Efficiency of Resolution and Davis--Putnam Procedures
Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers
Pebble Games, Proof Complexity, and Time-Space Trade-offs
Evaluating CDCL Variable Scoring Schemes
Solving SAT and SAT Modulo Theories
Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
Efficiently Calculating Evolutionary Tree Measures Using SAT
The relative efficiency of propositional proof systems
On the Complexity of the Hidden Weighted Bit Function for Various BDD Models
Short proofs are narrow—resolution made simple
GRASP: a search algorithm for propositional satisfiability
Lower Bounds for Width-Restricted Clause Learning on Small Width Formulas
Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning
Improved Separations of Regular Resolution from Clause Learning Proof Systems
Small Stone in Pool
A Machine-Oriented Logic Based on the Resolution Principle
A Computing Procedure for Quantification Theory
A machine program for theorem-proving
Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
Formal Methods for Hardware Verification

This page was built for publication: On CDCL-Based Proof Systems with the Ordered Decision Strategy