cl-banner

Constructing Cycles in the Simplex Method for DPLL(T)

Bertram Felgenhauer and Aart Middeldorp

Proceedings of the 14th International Colloquium on Theoretical Aspects of Computing (ICTAC 2017), Lecture Notes in Computer Science 10580, pp. 213 – 228, 2017.

Abstract

Modern SMT solvers use a special DPLL 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 variant. We present two SMT encodings of the problem of finding cycles, using linear and nonlinear real arithmetic.

 

  PDF |    doi:10.1007/978-3-319-67729-3_13 |  © Springer International Publishing AG

BibTeX 

@inproceedings{BFAM-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 = "D.V. Hung and D. Kapur",
series = "Lecture Notes in Computer Science",
volume = 10580,
pages = "213--228",
year = 2017,
doi = "10.1007/978-3-319-67729-3_13"
}
Nach oben scrollen