Many hard examples for resolution
From MaRDI portal
Publication:3496310
DOI10.1145/48014.48016zbMath0712.03008OpenAlexW2126420408WikidataQ59699144 ScholiaQ59699144MaRDI QIDQ3496310
Publication date: 1988
Published in: Journal of the ACM (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1145/48014.48016
Analysis of algorithms and problem complexity (68Q25) Mechanization of proofs and logical operations (03B35)
Related Items (94)
Complete on average Boolean satisfiability ⋮ From Small Space to Small Width in Resolution ⋮ Narrow Proofs May Be Maximally Long ⋮ Kolmogorov complexity based upper bounds for the unsatisfiability threshold of random k-SAT ⋮ Witnesses for Answer Sets of Logic Programs ⋮ Random \( \Theta (\log n) \) -CNFs are Hard for Cutting Planes ⋮ A lower bound for tree resolution ⋮ Many hard examples in exact phase transitions ⋮ Mutilated chessboard problem is exponentially hard for resolution ⋮ An improved upper bound on the non-3-colourability threshold ⋮ A sharp threshold in proof complexity yields lower bounds for satisfiability search ⋮ Vašek Chvátal: a very short introduction (on the occasion of his 60th birthday) ⋮ Cumulative Space in Black-White Pebbling and Resolution ⋮ Width versus size in resolution proofs ⋮ Davis-Putnam resolution versus unrestricted resolution ⋮ An average case analysis of a resolution principle algorithm in mechanical theorem proving. ⋮ DP-Complete Problems Derived from Extremal NP-Complete Properties ⋮ The state of SAT ⋮ Graph decompositions and tree automata in reasoning with uncertainty ⋮ Regular random \(k\)-SAT: Properties of balanced formulas ⋮ Almost all graphs with 1.44n edges are 3-colorable ⋮ A general model and thresholds for random constraint satisfaction problems ⋮ Heuristic average-case analysis of the backtrack resolution of random 3-satisfiability instances ⋮ Simplified lower bounds for propositional proofs ⋮ Proof complexity in algebraic systems and bounded depth Frege systems with modular counting ⋮ Some computational aspects of DISTANCE SAT ⋮ Space Complexity in Polynomial Calculus ⋮ Generating hard satisfiability problems ⋮ Experimental results on the crossover point in random 3-SAT ⋮ Hard random 3-SAT problems and the Davis-Putnam procedure ⋮ Implicates and prime implicates in random 3-SAT ⋮ Why adiabatic quantum annealing is unlikely to yield speed-up ⋮ The impact of heterogeneity and geometry on the proof complexity of random satisfiability ⋮ Biased random k‐SAT ⋮ Towards NP-P via proof complexity and search ⋮ Resolution lower bounds for the weak functional pigeonhole principle. ⋮ Clause trees: A tool for understanding and implementing resolution in automated reasoning ⋮ A spectral technique for random satisfiable 3CNF formulas ⋮ Irreducible subcube partitions ⋮ On good algorithms for determining unsatisfiability of propositional formulas ⋮ On the structure of some classes of minimal unsatisfiable formulas ⋮ Lower bounds for \(k\)-DNF resolution on random 3-CNFs ⋮ A feasibly constructive lower bound for resolution proofs ⋮ Probabilistic bounds and algorithms for the maximum satisfiability problem ⋮ The \(Multi\)-SAT algorithm ⋮ The symmetry rule in propositional logic ⋮ An Introduction to Lower Bounds on Resolution Proof Systems ⋮ The scaling window of the 2-SAT transition ⋮ Unrestricted resolution versus N-resolution ⋮ Meta-resolution: An algorithmic formalisation ⋮ Captain Jack: New Variable Selection Heuristics in Local Search for SAT ⋮ On Minimal Unsatisfiability and Time-Space Trade-offs for k-DNF Resolution ⋮ Tseitin's formulas revisited ⋮ Counting truth assignments of formulas of bounded tree-width or clique-width ⋮ A combinatorial characterization of resolution width ⋮ Construction of expanders and superconcentrators using Kolmogorov complexity ⋮ A sharp threshold for the phase transition of a restricted satisfiability problem for Horn clauses ⋮ Space proof complexity for random 3-CNFs ⋮ An Upper Bound on the Space Complexity of Random Formulae in Resolution ⋮ Limitations of restricted branching in clause learning ⋮ Testing satisfiability of CNF formulas by computing a stable set of points ⋮ Restarts and exponential acceleration of the Davis-Putnam-Loveland-Logemann algorithm: A large deviation analysis of the generalized unit clause heuristic for random 3-SAT ⋮ Unnamed Item ⋮ The Complexity of Propositional Proofs ⋮ Sharp thresholds for constraint satisfaction problems and homomorphisms ⋮ Upper bounds on the satisfiability threshold ⋮ Frozen development in graph coloring ⋮ A Framework for Space Complexity in Algebraic Proof Systems ⋮ Parameterized Complexity of DPLL Search Procedures ⋮ Short propositional refutations for dense random 3CNF formulas ⋮ A threshold for unsatisfiability ⋮ Supercritical Space-Width Trade-offs for Resolution ⋮ A combinatorial characterization of treelike resolution space ⋮ On the Hardness of SAT with Community Structure ⋮ Trade-offs Between Time and Memory in a Tighter Model of CDCL SAT Solvers ⋮ Propositional proof complexity ⋮ A Tutorial on Time and Space Bounds in Tree-Like Resolution ⋮ Random resolution refutations ⋮ The solution space geometry of random linear equations ⋮ On the relation among answer set solvers ⋮ Exact thresholds for DPLL on random XOR-SAT and NP-complete extensions of XOR-SAT ⋮ The probabilistic analysis of a greedy satisfiability algorithm ⋮ An exponential lower bound for the size of monotone real circuits ⋮ When does the giant component bring unsatisfiability? ⋮ On the relations between SAT and CSP enumerative algorithms ⋮ Space bounds for resolution ⋮ Lower bounds for the weak pigeonhole principle and random formulas beyond resolution ⋮ The resolution complexity of random graph \(k\)-colorability ⋮ Typical case complexity of satisfiability algorithms and the threshold phenomenon ⋮ An efficient local search method for random 3-satisfiability ⋮ A perspective on certain polynomial-time solvable classes of satisfiability ⋮ Spines of random constraint satisfaction problems: definition and connection with computational complexity ⋮ Reflections on Proof Complexity and Counting Principles ⋮ Solving non-uniform planted and filtered random SAT formulas greedily
This page was built for publication: Many hard examples for resolution
