Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
MTZ-Fachkongress

Antriebe und Energiesysteme von morgen


Austausch von Automobil- und Energiewirtschaft

Am 14./15. Mai geht es in Chemnitz um die Mobilitätswende durch Elektro- und Wasserstofffahrzeuge.
Erweiterte Suche
Anmelden
nach oben
Formal Methods in System Design
Erschienen in: Formal Methods in System Design 3/2017

27.06.2017

raSAT: an SMT solver for polynomial constraints

verfasst von: Vu Xuan Tung, To Van Khanh, Mizuhito Ogawa

Erschienen in: Formal Methods in System Design | Ausgabe 3/2017

Einloggen

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

search-config
loading …

Abstract

This paper presents raSAT SMT solver, which is aimed to handle polynomial constraints over both reals and integers with simple unified methodologies. Its three main features are (1) a raSAT loop for inequalities, which adds testing to interval constraint propagation to accelerate SAT detection, (2) a non-constructive reasoning for equations over reals based on the generalized intermediate value theorem, and (3) soundness of floating-point arithmetic that is guaranteed by (a) rounding up/down over-approximations of intervals, and (b) confirmation of a satisfying instance detected by testing using the iRRAM package, which guarantees error bounds.
Vorheriger Artikel New techniques for linear arithmetic: cubes and equalities
Nächster Artikel Solving quantified linear arithmetic by counterexample-guided instantiation

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 "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

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
Anhänge
Nur mit Berechtigung zugänglich
Fußnoten
Literatur
1.
Alliot JM, Gotteland JB, Vanaret C, Durand N, Gianazza D (2012) Implementing an interval computation library for OCaml on x86/amd64 architectures. In: OUD 2012, OCaml users and developers workshop
2.
Barr ET, Vo T, Le V, Su Z (2013) Automatic detection of floating-point exceptions. In: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, ACM, New York, POPL ’13, pp 549–560
3.
Benhamou F, Granvilliers L (2006) Continuous and interval constraints. In: Rossi F, Pv B, Walsh T (eds) Handbook of constraint programming. Elsevier, New York, pp 571–604CrossRef
4.
Bofill M, Nieuwenhuis R, Oliveras A, Rodríguez-Carbonell E, Rubio A (2008) The barcelogic SMT solver. In: Gupta A, Malik S (eds) Computer aided verification. Springer, Berlin, pp 294–298CrossRef
5.
Brain M, D’Silva V, Griggio A, Haller L, Kroening D (2014) Deciding floating-point logic with abstract conflict driven clause learning. Form Methods Syst Des 45:213–245CrossRefMATH
6.
Comba JLD, Stolfi J (1993) Affine arithmetic and its applications to computer graphics. In: SIBGRAPI’93, pp 9–18
7.
8.
D’Silva V, Haller L, Kroening D, Tautschnig M (2012) Numeric bounds analysis with conflict-driven learning. In: Flanagan C, König B (eds) Tools and algorithms for the construction and analysis of systems. Springer, Berlin, pp 48–63CrossRef
9.
D’Silva V, Haller L, Kroening D (2013) Abstract conflict driven learning. In: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on principles of programming languages, ACM, New York, POPL ’13, pp 143–154
10.
Dutertre B, de Moura L (2006) A fast linear-arithmetic solver for DPLL(T). In: Ball T, Jones RB (eds) Computer aided verification. Springer, Berlin, pp 81–94CrossRef
11.
Eén N, Sörensson N (2004) An extensible SAT-solver. In: Giunchiglia E, Tacchella A (eds) Theory and applications of satisfiability testing. Springer, Berlin, pp 502–518CrossRef
12.
Florian C, Ulrich L, Sebastian J, Erika Á (2012) SMT-RAT: an SMT-compliant nonlinear real arithmetic toolbox. In: Alessandro C, Roberto S (eds) Theory and applications of satisfiability testing–SAT 2012. Springer, Berlin, pp 442–448
13.
Fränzle M, Herde C, Teige T, Ratschan S, Schubert T (2007) Efficient solving of large non-linear arithmetic constraint systems with complex boolean structure. J Satisf Boolean Model Comput 1:209–236MATH
14.
Ganai M, Ivancic F (2009) Efficient decision procedure for non-linear arithmetic constraints using cordic. In: Formal methods in computer-aided design, 2009. FMCAD 2009, pp 61–68
15.
Gao S, Kong S, Clarke E (2013a) dReal: an SMT solver for nonlinear theories over the reals. In: Bonacina M (ed) Automated deduction–CADE-24. Springer, Berlin, pp 208–214CrossRef
16.
Gao S, Kong S, Clarke EM (2013) Satisfiability modulo ODEs. Form Methods Comput Aided Des (FMCAD) 2013:105–112
17.
Goldsztejn A (2006) A branch and prune algorithm for the approximation of non-linear ae-solution sets. In: Proceedings of the 2006 ACM symposium on applied computing, ACM, New York, USA, pp 1650–1654
18.
Granvilliers L, Benhamou F (2006) RealPaver: an interval solver using constraint satisfaction techniques. ACM Trans Math Softw 32:138–156MathSciNetCrossRefMATH
19.
Haller L, Griggio A, Brain M, Kroening D (2012) Deciding floating-point logic with systematic abstraction. In: 2012 formal methods in computer-aided design (FMCAD), pp 131–140
20.
Ishii D, Goldsztejn A, Jermann C (2012) Interval-based projection method for under-constrained numerical systems. Constraints 17:432–460MathSciNetCrossRefMATH
21.
Jovanović D, de Moura L (2012) Solving non-linear arithmetic. In: Gramlich B, Miller D, Sattler U (eds) Automated reasoning. Springer, Berlin, pp 339–354CrossRef
22.
Khanh TV, Ogawa M (2012) SMT for polynomial constraints on real numbers. Electron Notes Theor Comput Sci 289:27–40 (third Workshop on Tools for Automatic Program Analysis (TAPAS’ 2012))CrossRef
23.
Loup U, Scheibler K, Corzilius F, Ábrahám E, Becker B (2013) A symbiosis of interval constraint propagation and cylindrical algebraic decomposition. In: Bonacina MP (ed) Automated deduction–CADE-24. Springer, Berlin, pp 193–207CrossRef
24.
Messine F (2002) Extentions of affine arithmetic: application to unconstrained global optimization. J Univers Comput Sci 8:992–1015MathSciNetMATH
25.
Miyajima S, Miyata T, Kashiwagi M (2003) A new dividing method in affine arithmetic. IEICE Trans Fundam Electron Commun Comput Sci E86–A:2192–2196
26.
Moore R (1966) Interval analysis. Prentice-Hall, Englewood CliffsMATH
27.
Neumaier A (1990) Interval methods for systems of equations. Cambridge University Press, CambridgeMATH
28.
Ngoc DTB, Ogawa M (2009) Overflow and roundoff error analysis via model checking. In: Proceedings of the 2009 seventh IEEE international conference on software engineering and formal methods, IEEE computer society, Washington, SEFM ’09, pp 105–114
29.
Nieuwenhuis R, Oliveras A, Tinelli C (2006) Solving SAT and SAT modulo theories: from an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T). J ACM 53:937–977MathSciNetCrossRefMATH
30.
Passmore GO (2011) Combined decision procedures for nonlinear arithmetics, real and complex. Dissertation, School of informatics, University of Edinburgh
31.
Passmore GO, Jackson PB (2009) Combined decision techniques for the existential theory of the reals. In: Carette J, Dixon L, Coen CS, Watt SM (eds) Intelligent computer mathematics. Springer, Berlin, pp 122–137CrossRef
32.
Ratschan S (2006) Efficient solving of quantified inequality constraints over the real numbers. ACM Trans Comput Log 7:723–748MathSciNetCrossRefMATH
33.
34.
Stolfi J, Figueiredo LHD (1997) Self-validated numerical methods and applications. In: Monograph for 21st Brazilian mathematics colloquium
35.
Sturm T (2015) Subtropical real root finding. In: Proceedings of the 2015 ACM on international symposium on symbolic and algebraic computation, ACM, New York, ISSAC ’15, pp 347–354
36.
Tseitin G (1983) On the complexity of derivation in propositional calculus. In: Siekmann JH, Wrightson G (eds) Automation of reasoning, symbolic computation. Springer, Berlin
37.
Tung VX, Van Khanh T, Ogawa M (2016) raSAT: an SMT solver for polynomial constraints. In: Olivetti N, Tiwari A (eds) Automated reasoning. Springer, Cham, pp 228–237
38.
Zankl H, Middeldorp A (2010) Satisfiability of non-linear (ir)rational arithmetic. In: Clarke EM, Voronkov A (eds) Logic for programming, artificial intelligence, and reasoning. Springer, Berlin, pp 481–500CrossRef
Metadaten
Titel
raSAT: an SMT solver for polynomial constraints
verfasst von
Vu Xuan Tung
To Van Khanh
Mizuhito Ogawa
Publikationsdatum
27.06.2017
Verlag
Springer US
Erschienen in
Formal Methods in System Design / Ausgabe 3/2017
Print ISSN: 0925-9856
Elektronische ISSN: 1572-8102
DOI
https://doi.org/10.1007/s10703-017-0284-9

Weitere Artikel der Ausgabe 3/2017

Formal Methods in System Design 3/2017 Zur Ausgabe

OriginalPaper

Propagation based local search for bit-precise reasoning

OriginalPaper

NP-completeness of small conflict set generation for congruence closure

OriginalPaper

New techniques for linear arithmetic: cubes and equalities

OriginalPaper

Compositional entailment checking for a fragment of separation logic

OriginalPaper

Cardinality constraints for arrays (decidability results and applications)

OriginalPaper

Solving quantified linear arithmetic by counterexample-guided instantiation

Premium Partner

    Bildnachweise