Many hard examples for resolution

DOI10.1145/48014.48016MaRDI QIDQ3496310zbMATH OpenOpenAlexWikidataFDO

Authors Vašek Chvátal, Endre Szemerédi

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

zbMATH Keywords

satisfiabilityresolution proofunsatisfiabilitycomplexity of proof procedures

Mathematics Subject Classification ID

Analysis of algorithms and problem complexity (68Q25) Mechanization of proofs and logical operations (03B35)

Recommendations

• On Random 3-sat
• scientific article; zbMATH DE number 1775444
• Random resolution refutations
• A sharp threshold in proof complexity
• The Resolution Complexity of Random Constraint Satisfaction Problems

Cited in

(only showing first 100 items - show all)

• Many hard examples in exact phase transitions
• An Upper Bound on the Space Complexity of Random Formulae in Resolution
• Space bounds for resolution
• The scaling window of the 2-SAT transition
• Captain Jack: new variable selection heuristics in local search for SAT
• A combinatorial characterization of treelike resolution space
• Tseitin's formulas revisited
• scientific article; zbMATH DE number 408796 (Why is no real title available?)
• Reflections on Proof Complexity and Counting Principles
• Generating hard satisfiability problems
• scientific article; zbMATH DE number 7561756 (Why is no real title available?)
• A feasibly constructive lower bound for resolution proofs
• Random \( \Theta (\log n) \) -CNFs are Hard for Cutting Planes
• Towards NP-P via proof complexity and search
• The state of SAT
• On the structure of some classes of minimal unsatisfiable formulas
• Typical case complexity of satisfiability algorithms and the threshold phenomenon
• Unrestricted resolution versus N-resolution
• The Complexity of Propositional Proofs
• A perspective on certain polynomial-time solvable classes of satisfiability
• On good algorithms for determining unsatisfiability of propositional formulas
• Solving non-uniform planted and filtered random SAT formulas greedily
• The impact of heterogeneity and geometry on the proof complexity of random satisfiability
• Limitations of restricted branching in clause learning
• Clause trees: A tool for understanding and implementing resolution in automated reasoning
• Frozen development in graph coloring
• Space proof complexity for random 3-CNFs
• An efficient local search method for random 3-satisfiability
• The symmetry rule in propositional logic
• Vašek Chvátal: a very short introduction (on the occasion of his 60th birthday)
• Sharp thresholds for constraint satisfaction problems and homomorphisms
• A spectral technique for random satisfiable 3CNF formulas
• Parameterized complexity of DPLL search procedures
• Probabilistic bounds and algorithms for the maximum satisfiability problem
• An improved upper bound on the non-3-colourability threshold
• Lower bounds for k-DNF resolution on random 3-CNFs
• Experimental results on the crossover point in random 3-SAT
• Graph decompositions and tree automata in reasoning with uncertainty
• DP-Complete Problems Derived from Extremal NP-Complete Properties
• Proof complexity in algebraic systems and bounded depth Frege systems with modular counting
• Upper bounds on the satisfiability threshold
• Resolution lower bounds for the weak functional pigeonhole principle.
• A sharp threshold for the phase transition of a restricted satisfiability problem for Horn clauses
• An Introduction to Lower Bounds on Resolution Proof Systems
• Cumulative space in black-white pebbling and resolution
• On the relation among answer set solvers
• Complete on average Boolean satisfiability
• Heuristic average-case analysis of the backtrack resolution of random 3-satisfiability instances
• A tutorial on time and space bounds in tree-like resolution
• Reasoning with propositional logic: from SAT solvers to knowledge compilation
• A threshold for unsatisfiability
• Implicates and prime implicates in random 3-SAT
• Hard random 3-SAT problems and the Davis-Putnam procedure
• Some computational aspects of DISTANCE SAT
• Short propositional refutations for dense random 3CNF formulas
• Witnesses for Answer Sets of Logic Programs
• Trade-offs between time and memory in a tighter model of CDCL SAT solvers
• Testing satisfiability of CNF formulas by computing a stable set of points
• Consistency, acyclicity, and positive Semirings
• Proof complexity and beyond. Abstracts from the workshop held March 24--29, 2024
• From small space to small width in resolution
• A general model and thresholds for random constraint satisfaction problems
• On minimal unsatisfiability and time-space trade-offs for \(k\)-DNF resolution
• Almost all graphs with 1.44n edges are 3-colorable
• On the relations between SAT and CSP enumerative algorithms
• A combinatorial characterization of resolution width
• Biased random k‐SAT
• Width versus size in resolution proofs
• The Multi-SAT algorithm
• Counting truth assignments of formulas of bounded tree-width or clique-width
• The probabilistic analysis of a greedy satisfiability algorithm
• Space Complexity in Polynomial Calculus
• Irreducible subcube partitions
• Lower bounds for the weak pigeonhole principle and random formulas beyond resolution
• Polarised random \(k\)-SAT
• Mutilated chessboard problem is exponentially hard for resolution
• 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
• Exact thresholds for DPLL on random XOR-SAT and NP-complete extensions of XOR-SAT
• Regular random \(k\)-SAT: Properties of balanced formulas
• The resolution complexity of random graph \(k\)-colorability
• Propositional proof complexity
• On the hardness of SAT with community structure
• Why adiabatic quantum annealing is unlikely to yield speed-up
• The solution space geometry of random linear equations
• Supercritical space-width trade-offs for resolution
• Davis-Putnam resolution versus unrestricted resolution
• An average case analysis of a resolution principle algorithm in mechanical theorem proving.
• An exponential lower bound for the size of monotone real circuits
• A lower bound for tree resolution
• Narrow proofs may be maximally long
• A sharp threshold in proof complexity yields lower bounds for satisfiability search
• Kolmogorov complexity based upper bounds for the unsatisfiability threshold of random \(k\)-SAT
• Complexity theory. Abstracts from the workshop held June 2--7, 2024
• Random resolution refutations
• On hard instances
• Meta-resolution: An algorithmic formalisation
• Finding the hardest formulas for resolution
• A framework for space complexity in algebraic proof systems
• Construction of expanders and superconcentrators using Kolmogorov complexity
• Simplified lower bounds for propositional proofs

This page was built for publication: Many hard examples for resolution

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3496310)