Many hard examples for resolution
From MaRDI portal
Publication:3496310
DOI10.1145/48014.48016zbMath0712.03008OpenAlexW2126420408WikidataQ59699144 ScholiaQ59699144MaRDI QIDQ3496310
Endre Szemerédi, Vašek Chvátal
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
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
