Skip to main content
SpringerLink
Log in

Observed Lower Bounds for Random 3-SAT Phase Transition Density Using Linear Programming

  • Conference paper
Theory and Applications of Satisfiability Testing (SAT 2005)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 3569))

  • 1041 Accesses

Abstract

We introduce two incomplete polynomial time algorithms to solve satisfiability problems which both use Linear Programming (LP) techniques. First, the FlipFlop LP attempts to simulate a Quadratic Program which would solve the CNF at hand. Second, the WeightedLinearAutarky LP is an extended variant of the LinearAutarky LP as defined by Kullmann [6] and iteratively updates its weights to find autarkies in a given formula. Besides solving satisfiability problems, this LP could also be used to study the existence of autark assignments in formulas. Results within the experimental domain (up to 1000 variables) show a considerably sharper lower bound for the uniform random 3-Sat phase transition density than the proved lower bound of the myopic algorithm (> 3.26) by Achlioptas [1] and even than that of the greedy algorithm (> 3.52) proposed by Kaporis [5].

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Achlioptas, D.: Lower Bounds for Random 3-SAT via Differential Equations. Theoretical Computer Science 265(1-2), 159–185 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  2. Boros, E., Crama, Y., Hammer, P., Saks, M.: A complexity Index for Satisfiability Problems. SIAM Journal on Computing 23(1), 45–49 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  3. Franco, J.: Results related to threshold phenomena research in Satisfiability: lower bounds. Theoretical Computer Science 265(1-2), 147–157 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  4. Kaporis, A.C., Kirousis, L.M., Lalas, E.G.: The Probabilistic Analysis of a Greedy Satisfiability Algorithm. In: Möhring, R.H., Raman, R. (eds.) ESA 2002. LNCS, vol. 2461, pp. 574–585. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  5. Kaporis, A.C., Kirousis, L.M., Lalas, E.G.: Selecting complementary pairs of literals. Electronic Notes in Discrete Mathematics 16 (2003)

    Google Scholar 

  6. Kullmann, O.: Investigations on autark assignments. Discrete Applied Mathematics 107(1-3), 99–137 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  7. Kullmann, O.: Lean clause-sets: generalizations of minimally unsatisfiable clause-sets. Discrete Applied Mathematics 130(2), 209–249 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  8. Van Gelder, A.: Problem generator mkcnf.c contributed to the DIMACS Challenge archieve

    Google Scholar 

  9. Warners, J.P., van Maaren, H.: A two phase algorithm for solving a class of hard satisfiability problems. Oper. Res. Lett. 23(3-5), 81–88 (1998)

    Article  MATH  MathSciNet  Google Scholar 

  10. Warners, J., van Maaren, H.: Solving satisfiability problems using elliptic approximations. Effective branching rules. Discrete Applied Mathematics 107(1-3), 241–259 (2000)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Software Technology, Faculty of Electrical Engineering, Mathematics and Computer Sciences, Delft University of Technology,  

    Marijn Heule & Hans van Maaren

Authors
  1. Marijn Heule
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Hans van Maaren
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, University of Toronto, Canada

    Fahiem Bacchus

  2. Dept. of Computer Science, Trinity College, Dublin 2

    Toby Walsh

Rights and permissions

Reprints and permissions

Copyright information

© 2005 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Heule, M., van Maaren, H. (2005). Observed Lower Bounds for Random 3-SAT Phase Transition Density Using Linear Programming. In: Bacchus, F., Walsh, T. (eds) Theory and Applications of Satisfiability Testing. SAT 2005. Lecture Notes in Computer Science, vol 3569. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11499107_9

Download citation

  • DOI: https://doi.org/10.1007/11499107_9

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-26276-3

  • Online ISBN: 978-3-540-31679-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation