nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Polynomial Constraints and Unsat Cores in Tarski

verfasst von : Fernando Vale-Enriquez, Christopher W. Brown

Erschienen in: Mathematical Software – ICMS 2018

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

This paper gives a brief overview of Tarski, a system for computing with Tarski formulas, which are boolean combinations of non-linear polynomial constraints over the reals. It gives an overview of Tarski’s basic functionality, then goes into more detail on facilities Tarski provides for checking the satisfiability of conjunctions of constraints that are able to produce “unsat cores” for unsatisfiable inputs.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel HomotopyContinuation.jl: A Package for Homotopy Continuation in Julia

Nächstes Kapitel Private-Key Fully Homomorphic Encryption for Private Classification

Tarski is available at https://www.usna.edu/Users/cs/wcbrown/tarski/. It is open source, distributed under an ISC-style license.

Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: version 2.0. In: Gupta, A., Kroening, D. (eds.) Proceedings of the 8th International Workshop on Satisfiability Modulo Theories, Edinburgh, UK (2010)

Brown, C.W.: QEPCAD B: a program for computing with semi-algebraic sets using CADs. ACM SIGSAM Bull. 37(4), 97–108 (2003)CrossRef

Brown, C.W.: Fast simplifications for Tarski formulas. In: Proceedings of the 2009 International Symposium on Symbolic and Algebraic Computation, ISSAC 2009, New York, NY, USA, pp. 63–70. ACM (2009)

Brown, C.W.: Fast simplifications for Tarski formulas based on monomial inequalities. J. Symb. Comput. 47(7), 859–882 (2012)MathSciNetCrossRef

Brown, C.W., Davenport, J.H.: The complexity of quantifier elimination and cylindrical algebraic decomposition. In: Proceedings of the 2007 International Symposium on Symbolic and Algebraic Computation, ISSAC 2007, New York, NY, USA, pp. 54–60. ACM (2007)

Brown, C.W., Strzeboński, A.: Black-box/white-box simplification and applications to quantifier elimination. In: Proceedings of the 2010 International Symposium on Symbolic and Algebraic Computation, ISSAC 2010, New York, NY, USA, pp. 69–76. ACM (2010)

Caviness, B.F., Johnson, J.R. (eds.): Quantifier Elimination and Cylindrical Algebraic Decomposition. Texts and Monographs in Symbolic Computation. Springer, Heidelberg (1998). https://doi.org/10.1007/978-3-7091-9459-1CrossRefMATH

Chen, C., Davenport, J.H., Lemaire, F., Maza, M.M., Xia, B., Xiao, R., Xie, Y.: Computing the real solutions of polynomial systems with the RegularChains library in Maple. ACM Commun. Comput. Algebra 45, 166–168 (2011)CrossRef

Corzilius, F., Loup, U., Junges, S., Ábrahám, E.: SMT-RAT: an SMT-compliant nonlinear real arithmetic toolbox. In: Cimatti, A., Sebastiani, R. (eds.) SAT 2012. LNCS, vol. 7317, pp. 442–448. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31612-8_35CrossRef

10.

Davenport, J.H., Heintz, J.: Real quantifier elimination is doubly exponential. J. Symb. Comput. 5, 29–35 (1997)MathSciNetCrossRef

11.

Dolzmann, A., Seidl, A., Sturm, T.: Efficient projection orders for CAD. In: Gutierrez, J. (ed.) Proceedings of the 2004 International Symposium on Symbolic and Algebraic Computation (ISSAC 2004), Santander, Spain, July 2004. ACM (2004)

12.

Dutertre, B.: Yices 2.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737–744. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08867-9_49CrossRef

13.

England, M., et al.: Problem formulation for truth-table invariant cylindrical algebraic decomposition by incremental triangular decomposition. In: Watt, S.M., Davenport, J.H., Sexton, A.P., Sojka, P., Urban, J. (eds.) CICM 2014. LNCS (LNAI), vol. 8543, pp. 45–60. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08434-3_5CrossRef

14.

Huang, Z., England, M., Davenport, J.M., Paulson, L.C.: Using machine learning to decide when to precondition cylindrical algebraic decomposition with Groebner bases. In: 2016 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), pp. 45–52, September 2016

15.

Jovanović, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 339–354. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31365-3_27CrossRef

16.

McCallum, S.: Solving polynomial strict inequalities using cylindrical algebraic decomposition. Comput. J. 36(5), 432–438 (1993)MathSciNetCrossRef

17.

Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis-Putnam-Logemann-Loveland procedure to DPLL(T). J. ACM 53, 2006 (2006)MathSciNetCrossRef

18.

Papachristodoulou, A., Anderson, J., Valmorbida, G., Prajna, S., Seiler, P., Parrilo, P.A.: SOSTOOLS: sum of squares optimization toolbox for MATLAB (2013). http://www.eng.ox.ac.uk/control/sostools. http://arxiv.org/abs/1310.4716

19.

Strzebonski, A.: Solving systems of strict polynomial inequalities. J. Symb. Comput. 29, 471–480 (2000)MathSciNetCrossRef

20.

Tarski, A.: A Decision Method for Elementary Algebra and Geometry, Second edn. University of California Press, Berkeley (1951). rev. Reprinted in [7]

21.

Weispfenning, V.: The complexity of linear problems in fields. J. Symb. Comput. 5(1–2), 3–27 (1988)MathSciNetCrossRef

Titel: Polynomial Constraints and Unsat Cores in Tarski
verfasst von: Fernando Vale-Enriquez
Christopher W. Brown
Verlag: Springer International Publishing
Buch: Mathematical Software – ICMS 2018
Print ISBN: 978-3-319-96417-1

Electronic ISBN: 978-3-319-96418-8

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-319-96418-8_55

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner