Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem
From MaRDI portal
Publication:1170883
DOI10.1016/0166-218X(83)90017-3zbMath0497.68021OpenAlexW2022695609MaRDI QIDQ1170883
John V. Franco, Marvin C. Paull
Publication date: 1983
Published in: Discrete Applied Mathematics (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/0166-218x(83)90017-3
probabilistic analysisNP-completenesssatisfiability problemDavis-Putnam procedureinstance distributionspolynomial average complexity
Analysis of algorithms and problem complexity (68Q25) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17)
Related Items (55)
Kolmogorov complexity based upper bounds for the unsatisfiability threshold of random k-SAT ⋮ Waiter-client and client-waiter colourability and \(k\)-SAT games ⋮ Solving satisfiability in less than \(2^ n\) steps ⋮ A lower bound for tree resolution ⋮ Exploiting the deep structure of constraint problems ⋮ Polynomial-average-time satisfiability problems ⋮ A new algorithm for the propositional satisfiability problem ⋮ The expected complexity of analytic tableaux analyses in propositional calculus. II ⋮ An average case analysis of a resolution principle algorithm in mechanical theorem proving. ⋮ Some results and experiments in programming techniques for propositional logic ⋮ Branch-and-cut solution of inference problems in propositional logic ⋮ Solving propositional satisfiability problems ⋮ The threshold for random 𝑘-SAT is 2^{𝑘}log2-𝑂(𝑘) ⋮ Probabilistic performance of a heurisic for the satisfiability problem ⋮ Unnamed Item ⋮ Proof of the satisfiability conjecture for large \(k\) ⋮ Generating hard satisfiability problems ⋮ Hard random 3-SAT problems and the Davis-Putnam procedure ⋮ Why adiabatic quantum annealing is unlikely to yield speed-up ⋮ Unnamed Item ⋮ Generating random instances of weighted model counting. An empirical analysis with varying primal treewidth ⋮ Go-MOCE: greedy order method of conditional expectations for Max Sat ⋮ On good algorithms for determining unsatisfiability of propositional formulas ⋮ Complete Boolean satisfiability solving algorithms based on local search ⋮ Average performance of greedy heuristics for the integer knapsack problem. ⋮ Probabilistic analysis of a generalization of the unit-clause literal selection heuristics for the k-satisfiability problem ⋮ Probabilistic bounds and algorithms for the maximum satisfiability problem ⋮ Two tractable subclasses of minimal unsatisfiable formulas ⋮ Gibbs states and the set of solutions of random constraint satisfaction problems ⋮ The scaling window of the 2-SAT transition ⋮ Controlled generation of hard and easy Bayesian networks: Impact on maximal clique size in tree clustering ⋮ The large deviations of the whitening process in random constraint satisfaction problems ⋮ Satisfiability threshold for power law random 2-SAT in configuration model ⋮ Counting propositional models ⋮ On the satisfiability threshold of formulas with three literals per clause ⋮ Rigorous results for random (\(2+p)\)-SAT ⋮ Random 2-SAT: Results and problems ⋮ Results related to threshold phenomena research in satisfiability: Lower bounds ⋮ Lower bounds for random 3-SAT via differential equations ⋮ Upper bounds on the satisfiability threshold ⋮ A complete adaptive algorithm for propositional satisfiability ⋮ A dual algorithm for the satisfiability problem ⋮ Correction to ``Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem ⋮ Linear programs for constraint satisfaction problems ⋮ Exact thresholds for DPLL on random XOR-SAT and NP-complete extensions of XOR-SAT ⋮ On subclasses of minimal unsatisfiable formulas ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Average time analyses of simplified Davis-Putnam procedures ⋮ Using the method of conditional expectations to supply an improved starting point for CCLS ⋮ Biased landscapes for random constraint satisfaction problems ⋮ Typical case complexity of satisfiability algorithms and the threshold phenomenon ⋮ A perspective on certain polynomial-time solvable classes of satisfiability ⋮ Solving non-uniform planted and filtered random SAT formulas greedily ⋮ A model of random industrial SAT
Cites Work
This page was built for publication: Probabilistic analysis of the Davis Putnam procedure for solving the satisfiability problem
