On the power of clause-learning SAT solvers as resolution engines (Q543613): Difference between revisions

@@ Property / cites work @@
+Clause-Learning Algorithms with Many Restarts and Bounded-Width Resolution
+Normal rank
@@ Property / cites work @@
+A Generalized Framework for Conflict Analysis
@@ Property / cites work: A Generalized Framework for Conflict Analysis / rank @@
+Normal rank
@@ Property / cites work @@
+Q5715680
@@ Property / cites work: Q5715680 / rank @@
+Normal rank
@@ Property / cites work @@
+Short proofs are narrow—resolution made simple
@@ Property / cites work: Short proofs are narrow—resolution made simple / rank @@
+Normal rank
@@ Property / cites work @@
+Resolution Trees with Lemmas: Resolution Refinements that Characterize DLL Algorithms with Clause Learning
+Normal rank
@@ Property / cites work @@
+The relative efficiency of propositional proof systems
+Normal rank
@@ Property / cites work @@
+A machine program for theorem-proving
@@ Property / cites work: A machine program for theorem-proving / rank @@
+Normal rank
@@ Property / cites work @@
+Theory and Applications of Satisfiability Testing
@@ Property / cites work: Theory and Applications of Satisfiability Testing / rank @@
+Normal rank
@@ Property / cites work @@
+BerkMin: A fast and robust SAT-solver
@@ Property / cites work: BerkMin: A fast and robust SAT-solver / rank @@
+Normal rank
@@ Property / cites work @@
+Optimal speedup of Las Vegas algorithms
@@ Property / cites work: Optimal speedup of Las Vegas algorithms / rank @@
+Normal rank
@@ Property / cites work @@
+Theory and Applications of Satisfiability Testing
@@ Property / cites work: Theory and Applications of Satisfiability Testing / rank @@
+Normal rank
@@ Property / cites work @@
+A Machine-Oriented Logic Based on the Resolution Principle
+Normal rank
@@ Property / cites work @@
+Theory and Applications of Satisfiability Testing
@@ Property / cites work: Theory and Applications of Satisfiability Testing / rank @@
+Normal rank
@@ Property / cites work @@
+Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning
+Normal rank