SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers
| Autor: | Germain Faure, Robert Nieuwenhuis, Enric Rodríguez-Carbonell, Albert Oliveras |
|---|---|
| Přispěvatelé: | Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X), Universitat Politècnica de Catalunya [Barcelona] (UPC), Faure, Germain |
| Jazyk: | angličtina |
| Rok vydání: | 2008 |
| Předmět: |
Theoretical computer science
[INFO.INFO-PL]Computer Science [cs]/Programming Languages [cs.PL] Modulo 0202 electrical engineering electronic engineering information engineering Linear arithmetic 020207 software engineering 020201 artificial intelligence & image processing Fraction (mathematics) 02 engineering and technology Mathematics [INFO.INFO-PL] Computer Science [cs]/Programming Languages [cs.PL] |
| Zdroj: | Theory and Applications of Satisfiability Testing-SAT 2008, 11th International Conference, SAT 2008, Guangzhou, China, May 12-15, 2008. Proceedings Theory and Applications of Satisfiability Testing-SAT 2008, 11th International Conference, SAT 2008, Guangzhou, China, May 12-15, 2008. Proceedings, Springer, 2008, 4996, pp.77-90 Theory and Applications of Satisfiability Testing – SAT 2008 ISBN: 9783540797180 SAT |
| Popis: | International audience; Many highly sophisticated tools exist for solving linear arith- metic optimization and feasibility problems. Here we analyze why it is difficult to use these tools inside systems for SAT Modulo Theories (SMT) for linear arithmetic: one needs support for disequalities, strict inequalities and, more importantly, for dealing with incorrect results due to the internal use of imprecise floating-point arithmetic. We explain how these problems can be overcome by means of result checking and error recovery policies. Second, by means of carefully designed experiments with, among other tools, the newest version of ILOG CPLEX and our own new Barcelogic T -solver for arithmetic, we show that, interestingly, the cost of result checking is only a small fraction of the total T -solver time. Third, we report on extensive experiments running exactly the same SMT search using CPLEX and Barcelogic as T -solvers, where CPLEX tends to be slower than Barcelogic. We analyze these at first sight surpris- ing results, explaining why tools such as CPLEX are not very adequate (nor designed) for this kind of relatively small incremental problems. Finally, we show how our result checking techniques can still be very use- ful in combination with inexact floating-point-based T -solvers designed for incremental SMT problems. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|