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

@@ Property / describes a project that uses @@
+RSat
@@ Property / describes a project that uses: RSat / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Siege
@@ Property / describes a project that uses: Siege / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Zchaff2004
@@ Property / describes a project that uses: Zchaff2004 / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+BerkMin
@@ Property / describes a project that uses: BerkMin / rank @@
+Normal rank
@@ Property / describes a project that uses @@
+Eureka
@@ Property / describes a project that uses: Eureka / rank @@
+Normal rank
@@ Property / MaRDI profile type @@
+MaRDI publication profile
@@ Property / MaRDI profile type: MaRDI publication profile / rank @@
+Normal rank
@@ Property / full work available at URL @@
+https://doi.org/10.1016/j.artint.2010.10.002
+Normal rank
@@ Property / OpenAlex ID @@
+W2121015471
@@ Property / OpenAlex ID: W2121015471 / rank @@
+Normal rank
@@ 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