Clark Barrett, Pascal Fontaine & Cesare Tinelli (2016):
The Satisfiability Modulo Theories Library (SMT-LIB).
www.SMT-LIB.org.
Clark Barrett, Robert Nieuwenhuis, Albert Oliveras & Cesare Tinelli (2006):
Splitting on Demand in SAT Modulo Theories.
In: International Conference on Logic for Programming Artificial Intelligence and Reasoning (LPAR'06).
Springer,
pp. 512–526,
doi:10.1007/11916277_35.
Florian Corzilius & Erika Ábrahám (2011):
Virtual Substitution for SMT-Solving.
In: International Symposium on Fundamentals of Computation Theory (FCT'11).
Springer,
pp. 360–371,
doi:10.1007/978-3-642-22953-4_31.
Florian Corzilius, Gereon Kremer, Sebastian Junges, Stefan Schupp & Erika Ábrahám (2015):
SMT-RAT: An Open Source C++ Toolbox for Strategic and Parallel SMT Solving.
In: International Conference on Theory and Applications of Satisfiability Testing (SAT'15).
Springer,
pp. 360–368,
doi:10.1007/978-3-319-24318-4_26.
Scott Cotton (2010):
Natural Domain SMT: A Preliminary Assessment.
In: International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS'10).
Springer,
pp. 77–91,
doi:10.1007/978-3-642-15297-9_8.
George Bernard Dantzig (1998):
Linear Programming and Extensions 48.
Princeton University Press,
doi:10.1515/9781400884179.
Bruno Dutertre & Leonardo De Moura (2006):
Integrating Simplex with DPLL(T).
Computer Science Laboratory, SRI International, Tech. Rep. SRI-CSL-06-01.
Julius Farkas (1902):
Theorie der einfachen Ungleichungen.
Journal für die reine und angewandte Mathematik (Crelles Journal) 1902(124),
pp. 1–27,
doi:10.1515/crll.1902.124.1.
Jean Baptiste Joseph Fourier (1827):
Analyse des travaux de l’Académie Royale des Sciences pendant l’année 1824.
Partie mathématique.
Jean-Louis Imbert (1990):
About Redundant Inequalities Generated by Fourier's Algorithm.
In: International Conference on Artificial Intelligence: Methodology, Systems, Applications (AIMSA'90).
Elsevier,
pp. 117–127,
doi:10.1016/B978-0-444-88771-9.50019-2.
Jean-Louis Imbert (1993):
Fourier's Elimination: Which to Choose?.
In: International Conference on Principles and Practice of Constraint Programming (PPCP'93) 1.
Citeseer,
pp. 117–129.
Rui-Juan Jing, Marc Moreno-Maza & Delaram Talaashrafi (2020):
Complexity Estimates for Fourier-Motzkin Elimination.
In: Computer Algebra in Scientific Computing (CASC'20).
Springer,
pp. 282–306,
doi:10.1007/978-3-030-60026-6_16.
Leonid Genrikhovich Khachiyan (1980):
Polynomial Algorithms in Linear Programming.
USSR Computational Mathematics and Mathematical Physics 20(1),
pp. 53–72,
doi:10.1016/0041-5553(80)90061-0.
Tim King, Clark Barrett & Bruno Dutertre (2013):
Simplex with Sum of Infeasibilities for SMT.
In: Formal Methods in Computer-Aided Design (FMCAD'13),
pp. 189–196,
doi:10.1109/FMCAD.2013.6679409.
Konstantin Korovin, Marek Kosta & Thomas Sturm (2014):
Towards Conflict-driven Learning for Virtual Substitution.
In: International Workshop on Computer Algebra in Scientific Computing (CASC'14).
Springer,
pp. 256–270,
doi:10.1007/978-3-319-10515-4_19.
Konstantin Korovin, Nestan Tsiskaridze & Andrei Voronkov (2009):
Conflict Resolution.
In: Principles and Practice of Constraint Programming (CP'09).
Springer,
pp. 509–523,
doi:10.1007/978-3-642-04244-7_41.
Konstantin Korovin & Andrei Voronkov (2011):
Solving Systems of Linear Inequalities by Bound Propagation.
In: Conference on Automated Deduction (CADE'23).
Springer,
pp. 369–383,
doi:10.1007/978-3-642-22438-6_28.
Carlton E. Lemke (1954):
The Dual Method of Solving the Linear Programming Problem.
Naval Research Logistics Quarterly 1(1),
pp. 36–47,
doi:10.1002/nav.3800010107.
Haokun Li, Bican Xia, Huiying Zhang & Tao Zheng (2021):
Choosing the Variable Ordering for Cylindrical Algebraic Decomposition via Exploiting Chordal Structure.
In: International Symposium on Symbolic and Algebraic Computation (ISSAC'21).
ACM,
pp. 281–288,
doi:10.1145/3452143.3465520.
Rüdiger Loos & Volker Weispfenning (1993):
Applying Linear Quantifier Elimination.
The Computer Journal 36(5),
pp. 450–462,
doi:10.1093/comjnl/36.5.450.
David G Luenberger & Yinyu Ye (1984):
Linear and Nonlinear Programming 2nd edition.
Springer,
doi:10.1007/978-3-030-85450-8.
Kenneth L. McMillan, Andreas Kuehlmann & Mooly Sagiv (2009):
Generalizing DPLL to Richer Logics.
In: International Conference on Computer Aided Verification (CAV'09).
Springer,
pp. 462–476,
doi:10.1007/978-3-642-02658-4_35.
Theodore Samuel Motzkin (1936):
Beiträge zur Theorie der linearen Ungleichungen.
Azriel.
Jasper Nalbach, Erika Ábrahám & Gereon Kremer (2021):
Extending the Fundamental Theorem of Linear Programming for Strict Inequalities.
In: International Symposium on Symbolic and Algebraic Computation (ISSAC'21).
ACM,
pp. 313–320,
doi:10.1145/3452143.3465538.
Jasper Nalbach, Valentin Promies, Erika Ábrahám & Paul Kobialka (2023):
FMplex: A Novel Method for Solving Linear Real Arithmetic Problems.
ArXiv:2309.03138.
Tobias Nipkow (2008):
Linear Quantifier Elimination.
In: Internation Joint Conference on Automated Reasoning (IJCAR'08).
Springer,
pp. 18–33,
doi:10.1007/978-3-540-71070-7_3.
Volker Weispfenning (1997):
Quantifier Elimination for Real Algebra—the Quadratic Case and Beyond.
Applicable Algebra in Engineering, Communication and Computing 8(2),
pp. 85–101,
doi:10.1007/s002000050055.
eptcs@eptcs.org