Automating Resolution is NP-Hard
From MaRDI portal
Publication:5133983
DOI10.1145/3409472zbMath1491.68078arXiv1904.02991OpenAlexW3081705035MaRDI QIDQ5133983
Albert Atserias, Moritz Müller
Publication date: 11 November 2020
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1904.02991
Mechanization of proofs and logical operations (03B35) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Complexity of proofs (03F20)
Related Items
On the complexity of finding shortest variable disjunction branch-and-bound proofs, INFORMATION IN PROPOSITIONAL PROOFS AND ALGORITHMIC PROOF SEARCH, Optimal length cutting plane refutations of integer programs, The canonical pairs of bounded depth Frege systems, Unnamed Item, Propositional proof complexity, Bounded-depth Frege complexity of Tseitin formulas for all graphs, Theorem proving as constraint solving with coherent logic, Large clique is hard on average for resolution
