Generating extended resolution proofs with a BDD-based SAT solver (Q2044191): Difference between revisions

@@ Property / cites work @@
+Mutilated chessboard problem is exponentially hard for resolution
+Normal rank
@@ Property / cites work @@
+Graph-Based Algorithms for Boolean Function Manipulation
+Normal rank
@@ Property / cites work @@
+Binary Decision Diagrams
@@ Property / cites work: Binary Decision Diagrams / rank @@
+Normal rank
@@ Property / cites work @@
+Symbolic model checking: \(10^{20}\) states and beyond
+Normal rank
@@ Property / cites work @@
+Efficient certified RAT verification
@@ Property / cites work: Efficient certified RAT verification / rank @@
+Normal rank
@@ Property / cites work @@
+A Computing Procedure for Quantification Theory
@@ Property / cites work: A Computing Procedure for Quantification Theory / rank @@
+Normal rank
@@ Property / cites work @@
+Bucket elimination: A unifying framework for reasoning
+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 @@
+Resolution and binary decision diagrams cannot simulate each other polynomially
+Normal rank
@@ Property / cites work @@
+The intractability of resolution
@@ Property / cites work: The intractability of resolution / rank @@
+Normal rank
@@ Property / cites work @@
+Q5219922
@@ Property / cites work: Q5219922 / rank @@
+Normal rank
@@ Property / cites work @@
+What a difference a variable makes
@@ Property / cites work: What a difference a variable makes / rank @@
+Normal rank
@@ Property / cites work @@
+Efficient, verified checking of propositional proofs
+Normal rank
@@ Property / cites work @@
+Extended Resolution Proofs for Symbolic SAT Solving with Quantification
+Normal rank
@@ Property / cites work @@
+On a generalization of extended resolution
@@ Property / cites work: On a generalization of extended resolution / rank @@
+Normal rank
@@ Property / cites work @@
+Efficient verified (UN)SAT certificate checking
@@ Property / cites work: Efficient verified (UN)SAT certificate checking / 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 @@
+Towards an Optimal CNF Encoding of Boolean Cardinality Constraints
+Normal rank
@@ Property / cites work @@
+Extended Resolution Proofs for Conjoining BDDs
@@ Property / cites work: Extended Resolution Proofs for Conjoining BDDs / rank @@
+Normal rank
@@ Property / cites work @@
+Q3682462
@@ Property / cites work: Q3682462 / rank @@
+Normal rank
@@ Property / cites work @@
+Ordered Binary Decision Diagrams and the Davis-Putnam procedure
+Normal rank
@@ Property / cites work @@
+DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
+Normal rank