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.

BibTeX Entry

@inproceedings{FM-ICTAC17,
 author    = "Bertram Felgenhauer and Aart Middeldorp",
 title     = "Constructing Cycles in the Simplex Method for {DPLL(T)}",
 booktitle = "Proceedings of the 14th International Colloquium on
              Theoretical Aspects of Computing",
 editor    = "Dang Van Hung and Deepak Kapur",
 series    = "Lecture Notes in Computer Science",
 volume    = 10580,
 pages     = "213--228",
 year      = 2017,
 doi       = "10.1007/978-3-319-67729-3\_13"
}