Simulating strong practical proof systems with extended resolution (Q2209554): Difference between revisions

@@ Property / describes a project that uses @@
+DRAT-trim
@@ Property / describes a project that uses: DRAT-trim / 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.1007/s10817-020-09554-z
+Normal rank
@@ Property / OpenAlex ID @@
+W3046591311
@@ Property / OpenAlex ID: W3046591311 / rank @@
+Normal rank
@@ Property / cites work @@
+Mutilated chessboard problem is exponentially hard for resolution
+Normal rank
@@ Property / cites work @@
+Methods of cut-elimination
@@ Property / cites work: Methods of cut-elimination / rank @@
+Normal rank
@@ Property / cites work @@
+The relative efficiency of propositional proof systems
+Normal rank
@@ Property / cites work @@
+Efficient certified RAT verification
@@ Property / cites work: Efficient certified RAT verification / rank @@
+Normal rank
@@ Property / cites work @@
+The intractability of resolution
@@ Property / cites work: The intractability of resolution / 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 @@
+Solving and Verifying the Boolean Pythagorean Triples Problem via Cube-and-Conquer
+Normal rank
@@ Property / cites work @@
+Efficient, verified checking of propositional proofs
+Normal rank
@@ Property / cites work @@
+Short proofs without new variables
@@ Property / cites work: Short proofs without new variables / rank @@
+Normal rank
@@ Property / cites work @@
+Strong extension-free proof systems
@@ Property / cites work: Strong extension-free proof systems / rank @@
+Normal rank
@@ Property / cites work @@
+Blocked Clause Elimination
@@ Property / cites work: Blocked Clause Elimination / rank @@
+Normal rank
@@ Property / cites work @@
+Inprocessing Rules
@@ Property / cites work: Inprocessing Rules / rank @@
+Normal rank
@@ Property / cites work @@
+Extended Resolution Proofs for Symbolic SAT Solving with Quantification
+Normal rank
@@ Property / cites work @@
+Extended resolution simulates \({\mathsf{DRAT}}\)
@@ Property / cites work: Extended resolution simulates \({\mathsf{DRAT}}\) / rank @@
+Normal rank
@@ Property / cites work @@
+Computer-aided proof of Erdős discrepancy properties
+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 @@
+GRASP: a search algorithm for propositional satisfiability
+Normal rank
@@ Property / cites work @@
+Towards a Semantics of Unsatisfiability Proofs with Inprocessing
+Normal rank
@@ Property / cites work @@
+A Theory of Satisfiability-Preserving Proofs in SAT Solving
+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 @@
+Q5604434
@@ Property / cites work: Q5604434 / rank @@
+Normal rank
@@ Property / cites work @@
+Hard examples for resolution
@@ Property / cites work: Hard examples for resolution / rank @@
+Normal rank
@@ Property / cites work @@
+The Complexity of Propositional                                                   Proofs
@@ Property / cites work: The Complexity of Propositional Proofs / rank @@
+Normal rank
@@ Property / cites work @@
+Producing and verifying extremely large propositional refutations
+Normal rank
@@ Property / cites work @@
+DRAT-trim: Efficient Checking and Trimming Using Expressive Clausal Proofs
+Normal rank