nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Reducing Bit-Vector Polynomials to SAT Using Gröbner Bases

verfasst von : Thomas Seed, Andy King, Neil Evans

Erschienen in: Theory and Applications of Satisfiability Testing – SAT 2020

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

We address the satisfiability of systems of polynomial equations over bit-vectors. Instead of conventional bit-blasting, we exploit word-level inference to translate these systems into non-linear pseudo-boolean constraints. We derive the pseudo-booleans by simulating bit assignments through the addition of (linear) polynomials and applying a strong form of propagation by computing Gröbner bases. By handling bit assignments symbolically, the number of Gröbner basis calculations, along with the number of assignments, is reduced. The final Gröbner basis yields expressions for the bit-vectors in terms of the symbolic bits, together with non-linear pseudo-boolean constraints on the symbolic variables, modulo a power of two. The pseudo-booleans can be solved by translation into classical linear pseudo-boolean constraints (without a modulo) or by encoding them as propositional formulae, for which a novel translation process is described.

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 Taming High Treewidth with Abstraction, Nested Dynamic Programming, and Database Technology

Nächstes Kapitel Speeding up Quantified Bit-Vector SMT Solvers by Bit-Width Reductions and Extensions

Ábráham, E.: Building bridges between symbolic computation and satisfiability checking. In: International Symposium on Symbolic and Algebraic Computation, pp. 1–6. ACM Press (2015)

Adams, W., Loustaunau, P.: An Introduction to Gröbner Bases. American Mathematical Society, Providence (1994)CrossRef

Backeman, P., Rümmer, P., Zeljic, A.: Bit-vector interpolation and quantifier elimination by lazy reduction. In: Formal Methods in Computer Aided Design, pp. 1–10. IEEE (2018)

Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22110-1_14CrossRef

Brickenstein, M., Dreyer, A., Greuel, G., Wedler, M., Wienand, O.: New developments in the theory of Gröbner bases and applications to formal verification. J. Pure Appl. Algebra 213, 1612–1635 (2009)MathSciNetCrossRef

Brown, C.: Bridging two communities to solve real problems. In: International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, pp. 11–14. IEEE Press (2016)

Buchberger, B.: Bruno Buchberger’s PhD thesis 1965: an algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal. J. Symb. Comput. 41, 475–511 (2006)CrossRef

Collins, G.E.: Quantifier elimination for real closed fields by cylindrical algebraic decompostion. In: Brakhage, H. (ed.) GI-Fachtagung 1975. LNCS, vol. 33, pp. 134–183. Springer, Heidelberg (1975). https://doi.org/10.1007/3-540-07407-4_17CrossRef

Cox, D., Little, J., O’Shea, D.: Ideals, Varieties and Algorithms. Undergraduate Texts in Mathematics. Springer, Heidelberg (1992). https://doi.org/10.1007/978-1-4757-2181-2CrossRefMATH

10.

Davenport, J.H., England, M., Griggio, A., Sturm, T., Tinelli, C.: Symbolic computation and satisfiability checking. J. Symb. Comput. (2019). https://doi.org/10.1016/j.jsc.2019.07.017

11.

Faugére, J.: A new efficient algorithm for computing Gröbner bases (F4). J. Pure Appl. Algebra 139(1–3), 61–88 (1999)MathSciNetCrossRef

12.

Faugére, J.: A new efficient algorithm for computing Gröbner bases without reduction to zero (F5). In: International Symposium on Symbolic and Algebraic Computation, pp. 75–83 (2002)

13.

Fekete, Y., Codish, M.: Simplifying pseudo-boolean constraints in residual number systems. In: Sinz, C., Egly, U. (eds.) SAT 2014. LNCS, vol. 8561, pp. 351–366. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-09284-3_26CrossRef

14.

Griggio, A.: Effective word-level interpolation for software verification. In: Formal Methods in Computer-Aided Design, pp. 28–36. IEEE (2011)

15.

Horáček, J., Burchard, J., Becker, B., Kreuzer, M.: Integrating algebraic and SAT solvers. In: Blömer, J., Kotsireas, I.S., Kutsia, T., Simos, D.E. (eds.) MACIS 2017. LNCS, vol. 10693, pp. 147–162. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-72453-9_11CrossRefMATH

16.

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

17.

Kaufmann, D., Biere, A., Kauers, M.: Verifying large multipliers by combining SAT and computer algebra. In: Formal Methods in Computer-Aided Design, pp. 28–36 (2019)

18.

Lang, S.: Algebra. Graduate Texts in Mathematics. Springer, Heidelberg (2002). https://doi.org/10.1007/978-1-4613-0041-0CrossRefMATH

19.

Manquinhoand, V.M., Marques-Silva, J.: Using cutting planes in pseudo-boolean optimization. J. Satisf. Boolean Model. Comput. 2, 199–208 (2006)

20.

Michel, L.D., Van Hentenryck, P.: Constraint satisfaction over bit-vectors. In: Milano, M. (ed.) CP 2012. LNCS, pp. 527–543. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-33558-7_39CrossRef

21.

Müller-Olm, M., Seidl, H.: Analysis of modular arithmetic. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 46–60. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-31987-0_5CrossRef

22.

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(6), 937–977 (2006)MathSciNetCrossRef

23.

Viehmann, T., Kremer, G., Ábráham, E.: Comparing different projection operators in the cylindrical algebraic decomposition for SMT solving. In: International Workshop on Satisfiability Checking and Symbolic Computation (2017). http://www.sc-square.org/CSA/workshop2-papers/RP2-FinalVersion.pdf

24.

Tseytin, G.S.: On the complexity of derivation in propositional calculus. In: Slisenko, A.O. (ed.) Studies in Constructive Mathematics and Mathematical Logic, pp. 115–125. Steklov Mathematical Institute (1970). Translated from Russian: Zapiski Nauchnykh Seminarov LOMI 8 (1968)

25.

Wang, W., Søndergaard, H., Stuckey, P.J.: Wombit: a portfolio bit-vector solver using word-level propagation. J. Autom. Reasoning 63(3), 723–762 (2018). https://doi.org/10.1007/s10817-018-9493-1MathSciNetCrossRefMATH

26.

Warren, H.: Hacker’s Delight. Addison-Wesley, Boston (2012)

Titel: Reducing Bit-Vector Polynomials to SAT Using Gröbner Bases
verfasst von: Thomas Seed
Andy King
Neil Evans
Verlag: Springer International Publishing
Buch: Theory and Applications of Satisfiability Testing – SAT 2020
Print ISBN: 978-3-030-51824-0

Electronic ISBN: 978-3-030-51825-7

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-51825-7_26

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"