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
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben
Journal of Automated Reasoning
Erschienen in: Journal of Automated Reasoning 1/2020

05.12.2018

A Conflict-Driven Solving Procedure for Poly-Power Constraints

verfasst von: Cheng-Chao Huang, Ming Xu, Zhi-Bin Li

Erschienen in: Journal of Automated Reasoning | Ausgabe 1/2020

Einloggen

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

search-config
loading …

Abstract

This paper studies the satisfiability problem of poly-power constraints (conjunctions of poly-power equations and inequalities), in which poly-powers are univariate nonlinear functions that extend integer exponents of polynomials to real algebraic exponents. To solve the poly-power constraint, we present a sound and complete procedure that incorporates conflict-driven learning with the exclusion algorithm for isolating positive roots of poly-powers. Furthermore, we introduce a kind of optimal interval-splitting, based on the Stern–Brocot tree and on binary rational numbers respectively, so that the operands occurring in the execution are chosen to be as simple as possible. The solving procedure, thereby, turns out to be promisingly efficient on randomly generated examples.
Nächster Artikel ExpTime Tableaux with Global Caching for Hybrid PDL

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
Literatur
1.
Achatz, M., McCallum, S., Weispfenning, V.: Deciding polynomial–exponential problems. In: Sendra, J.R., González-Vega, L. (eds.) Proceedings of the 33rd ISSAC, pp. 215–222. ACM Press, New York (2008)
2.
Akbarpour, B., Paulson, L.C.: MetiTarski: an automatic theorem prover for real-valued special functions. J. Autom. Reason. 44(3), 175–205 (2010)MathSciNetCrossRef
3.
4.
Bonacina, M.P., Graham-Lengrand, S., Shankar, N.: Satisfiability modulo theories and assignments. In: de Moura, L. (ed.) Proceedings of the 26th CADE, LNCS, vol. 10395, pp. 42–59. Springer, New York (2017)CrossRef
5.
Bromberger, M., Sturm, T., Weidenbach, C.: Linear integer arithmetic revisited. In: Felty, A.P., Middeldorp, A. (eds.) Proceedings of the 25th CADE, LNCS, vol. 9195, pp. 623–637. Springer, New York (2015)CrossRef
6.
Cimatti, A., Griggio, A., Irfan, A., Roveri, M., Sebastiani, R.: Satisfiability modulo transcendental functions via incremental linearization. In: de Moura, L. (ed.) Proceedings of the 26th CADE, LNCS, vol. 10395, pp. 95–113. Springer, New York (2017)CrossRef
7.
Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT Solver. In: Piterman, N., Smolka, S.A. (eds.) Proceedings of the 19th TACAS, LNCS, vol. 7795, pp. 93–107. Springer, New York (2013)CrossRef
8.
Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decomposition. In: Barkhage, H. (ed.) Proceedings of the 2nd GI Conference on Automata Theory and Formal Languages, LNCS, vol. 33, pp. 134–183. Springer, New York (1975)
9.
Collins, G.E., Loos, R.: Polynomial real root isolation by differentiation. In: Jenks, R.D. (ed.) Proceedings of the 3rd SYMSAC, pp. 15–25. ACM Press, New York (1976)
10.
Davis, M., Logemann, G., Loveland, D.: A machine program for theorem-proving. Commun. ACM 5(7), 394–397 (1962)MathSciNetCrossRef
11.
12.
de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Proceedings of the 14th TACAS, LNCS, vol. 4963, pp. 337–340. Springer, New York (2008)
13.
de Moura, L., Passmore, G.O.: Computation in real closed infinitesimal and transcendental extensions of the rationals. In: Bonacina, M.P. (ed.) Proceedings of the 24th CADE, LNCS, vol. 7898, pp. 178–192. Springer, New York (2013)
14.
Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) Proceedings of the 18th CAV, LNCS, vol. 4144, pp. 81–94. Springer, New York (2006)CrossRef
15.
Giunchiglia, F., Sebastiani, R.: Building decision procedures for modal logics from propositional decision procedures: the case study of modal K(m). Inf. Comput. 162(1–2), 158–178 (2000)MathSciNetCrossRef
16.
Graham, R.L., Knuth, D.E., Patashnik, O.: Concrete Mathematics: A Foundation for Computer Science, 2nd edn. Addison-Wesley, New York (1994)MATH
17.
18.
Huang, C.C., Li, J.C., Xu, M., Li, Z.B.: Positive root isolation for poly-powers by exclusion and differentiation. J. Symb. Comput. 85, 148–169 (2018)MathSciNetCrossRef
19.
Jovanović, D., de Moura, L.: Solving non-linear arithmetic. In: Gramlich, B., Miller, D., Sattler, U. (eds.) Proceedings of the 6th IJCAR, LNCS, vol. 7364, pp. 339–354. Springer, New York (2012)CrossRef
20.
Jovanović, D., de Moura, L.: Cutting to the chase-solving linear integer arithmetic. J. Autom. Reason. 51(1), 79–108 (2013)CrossRef
21.
Kailath, T.: Linear Systems. Prentice Hall, Upper Saddle River (1980)MATH
22.
Kaltofen, E.: Polynomial-time reductions from multivariate to bi- and univariate integral polynomial factorization. SIAM J. Comput. 14(2), 469–489 (1985)MathSciNetCrossRef
23.
Kroening, D., Strichman, O.: Decision Procedures—An Algorithmic Point of View, 2nd edn. Springer, Berlin (2016)CrossRef
24.
Loos, R.: Computing in algebraic extensions. In: Buchberger, B., Collins, G.E., Loos, R. (eds.) Computer Algebra: Symbolic and Algebraic Computation, pp. 173–187. Springer, New York (1983)CrossRef
25.
Loup, U., Scheibler, K., Corzilius, F., Ábrahám, E., Becker, B.: A symbiosis of interval constraint propagation and cylindrical algebraic decomposition. In: Bonacina, M.P. (ed.) Proceedings of the 24th CADE, LNCS, vol. 7898, pp. 193–207. Springer, New York (2013)CrossRef
26.
Marques-Silva, J.P., Sakallah, K.A.: GRASP: a search algorithm for propositional satisfiability. IEEE Trans. Comput. 48(5), 506–521 (1999)MathSciNetCrossRef
27.
McCallum, S., Weispfenning, V.: Deciding polynomial–transcendental problems. J. Symb. Comput. 47(1), 16–31 (2012)MathSciNetCrossRef
28.
Nieuwenhuis, R., Oliveras, A., Tinelli, C.: Solving SAT and SAT modulo theories: from an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(T). JACM 53(6), 937–977 (2006)MathSciNetCrossRef
29.
Passmore, G.O.: Decidability of univariate real algebra with predicates for rational and integer powers. In: Felty, A.P., Middeldorp, A. (eds.) Proceedings of the 25th CADE, LNCS, vol. 9195, pp. 181–196. Springer, New York (2015)CrossRef
30.
Rouillier, F.: Solving zero-dimensional systems through the rational univariate representation. Appl. Algebra Eng. Commun. Comput. 9(5), 433–461 (1999)MathSciNetCrossRef
31.
She, Z., Li, H., Xue, B., Zheng, Z., Xia, B.: Discovering polynomial Lyapunov functions for continuous dynamical systems. J. Symb. Comput. 58, 41–63 (2013)MathSciNetCrossRef
32.
Siegel, C.L.: Transcendental Numbers. Princeton University Press, Princeton (1949)MATH
33.
Strzeboński, A.: Real root isolation for exp–log functions. In: Sendra, J.R., González-Vega, L. (eds.) Proceedings of the 33rd ISSAC, pp. 303–313. ACM Press, New York (2008)
34.
Strzeboński, A.: Real root isolation for tame elementary functions. In: Johnson, J.R., Park, H., Kaltofen, E. (eds.) Proceedings of the 34th ISSAC, pp. 341–350. ACM Press, New York (2009)
35.
36.
Xia, B., Yang, L.: An algorithm for isolating the real solutions of semi-algebraic systems. J. Symb. Comput. 34(5), 461–477 (2002)MathSciNetCrossRef
37.
Xu, M., Li, Z.B., Yang, L.: Quantifier elimination for a class of exponential polynomial formulas. J. Symb. Comput. 68(1), 146–168 (2015)MathSciNetCrossRef
38.
Yun, D.Y.Y.: On squarefree decomposition algorithms. In: Jenks, R.D. (ed.) Proceedings of the 3rd SYMSAC, pp. 26–35. ACM Press, New York (1976)
Metadaten
Titel
A Conflict-Driven Solving Procedure for Poly-Power Constraints
verfasst von
Cheng-Chao Huang
Ming Xu
Zhi-Bin Li
Publikationsdatum
05.12.2018
Verlag
Springer Netherlands
Erschienen in
Journal of Automated Reasoning / Ausgabe 1/2020
Print ISSN: 0168-7433
Elektronische ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-018-09501-z

Weitere Artikel der Ausgabe 1/2020

Journal of Automated Reasoning 1/2020 Zur Ausgabe

OriginalPaper

Politeness and Combination Methods for Theories with Bridging Functions

OriginalPaper

Automating Free Logic in HOL, with an Experimental Application in Category Theory

OriginalPaper

Priority Inheritance Protocol Proved Correct

OriginalPaper

ExpTime Tableaux with Global Caching for Hybrid PDL

OriginalPaper

A Prover Dealing with Nominals, Binders, Transitivity and Relation Hierarchies

Premium Partner

    Bildnachweise