Finding a tree structure in a resolution proof is NP-complete (Q1019749): Difference between revisions

@@ Property / cites work @@
+Minimum propositional proof length is NP-hard to linearly approximate
+Normal rank
@@ Property / cites work @@
+Q3002781
@@ Property / cites work: Q3002781 / rank @@
+Normal rank
@@ Property / cites work @@
+Resolution Is Not Automatizable Unless W[P] Is Tractable
+Normal rank
@@ Property / cites work @@
+Near optimal seperation of tree-like and general resolution
+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 @@
+The NP-hardness of finding a directed acyclic graph for regular resolution
+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 @@
+The intractability of resolution
@@ Property / cites work: The intractability of resolution / rank @@
+Normal rank
@@ Property / cites work @@
+Q4699307
@@ Property / cites work: Q4699307 / rank @@
+Normal rank
@@ Property / cites work @@
+Reducibility Among Combinatorial Problems
@@ Property / cites work: Reducibility Among Combinatorial Problems / rank @@
+Normal rank
@@ Property / cites work @@
+Q5593816
@@ Property / cites work: Q5593816 / rank @@
+Normal rank