, , 2018.
, , 2018.
,
, CAV, vol.6806, 2011.
, The Satisfiability Modulo Theories Library (SMT-LIB). www.SMT-LIB.org, 2016.
Splitting on demand in SAT modulo theories, Logic for Programming, vol.4246, pp.512-526, 2006. ,
A reduction from unbounded linear mixed arithmetic problems into bounded problems, Automated Reasoning, vol.10900, 2018. ,
URL : https://hal.archives-ouvertes.fr/hal-01942228
SPASS-SATT -A CDCL(LA) solver, editor, Automated Deduction -CADE 27 -27th International Conference on Automated Deduction, vol.11716, pp.111-122, 2019. ,
URL : https://hal.archives-ouvertes.fr/hal-02405524
Linear integer arithmetic revisited, LNCS, vol.9195, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01239394
Fast cube tests for LIA constraint solving, IJCAR 2016, vol.9706, 2016. ,
URL : https://hal.archives-ouvertes.fr/hal-01403200
New Techniques for Linear Arithmetic: Cubes and Equalities, Formal Methods in System Design, vol.51, issue.3, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01656397
Techniques for verifying superscalar microprocessors, DAC, pp.552-557, 1996. ,
The MathSAT5 SMT Solver, TACAS, vol.7795, 2013. ,
Exotic semi-ring constraints, SMT@IJCAR, vol.20, pp.88-97, 2012. ,
Z3: an efficient SMT solver, LNCS, vol.4963, pp.337-340, 2008. ,
, , 2008.
Cuts from proofs: A complete and practical technique for solving linear inequalities over integers, CAV, vol.5643, 2009. ,
Yices 2.2, CAV 2014, vol.8559, 2014. ,
Extended version: Integrating simplex with DPLL(T), CSL, SRI INTERNATIONAL, vol.4144, 2006. ,
DPLL(T): fast decision procedures, CAV, 2004. ,
A practical approach to satisfiability modulo linear integer arithmetic, JSAT, vol.8, issue.1, 2012. ,
Boolean methods in operations research and related areas, 2012. ,
FLINT: Fast Library for Number Theory, 2013. ,
Cutting to the chase solving linear integer arithmetic, CADE, vol.6803, pp.338-353, 2011. ,
Reducibility among combinatorial problems, Complexity of Computer Computations, The IBM Research Symposia Series, pp.85-103, 1972. ,
Efficient term-ite conversion for satisfiability modulo theories, SAT, vol.5584, pp.195-208, 2009. ,
The IntSat method for integer linear programming, Principles and Practice of Constraint Programming, vol.8656, 2014. ,
DPLL(T) with exhaustive theory propagation and its application to difference logic, CAV, pp.321-334, 2005. ,
Solving SAT and SAT modulo theories: From an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T ), J. ACM, vol.53, issue.6, pp.937-977, 2006. ,
Computing small clause normal forms, Handbook of Automated Reasoning, vol.1, 2001. ,
Theory of Linear and Integer Programming, 1986. ,
Lazy satisability modulo theories, JSAT, vol.3, issue.3-4, pp.141-224, 2007. ,
On the complexity of derivations in propositional calculus, Automation of Reasoning: Classical Papers on Computational Logic, vol.2, pp.466-483, 1968. ,
SPASS version 3.5, 22nd International Conference on Automated Deduction, vol.5663, pp.140-145, 2009. ,