The intractability of resolution
From MaRDI portal
Publication:1071750
DOI10.1016/0304-3975(85)90144-6zbMath0586.03010OpenAlexW2069767473WikidataQ56224983 ScholiaQ56224983MaRDI QIDQ1071750
Publication date: 1985
Published in: Theoretical Computer Science (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0304-3975(85)90144-6
propositional logicexponential lower boundextended resolutionpigeonhole principlecomplexity of general resolutiontautology problem
Analysis of algorithms and problem complexity (68Q25) Mechanization of proofs and logical operations (03B35) Complexity of computation (including implicit computational complexity) (03D15) Classical propositional logic (03B05) Complexity of proofs (03F20)
Related Items
Conditional term rewriting and first-order theorem proving, From Small Space to Small Width in Resolution, Narrow Proofs May Be Maximally Long, Hardness Characterisations and Size-width Lower Bounds for QBF Resolution, Witnesses for Answer Sets of Logic Programs, 2000 Annual Meeting of the Association for Symbolic Logic, The cost of a cycle is a square, Cumulative Space in Black-White Pebbling and Resolution, Between SAT and UNSAT: The Fundamental Difference in CDCL SAT, Width versus size in resolution proofs, Exact and parameterized algorithms for read-once refutations in Horn constraint systems, Boolean functions as models for quantified Boolean formulas, The state of SAT, Regular-SAT: A many-valued approach to solving combinatorial problems, Propositional proof systems, the consistency of first order theories and the complexity of computations, Lower bounds to the size of constant-depth propositional proofs, A simple proof of QBF hardness, INFORMATION IN PROPOSITIONAL PROOFS AND ALGORITHMIC PROOF SEARCH, Strong ETH and resolution via games and the multiplicity of strategies, Space Complexity in Polynomial Calculus, Simplifying clausal satisfiability problems, A polynomial time algorithm for read-once certification of linear infeasibility in UTVPI constraints, Analyzing read-once cutting plane proofs in Horn systems, Generating hard satisfiability problems, Integer feasibility and refutations in UTVPI constraints using bit-scaling, Polynomial size proofs of the propositional pigeonhole principle, Limitations of Restricted Branching in Clause Learning, Simulating strong practical proof systems with extended resolution, An Upper Bound for Resolution Size: Characterization of Tractable SAT Instances, A characterization of tree-like resolution size, Semidefinite resolution and exactness of semidefinite relaxations for satisfiability, An Introduction to Lower Bounds on Resolution Proof Systems, Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic, Partition-based logical reasoning for first-order and propositional theories, Polynomial time algorithms for optimal length tree-like refutations of linear infeasibility in UTVPI constraints, Copy complexity of Horn formulas with respect to unit read-once resolution, Tautologies from Pseudo-Random Generators, Lower bounds for cutting planes proofs with small coefficients, Lower bounds for resolution and cutting plane proofs and monotone computations, Finding the Hardest Formulas for Resolution, Exponential Lower Bounds for AC0-Frege Imply Superpolynomial Frege Lower Bounds, Parameterized Bounded-Depth Frege Is Not Optimal, Counting truth assignments of formulas of bounded tree-width or clique-width, A combinatorial characterization of resolution width, Extended resolution simulates binary decision diagrams, Upper bounds on complexity of Frege proofs with limited use of certain schemata, The complexity of the Hajós calculus for planar graphs, Asymptotic cyclic expansion and bridge groups of formal proofs, Limitations of restricted branching in clause learning, On propositional coding techniques for the distinguishability of objects in finite sets, Unnamed Item, Unnamed Item, The complexity of resolution refinements, The Complexity of Propositional Proofs, Unnamed Item, Exploiting Symmetry in SMT Problems, On the correspondence between arithmetic theories and propositional proof systems – a survey, Parameterized Complexity of DPLL Search Procedures, The search efficiency of theorem proving strategies, How many times do we need an assumption to prove a tautology in minimal logic? Examples on the compression power of classical reasoning, Automated Proof-searching for Strong Kleene Logic and its Binary Extensions via Correspondence Analysis, Supercritical Space-Width Trade-offs for Resolution, Proof Complexity of Non-classical Logics, Strong extension-free proof systems, Time-Space Trade-offs in Resolution: Superpolynomial Lower Bounds for Superlinear Space, Satisfiability via Smooth Pictures, Improved Static Symmetry Breaking for SAT, Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers, On Q-Resolution and CDCL QBF Solving, On Stronger Calculi for QBFs, NAE-resolution: A new resolution refutation technique to prove not-all-equal unsatisfiability, A Tutorial on Time and Space Bounds in Tree-Like Resolution, Autonomous Resolution Based on DNA Strand Displacement, Bounded-Resource Reasoning as (Strong or Classical) Planning, $$P\mathop{ =}\limits^{?}NP$$, Resolution and the binary encoding of combinatorial principles, Bounded-Depth Frege Complexity of Tseitin Formulas for All Graphs, A Survey of Satisfiability Modulo Theory, Unnamed Item, Combinatorial Problems for Horn Clauses, LOWER BOUNDS FOR DNF-REFUTATIONS OF A RELATIVIZED WEAK PIGEONHOLE PRINCIPLE, Unnamed Item, Unnamed Item, On the lengths of tree-like and dag-like cutting plane refutations of Horn constraint systems. Horn constraint systems and cutting plane refutations, Covered clauses are not propagation redundant, Typical case complexity of satisfiability algorithms and the threshold phenomenon, On Exponential Lower Bounds for Partially Ordered Resolution, Preprocessing of propagation redundant clauses, Synthetic tableaux: Minimal tableau search heuristics, Comments on: ``An overview of curriculum-based course timetabling, A Logical Autobiography, Reflections on Proof Complexity and Counting Principles, Satisfiability, Lattices, Temporal Logic and Constraint Logic Programming on Intervals, MaxSAT Resolution and Subcube Sums, Large clique is hard on average for resolution, QBFFam: a tool for generating QBF families from proof complexity, Lower bounds for QCDCL via formula gauge, Hardness and optimality in QBF proof systems modulo NP, On dedicated CDCL strategies for PB solvers, MaxSAT resolution for regular propositional logic, Generating Extended Resolution Proofs with a BDD-Based SAT Solver, Circular (Yet Sound) Proofs in Propositional Logic, Number of Variables for Graph Differentiation and the Resolution of Graph Isomorphism Formulas, Understanding the Relative Strength of QBF CDCL Solvers and QBF Resolution, Are hitting formulas hard for resolution?, Unit read-once refutations for systems of difference constraints, Preprocessing of propagation redundant clauses, Lower bounds for QCDCL via formula gauge, Propositional proof complexity, Monotone simulations of non-monotone proofs., On finding short resolution refutations and small unsatisfiable subsets, On certifying the UNSAT result of dynamic symmetry-handling-based SAT solvers, A kind of logical compilation for knowledge bases, On the relative merits of path dissolution and the method of analytic tableaux, Transformation rules for CNOT-based quantum circuits and their applications, A lower bound for tree resolution, Proof complexity of modal resolution, On the complexity of resolution with bounded conjunctions, The complexity of the pigeonhole principle, Proof compressions with circuit-structured substitutions, A new algorithm for the propositional satisfiability problem, Optimal length resolution refutations of difference constraint systems, A proper hierarchy of propositional sequent calculi, A note about \(k\)-DNF resolution, Resolution and the integrality of satisfiability problems, Davis-Putnam resolution versus unrestricted resolution, An average case analysis of a resolution principle algorithm in mechanical theorem proving., Generalized resolution for 0--1 linear inequalities, Resolution vs. cutting plane solution of inference problems: Some computational experience, Cutting planes, connectivity, and threshold logic, Planning as satisfiability: heuristics, Optimizing propositional calculus formulas with regard to questions of deducibility, Proof complexity in algebraic systems and bounded depth Frege systems with modular counting, On resolution with short clauses, A fast parallel SAT-solver -- efficient workload balancing, An exponential separation between the parity principle and the pigeonhole principle, Short resolution proofs for a sequence of tricky formulas, Relativization makes contradictions harder for resolution, Extended clause learning, Towards NP-P via proof complexity and search, Improved bounds on the weak pigeonhole principle and infinitely many primes from weaker axioms, Resolution lower bounds for the weak functional pigeonhole principle., Clause trees: A tool for understanding and implementing resolution in automated reasoning, Improved algorithms for optimal length resolution refutation in difference constraint systems, Resolution and binary decision diagrams cannot simulate each other polynomially, On the structure of some classes of minimal unsatisfiable formulas, Homomorphisms of conjunctive normal forms., A certifying algorithm for lattice point feasibility in a system of UTVPI constraints, Cliques enumeration and tree-like resolution proofs, A feasibly constructive lower bound for resolution proofs, On the automatizability of polynomial calculus, Resolution proofs of generalized pigeonhole principles, Resolution remains hard under equivalence, On a generalization of extended resolution, The symmetry rule in propositional logic, Mixed logical-linear programming, Solving SAT by algorithm transform of Wu's method, A resolution-based decision procedure for \({\mathcal{SHOIQ}}\)., Curriculum-based course timetabling with SAT and MaxSAT, Lifting lower bounds for tree-like proofs, On meta complexity of propositional formulas and propositional proofs, Unrestricted resolution versus N-resolution, The design of the zinc modelling language, Meta-resolution: An algorithmic formalisation, Tractability of cut-free Gentzen type propositional calculus with permutation inference, Tseitin's formulas revisited, Complexity of resolution proofs and function introduction, Resolution over linear equations and multilinear proofs, Finding read-once resolution refutations in systems of 2CNF clauses, Functional interpretations of feasibly constructive arithmetic, Exponential lower bounds for the pigeonhole principle, Cut formulas in propositional logic, Resolution cannot polynomially simulate compressed-BFS, Testing satisfiability of CNF formulas by computing a stable set of points, Extension without cut, On the complexity of cutting-plane proofs, Understanding cutting planes for QBFs, Resolution with counting: dag-like lower bounds and different moduli, Proof complexity of substructural logics, A flexible proof format for SAT solver-elaborator communication, Generating extended resolution proofs with a BDD-based SAT solver, Short propositional refutations for dense random 3CNF formulas, A combinatorial characterization of treelike resolution space, Analyzing unit read-once refutations in difference constraint systems, Tight rank lower bounds for the Sherali-Adams proof system, Finding a tree structure in a resolution proof is NP-complete, Cutting-plane proofs in polynomial space, Good degree bounds on Nullstellensatz refutations of the induction principle, On the relation among answer set solvers, Resolution for Max-SAT, On the Chvátal rank of the pigeonhole principle, On the bottleneck counting argument, On the modelling of search in theorem proving -- towards a theory of strategy analysis, Verifying time, memory and communication bounds in systems of reasoning agents, Learn to relax: integrating \(0-1\) integer linear programming with pseudo-Boolean conflict-driven search, \texttt{SymChaff}: Exploiting symmetry in a structure-aware satisfiability solver, Parameterized and exact algorithms for finding a read-once resolution refutation in 2CNF formulas, An exponential lower bound for the size of monotone real circuits, Tractability of cut-free Gentzen-type propositional calculus with permutation inference. II, Bounded-depth Frege complexity of Tseitin formulas for all graphs, On subclasses of minimal unsatisfiable formulas, Streams and strings in formal proofs., Space bounds for resolution, Lower bounds for the weak pigeonhole principle and random formulas beyond resolution, Simplification in a satisfiability checker for VLSI applications, Unrestricted vs restricted cut in a tableau method for Boolean circuits, Two party immediate response disputes: Properties and efficiency, Proving unsatisfiability of CNFs locally, Group cancellation and resolution
Cites Work
