Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Constructing Cycles in the Simplex Method for DPLL(T)

  • Conference paper
  • First Online:
Theoretical Aspects of Computing – ICTAC 2017 (ICTAC 2017)

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

Included in the following conference series:

  • 590 Accesses

Abstract

Modern SMT solvers use a special DPLL(T) variant of the simplex algorithm to solve satisfiability problems in linear real arithmetic. Termination is guaranteed by Bland’s pivot selection rule, but it is not immediately obvious that such a rule is required. For the traditional simplex method non-termination is well-understood, but the cycling examples from the literature do not immediately carry over to the DPLL(T) variant. We present two SMT encodings of the problem of finding cycles, using linear and nonlinear real arithmetic.

This research was supported by Austrian Science Fund (FWF) project P27528.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

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 EPUB and 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

Similar content being viewed by others

Notes

  1. 1.

    http://cl-informatik.uibk.ac.at/research/simplex/

  2. 2.

    We use \(\max (|p|,|q|)\) as a measure of simplicity of a rational number p / q; the smaller the measure the simpler the number.

  3. 3.

    While CVC4 [3] (snapshot version 2017-06-14) also has support for NRA, it cannot produce models, making it unfit for our purposes.

References

  1. Avis, D., Kaluzny, B., Titley-Péloquin, D.: Visualizing and constructing cycles in the simplex method. Oper. Res. 56(2), 512–518 (2008). doi:10.1287/opre.1070.0474

    Article  MathSciNet  MATH  Google Scholar 

  2. Balinski, M.L., Tucker, A.W.: Duality theory of linear programs: a constructive approach with applications. SIAM Rev. 11(3), 347–377 (1969). doi:10.1137/1011060

    Article  MathSciNet  MATH  Google Scholar 

  3. Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011). doi:10.1007/978-3-642-22110-1_14

    Chapter  Google Scholar 

  4. Beale, E.M.L.: Cycling in the dual simplex algorithm. Naval Res. Logistics Q. 2, 269–275 (1955). doi:10.1002/nav.3800020406

    Article  MathSciNet  Google Scholar 

  5. Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). doi:10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  6. Bland, R.G.: New finite pivoting rules for the simplex method. Math. Oper. Res. 2(2), 103–107 (1977). doi:10.1287/moor.2.2.103

    Article  MathSciNet  MATH  Google Scholar 

  7. Bradley, A.R., Manna, Z.: The Calculus of Computation—Decision Procedures with Applications to Verification. Springer, Heidelberg (2007). doi:10.1007/978-3-540-74113-8

    MATH  Google Scholar 

  8. Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737–744. Springer, Cham (2014). doi:10.1007/978-3-319-08867-9_49

    Google Scholar 

  9. Dutertre, B., Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81–94. Springer, Heidelberg (2006). doi:10.1007/11817963_11

    Chapter  Google Scholar 

  10. Dutertre, B., de Moura, L.: Integrating simplex with DPLL(T). Technical report SRI-CSL-06-01, SRI International (2006)

    Google Scholar 

  11. Goldfarb, D., Reid, J.K.: A practicable steepest-edge simplex algorithm. Math. Program. 12(1), 361–371 (1977). doi:10.1007/BF01593804

    Article  MathSciNet  MATH  Google Scholar 

  12. Harris, P.M.J.: Pivot selection methods of the Devex LP code. Math. Program. 5(1), 1–28 (1973). doi:10.1007/BF01580108

    Article  MathSciNet  MATH  Google Scholar 

  13. Hoffman, A.J.: Cycling in the simplex algorithm. Technical report, 2974. National Bureau of Standards (1953)

    Google Scholar 

  14. Kroening, D., Strichman, O.: Decision Procedures—An Algorithmic Point of View. Springer, Heidelberg (2008). doi:10.1007/978-3-540-74105-3

    MATH  Google Scholar 

  15. Marshall, K., Suurballe, J.: A note on cycling in the simplex method. Naval Res. Logistics Q. 16(1), 121–137 (1969). doi:10.1002/nav.3800160110

    Article  MATH  Google Scholar 

  16. Pan, P.Q.: A largest-distance pivot rule for the simplex algorithm. Eur. J. Oper. Res. 187(2), 393–402 (2008). doi:10.1016/j.ejor.2007.03.026

    Article  MathSciNet  MATH  Google Scholar 

  17. Sierksma, G.: Linear and Integer Programming, 2nd edn. Marcel Dekker Inc., New York City (1996)

    MATH  Google Scholar 

  18. Solow, D.: Linear Programming: An Introduction to Finite Improvement Algorithms. North-Holland, Amsterdam (1984)

    MATH  Google Scholar 

  19. Yudin, D.B., Gol’shtein, E.G.: Linear programming. In: Israel Program of Scientific Translations (1965)

    Google Scholar 

  20. Zörnig, P.: Systematic construction of examples for cycling in the simplex method. Comput. Oper. Res. 33(8), 2247–2262 (2006). doi:10.1016/j.cor.2005.02.001

    Article  MathSciNet  MATH  Google Scholar 

Download references

Acknowledgements

We thank the reviewers for their constructive feedback.

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Innsbruck, Innsbruck, Austria

    Bertram Felgenhauer & Aart Middeldorp

Authors
  1. Bertram Felgenhauer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Aart Middeldorp
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Bertram Felgenhauer .

Editor information

Editors and Affiliations

  1. Vietnam National University, Hanoi, Vietnam

    Dang Van Hung

  2. University of New Mexico, Albuquerque, New Mexico, USA

    Deepak Kapur

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Felgenhauer, B., Middeldorp, A. (2017). Constructing Cycles in the Simplex Method for DPLL(T). In: Hung, D., Kapur, D. (eds) Theoretical Aspects of Computing – ICTAC 2017. ICTAC 2017. Lecture Notes in Computer Science(), vol 10580. Springer, Cham. https://doi.org/10.1007/978-3-319-67729-3_13

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-67729-3_13

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-67728-6

  • Online ISBN: 978-3-319-67729-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation