Bibliography

Bibliography#

The current manual uses the BibTeX file. The entries below are cited in this manual. The literature notes and review ledger record editions and sections actually read; inclusion here does not establish reading coverage or implementation status.

The documentation distributes bibliographic metadata and original analysis, with DOI or stable publication links. Reference papers are not included.

[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]

Carlos Areces, David Déharbe, Pascal Fontaine, and Ezequiel Orbe. SyMT: finding symmetries in SMT formulas. In Proceedings of the 11th International Workshop on Satisfiability Modulo Theories. 2013. Work in progress. URL: https://members.loria.fr/PFontaine/Areces3.pdf.

[4]

Clark Barrett, Pascal Fontaine, and Cesare Tinelli. The SMT-LIB Standard: Version 2.7. 2026. Release March 27, 2026. URL: https://smt-lib.org/papers/smt-lib-reference-v2.7-r2026-03-27.pdf.

[5]

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

[6]

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

[7]

Nikolaj Bjørner and Katalin Fazekas. Incremental pre-processing for SMT. In Automated Deduction – CADE 29. 2023. URL: https://kfazekas.github.io/papers/BjornerFazekas-CADE23.pdf.

[8]

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.

[9]

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.

[10]

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.

[11]

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-/.

[12]

Richard Bödi, Katrin Herr, and Michael Joswig. Algorithms for highly symmetric linear and integer programs. 2011. arXiv:1012.4941, version 2. URL: https://arxiv.org/abs/1012.4941v2, doi:10.48550/arXiv.1012.4941.

[13]

Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, and Roberto Sebastiani. The MathSAT5 SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems, 93–107. 2013. URL: https://es-static.fbk.eu/people/griggio/papers/tacas13.pdf, doi:10.1007/978-3-642-36742-7_7.

[14]

Leonardo de Moura and Grant Olney Passmore. The Strategy Challenge in SMT Solving, pages 15–44. Springer Berlin Heidelberg, 2013. URL: https://doi.org/10.1007/978-3-642-36675-8_2, doi:10.1007/978-3-642-36675-8_2.

[15]

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.

[16]

Isil Dillig, Thomas Dillig, and Alex Aiken. Cuts from proofs: a complete and practical technique for solving linear inequalities over integers. Formal Methods in System Design, 39:246–260, 2011. URL: https://doi.org/10.1007/s10703-011-0127-z, doi:10.1007/s10703-011-0127-z.

[17]

Saket Dingliwal, Ronak Agarwal, Happy Mittal, and Parag Singla. Advances in symmetry breaking for SAT modulo theories. 2020. arXiv:1908.00860, version 2. URL: https://arxiv.org/abs/1908.00860v2, doi:10.48550/arXiv.1908.00860.

[18]

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.

[19]

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

[20]

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.

[21]

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.

[22]

David Déharbe, Pascal Fontaine, Stephan Merz, and Bruno Woltzenlogel Paleo. Exploiting symmetry in SMT problems. In Automated Deduction – CADE-23. 2011. URL: https://www.verit-solver.org/papers/cade2011.pdf.

[23]

Nick Feng and Fahiem Bacchus. Clause size reduction with all-UIP learning. In Theory and Applications of Satisfiability Testing – SAT 2020, 28–45. 2020. URL: https://pmc.ncbi.nlm.nih.gov/articles/PMC7326470/, doi:10.1007/978-3-030-51825-7_3.

[24]

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

[25]

Mathias Fleury and Armin Biere. Efficient all-UIP learned clause minimization (extended version). Technical Report 21/3, Johannes Kepler University Linz, 2021. URL: https://fmv.jku.at/papers/FleuryBiere-FMV-TR-21-3.pdf, doi:10.35011/fmvtr.2021-3.

[26]

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.

[27]

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

[28]

Mikoláš Janota and Jan Jakubův. Vibe-coded and tuned: a state-of-the-art SMT solver for QF-LRA. In Stephan Schulz, Konstantin Korovin, and Michael Rawson, editors, Proceedings of 16th International Workshop on the Implementation on Logics. Proceedings of the 26th Conference on Logic for Programming, Artificial Intelligence, and Reasoning (short papers), volume 23 of Kalpa Publications in Computing, 44–56. EasyChair, 2026. URL: https://easychair.org/publications/paper/rPZ9, doi:10.29007/rn52.

[29]

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.

[30]

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.

[31]

Tim King, Clark Barrett, and Bruno Dutertre. Simplex with sum of infeasibilities for SMT. In 2013 Formal Methods in Computer-Aided Design, 189–196. IEEE, October 2013. doi:10.1109/fmcad.2013.6679409.

[32]

François Margot. Symmetry in integer linear programming. In 50 Years of Integer Programming 1958–2008, pages 647–686. Springer, 2010. doi:10.1007/978-3-540-68279-0_17.

[33]

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.

[34]

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.

[35]

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.

[36]

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.

[37]

Niklas Sörensson and Armin Biere. Minimizing learned clauses. In Theory and Applications of Satisfiability Testing – SAT 2009, 237–243. 2009. URL: https://cca.informatik.uni-freiburg.de/papers/SoerenssonBiere-SAT09.pdf, doi:10.1007/978-3-642-02777-2_23.

[38]

Allen Van Gelder. Improved conflict-clause minimization leads to improved propositional proof traces. In Theory and Applications of Satisfiability Testing – SAT 2009, 141–146. 2009. URL: https://users.soe.ucsc.edu/~avg/Papers/ccmin-avg-sat09.pdf, doi:10.1007/978-3-642-02777-2_15.