Bibliography

Bibliography#

Publication metadata is maintained in the shared BibTeX file. The entries below are cited in this book. Paper notes record the edition and sections read, the implemented subset and remaining questions; a bibliography entry alone does not mean the publication has been read or its method implemented.

Use DOI links for the cited edition when available, and an institutional record, report identifier or stable author link otherwise. Reference papers are not distributed with the documentation.

[1]

Tobias Achterberg, Timo Berthold, and Gregor Hendel. Rounding and propagation heuristics for mixed integer programming. Technical Report 11-29, Zuse Institute Berlin, 2011. URL: https://edocs.tib.eu/files/e01fn13/733448909l.pdf.

[2]

Erling D. Andersen and Knud D. Andersen. Presolving in linear programming. Mathematical Programming, 71(2):221–245, December 1995. doi:10.1007/bf01586000.

[3]

Timo Berthold. Heuristic algorithms in global MINLP solvers. PhD thesis, Technische Universität Berlin, 2014. URL: https://www.zib.de/userpage/berthold/Berthold2014.pdf.

[4]

Timo Berthold. RENS: the optimal rounding. Mathematical Programming Computation, 6:33–54, 2014. doi:10.1007/s12532-013-0060-9.

[5]

Nikolaj S. Bjørner and Lev Nachmanson. Arithmetic solving in Z3. In Computer Aided Verification - 36th International Conference, CAV, volume 14681, 26–41. Springer, 2024. doi:10.1007/978-3-031-65627-9_2.

[6]

Martin Bromberger. Decision Procedures for Linear Arithmetic. PhD thesis, Universität des Saarlandes, 2019. URL: https://publikationen.sulb.uni-saarland.de/handle/20.500.11880/28955.

[7]

Martin Bromberger, Mathias Fleury, Simon Schwarz, and Christoph Weidenbach. SPASS-SATT: a CDCL(LA) solver. In Automated Deduction – CADE 27, 111–122. 2019. doi:10.1007/978-3-030-29436-6_7.

[8]

Robert Brummayer and Armin Biere. Fuzzing and delta-debugging SMT solvers. In Proceedings of the 7th International Workshop on Satisfiability Modulo Theories, SMT '09, 1–5. ACM, August 2009. doi:10.1145/1670412.1670413.

[9]

Robert Daniel Brummayer. Efficient SMT Solving for Bit-Vectors and the Extensional Theory of Arrays. PhD thesis, Johannes Kepler University Linz, 2009. URL: https://research.jku.at/en/publications/efficient-smt-solving-for-bit-vectors-and-the-extensional-theory-/.

[10]

Leonardo Mendonça de Moura and Nikolaj S. Bjørner. Model-based theory combination. Electronic Notes in Theoretical Computer Science, 198(2):37–49, 2008. doi:10.1016/J.ENTCS.2008.04.079.

[11]

Bruno Dutertre. Yices 2.2. In Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings, volume 8559 of Lecture Notes in Computer Science, 737–744. Springer, 2014. doi:10.1007/978-3-319-08867-9_49.

[12]

Bruno Dutertre. The nuts and bolts of Yices. SMT Workshop, Coimbra, presentation slides, 2016. URL: https://yices.csl.sri.com/papers/smt2016-talk.pdf.

[13]

Bruno Dutertre and Leonardo de Moura. A fast linear-arithmetic solver for DPLL(T). CAV presentation slides, 2006. URL: https://yices.csl.sri.com/old/slides-cav06.pdf.

[14]

Bruno Dutertre and Leonardo de Moura. Integrating simplex with DPLL(T). Technical Report SRI-CSL-06-01, SRI International, 2006. URL: https://yices.csl.sri.com/papers/sri-csl-06-01.pdf.

[15]

Bruno Dutertre and Leonardo de Moura. The Yices SMT solver. Technical Report, SRI International, 2006. URL: https://yices.csl.sri.com/papers/tool-paper.pdf.

[16]

Bruno Dutertre and Leonardo Mendonça de Moura. A fast linear-arithmetic solver for DPLL(T). In Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, volume 4144 of Lecture Notes in Computer Science, 81–94. Springer, 2006. doi:10.1007/11817963_11.

[17]

Matteo Fischetti, Fred Glover, and Andrea Lodi. The feasibility pump. Mathematical Programming, 104:91–104, 2005. doi:10.1007/s10107-004-0570-3.

[18]

Yeting Ge and Leonardo de Moura. Complete instantiation for quantified formulas in satisfiability modulo theories. In Computer Aided Verification, volume 5643 of Lecture Notes in Computer Science, 306–320. Springer, 2009. URL: https://leodemoura.github.io/files/ci.pdf, doi:10.1007/978-3-642-02658-4_25.

[19]

Alberto Griggio. An Effective SMT Engine for Formal Verification. PhD thesis, University of Trento, 2009. doi:10.15168/11572_368265.

[20]

Mikoláš Janota and Jan Jakubův. Vibe-coded and tuned: a state-of-the-art SMT solver for QF-LRA. 2026. URL: https://arxiv.org/abs/2609.16706, arXiv:2609.16706.

[21]

Martin Jonáš and Jan Strejček. On simplification of formulas with unconstrained variables and quantifiers. In Theory and Applications of Satisfiability Testing – SAT 2017, 364–379. Springer International Publishing, 2017. URL: https://www.fi.muni.cz/~xstrejc/publications/sat2017preprint.pdf, doi:10.1007/978-3-319-66263-3_23.

[22]

Tim King. Effective Algorithms for the Satisfiability of Quantifier-Free Formulas Over Linear Real and Integer Arithmetic. PhD thesis, New York University, 2014. URL: https://cs.nyu.edu/media/publications/king_tim.pdf.

[23]

Zhengyang Lu, Paul Sarnighausen-Cahn, Jiahao Chen, Arie Gurfinkel, Florin Manea, and Vijay Ganesh. Learning SMT algorithm selection with high-level natural-language descriptions. In Foundations of Information and Knowledge Systems, 353–358. 2026. doi:10.1007/978-3-032-21540-6_23.

[24]

David Monniaux. On using floating-point computations to help an exact linear arithmetic decision procedure. In Computer Aided Verification, 570–583. Springer Berlin Heidelberg, 2009. doi:10.1007/978-3-642-02658-4_42.

[25]

Robert Nieuwenhuis and Albert Oliveras. Fast congruence closure and extensions. Information and Computation, 205(4):557–580, 2007. doi:10.1016/j.ic.2006.08.009.

[26]

William Pugh. The Omega test: a fast and practical integer programming algorithm for dependence analysis. Communications of the ACM, 35(8):102–114, 1992. URL: https://www.cs.umd.edu/~pugh/papers/omega.pdf.

[27]

Andrew Reynolds, Haniel Barbosa, and Pascal Fontaine. Revisiting enumerative instantiation. In Tools and Algorithms for the Construction and Analysis of Systems, volume 10806 of Lecture Notes in Computer Science, 112–131. Springer, 2018. URL: https://hanielbarbosa.com/papers/tacas2018.pdf, doi:10.1007/978-3-319-89963-3_7.