Many hard examples for resolution
From MaRDI portal
Publication:3496310
DOI10.1145/48014.48016zbMATH Open0712.03008OpenAlexW2126420408WikidataQ59699144 ScholiaQ59699144MaRDI QIDQ3496310FDOQ3496310
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
Recommendations
Analysis of algorithms and problem complexity (68Q25) Mechanization of proofs and logical operations (03B35)
Cited In (only showing first 100 items - show all)
- Captain Jack: new variable selection heuristics in local search for SAT
- A combinatorial characterization of treelike resolution space
- Tseitin's formulas revisited
- Reflections on Proof Complexity and Counting Principles
- Generating hard satisfiability problems
- The state of SAT
- A feasibly constructive lower bound for resolution proofs
- Towards NP-P via proof complexity and search
- On the structure of some classes of minimal unsatisfiable formulas
- The Complexity of Propositional Proofs
- Unrestricted resolution versus N-resolution
- A perspective on certain polynomial-time solvable classes of satisfiability
- On good algorithms for determining unsatisfiability of propositional formulas
- Limitations of restricted branching in clause learning
- Frozen development in graph coloring
- Clause trees: A tool for understanding and implementing resolution in automated reasoning
- An efficient local search method for random 3-satisfiability
- The symmetry rule in propositional logic
- Parameterized complexity of DPLL search procedures
- Sharp thresholds for constraint satisfaction problems and homomorphisms
- A spectral technique for random satisfiable 3CNF formulas
- Experimental results on the crossover point in random 3-SAT
- Probabilistic bounds and algorithms for the maximum satisfiability problem
- Upper bounds on the satisfiability threshold
- Lower bounds for \(k\)-DNF resolution on random 3-CNFs
- An improved upper bound on the non-3-colourability threshold
- An Introduction to Lower Bounds on Resolution Proof Systems
- Proof complexity in algebraic systems and bounded depth Frege systems with modular counting
- Resolution lower bounds for the weak functional pigeonhole principle.
- Cumulative space in black-white pebbling and resolution
- On the relation among answer set solvers
- Complete on average Boolean satisfiability
- A threshold for unsatisfiability
- Heuristic average-case analysis of the backtrack resolution of random 3-satisfiability instances
- 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
- From small space to small width in resolution
- Almost all graphs with 1.44n edges are 3-colorable
- A general model and thresholds for random constraint satisfaction problems
- A combinatorial characterization of resolution width
- On the relations between SAT and CSP enumerative algorithms
- The probabilistic analysis of a greedy satisfiability algorithm
- The \(Multi\)-SAT algorithm
- Counting truth assignments of formulas of bounded tree-width or clique-width
- Lower bounds for the weak pigeonhole principle and random formulas beyond resolution
- 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
- Propositional proof complexity
- Regular random \(k\)-SAT: Properties of balanced formulas
- Why adiabatic quantum annealing is unlikely to yield speed-up
- On the hardness of SAT with community structure
- 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
- Kolmogorov complexity based upper bounds for the unsatisfiability threshold of random \(k\)-SAT
- A sharp threshold in proof complexity yields lower bounds for satisfiability search
- Construction of expanders and superconcentrators using Kolmogorov complexity
- On hard instances
- Meta-resolution: An algorithmic formalisation
- Simplified lower bounds for propositional proofs
- When does the giant component bring unsatisfiability?
- Spines of random constraint satisfaction problems: definition and connection with computational complexity
- Many hard examples in exact phase transitions
- The scaling window of the 2-SAT transition
- Space bounds for resolution
- Title not available (Why is that?)
- Random \( \Theta (\log n) \) -CNFs are Hard for Cutting Planes
- Title not available (Why is that?)
- Typical case complexity of satisfiability algorithms and the threshold phenomenon
- The impact of heterogeneity and geometry on the proof complexity of random satisfiability
- Solving non-uniform planted and filtered random SAT formulas greedily
- Space proof complexity for random 3-CNFs
- Vašek Chvátal: a very short introduction (on the occasion of his 60th birthday)
- Graph decompositions and tree automata in reasoning with uncertainty
- DP-Complete Problems Derived from Extremal NP-Complete Properties
- A sharp threshold for the phase transition of a restricted satisfiability problem for Horn clauses
- Reasoning with propositional logic: from SAT solvers to knowledge compilation
- A tutorial on time and space bounds in tree-like resolution
- 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
- On minimal unsatisfiability and time-space trade-offs for \(k\)-DNF resolution
- Biased random k‐SAT
- Width versus size in resolution proofs
- Irreducible subcube partitions
- Space Complexity in Polynomial Calculus
- Polarised random \(k\)-SAT
- The resolution complexity of random graph \(k\)-colorability
- The solution space geometry of random linear equations
- Narrow proofs may be maximally long
- Complexity theory. Abstracts from the workshop held June 2--7, 2024
- Finding the hardest formulas for resolution
- Random resolution refutations
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)
