Abstract
We present some recent results on algorithms for satisfiability of k-CNF formulas: fastest probabilistic algorithms. We mention some results in proof complexity that can be used to derive lower bounds on classes of algorithms for satisfiability.
The author was partially supported by grant A1019602 of the Academy of Sciences of the Czech Republic and by a joint grant of NSF (USA) and MšMT (Czech Rep.) INT-9600919/ME-103.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
P. Beame, R. Karp, T. Pitassi and M. Saks, On the complexity of unsatisfiability proofs for random k-CNF formulas, Proc. 30-th STOC, 1998, to appear.
S.A. Cook, The complexity of theorem proving procedures, Proc. 3-rd STOC, 1971, 151–158.
S.A. Cook and A.R. Reckhow, The relative efficiency of propositional proof systems, J. of Symbolic Logic 44(1), 1979, 36–50.
M. Davis, G. Logemann and D. Loveland, A machine program for theorem proving, Communications of the ACM 5, 1962, 394–397.
L.K. Grover, A fast quantum mechanical algorithm for database search, Proc. 28-th STOC 1996, 212–218.
A. Haken, The intractability of resolution, Theor. Computer Science, 39, 1985, 297–308.
J. Håstad, Almost optimal lower bounds for small depth circuits, Proc. 18-th STOC, 1986, 6–20.
E.A. Hirsch, Two new upper bounds for SAT, Proc. 9-th SODA, 1998, to appear.
R. Impagliazzo, P. Pudlák and J. Sgall, Lower Bounds for the Polynomial Calculus and the Groebner Basis Algorithm, to appear in Computational Complexity.
J. Krajíček, Bounded arithmetic, propositional logic, and complexity theory, Cambridge Univ. Press 1995.
B. Monien and E. Speckenmeyer, Solving satisfiability in less than 2n steps, Discrete Applied Math. 10, 1985, 287–295.
R. Paturi, P. Pudlák and F. Zane, Satisfiability coding lemma, Proc. 38-th FOCS, 1997, 566–574.
R. Paturi, P. Pudlák, M.E. Saks and F. Zane, An improved exponential-time algorithm for k-SAT, preprint, 1998.
P. Pudlák, Lower bounds for resolution and cutting planes proofs and monotone computations, J. of Symb. Logic 62(3), 1997, 981–998.
A. A. Razborov, Lower bounds for the polynomial calculus, to appear in Computational Complexity.
I. Schiermeyer, Solving 3-Satisfiability in less than 1.579n steps, CSL'92, LNCS 702, 1993, 379–394.
I. Schiermeyer, Pure literal look ahead: An O(1.497n) 3-satisfiability algorithm, preprint, 1996.
G.C. Tseitin, On the complexity of derivations in propositional calculus, Studies in mathematics and mathematical logic, Part II, ed. A.O. Slisenko, 1968, 115–125.
A. Urquhart, Hard examples for resolution, J. of ACM 34, 1987, 209–219.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1998 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pudlák, P. (1998). Satisfiability — Algorithms and logic. In: Brim, L., Gruska, J., Zlatuška, J. (eds) Mathematical Foundations of Computer Science 1998. MFCS 1998. Lecture Notes in Computer Science, vol 1450. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055762
Download citation
DOI: https://doi.org/10.1007/BFb0055762
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-64827-7
Online ISBN: 978-3-540-68532-6
eBook Packages: Springer Book Archive