Advertisement

3BA: A Border Bases Solver with a SAT Extension

  • Jan HoráčekEmail author
  • Martin Kreuzer
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10931)

Abstract

Many search problems over Boolean variables can be formulated in terms of satisfiability of a set of clauses or solving a system of Boolean polynomials. On one hand, there exists a great variety of software coming from different areas such as commutative algebra, SAT or SMT, that can be used to tackle these instances. On the other hand, their approaches to inferring new constraints vary and seem to be complementary to each other. For instance, compare the handling of XOR constraints in SAT solvers to that in computer algebra systems. We present a C++ implementation of a platform that combines the power of the Boolean Border Basis Algorithm (BBBA) with a CDCL SAT solver in a portfolio-based fashion. Instead of building a complete fusion or a theory solver for a particular problem, both solvers work independently and interact through a communication interface. Hence a greater degree of flexibility is achieved. The SAT solver antom, which is currently used in the integration, can be easily replaced by any other CDCL solver. Altogether, this is the first open-source implementation of the BBBA and its combination with a SAT solver.

Keywords

Boolean Border Basis Algorithm Boolean polynomial Cryptographic attack SAT solving 

Notes

Acknowledgments

The authors are grateful to Tobias Schubert for providing us the SAT solver antom [13] and Jan Burchard for making the communication between antom and 3BA possible. John Abbott and Anna Bigatti gave us useful feedback on our C++ implementation. This work was financially supported by the DFG project “Algebraische Fehlerangriffe” [KR 1907/6-2] and partially supported by the H2020-FETOPEN-2015-CSA project \(\text {SC}^2\) (712689).

References

  1. 1.
    Balyo, T., Heule, M. J., Järvisalo, M., et al.: Proceedings of SAT Competition 2016. Department of Computer Science, University of Helsinki (2016)Google Scholar
  2. 2.
    Balyo, T., Heule, M.J., Järvisalo, M., et al.: Proceedings of SAT Competition 2017. Department of Computer Science, University of Helsinki (2017)Google Scholar
  3. 3.
    Boyer, B., Eder, C., Faugère, J.-C., Lachartre, S., Martani, F.: GBLA: Gröbner basis linear algebra package. In: Proceedings of the ACM on International Symposium on Symbolic and Algebraic Computation, pp. 135–142. ACM (2016)Google Scholar
  4. 4.
    Brickenstein, M., Dreyer, A.: PolyBoRi: a framework for Gröbner basis computations with Boolean polynomials. J. Symbolic Comput. 44, 1326–1345 (2009)MathSciNetCrossRefGoogle Scholar
  5. 5.
    Faugère, J.-C.: FGb: a library for computing Gröbner bases. In: Fukuda, K., Hoeven, J., Joswig, M., Takayama, N. (eds.) ICMS 2010. LNCS, vol. 6327, pp. 84–87. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-15582-6_17CrossRefGoogle Scholar
  6. 6.
    Gay, M., Burchard, J., Horáček, J., Messeng Ekossono, A.S., Schubert, T., Becker, B., Kreuzer, M., Polian, I.: Small scale AES toolbox: algebraic and propositional formulas, circuit-implementations and fault equations. In: Conference on Trustworthy Manufacturing and Utilization of Secure Devices (TRUDEVICE 2016), Barcelona (2016)Google Scholar
  7. 7.
    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_11CrossRefGoogle Scholar
  8. 8.
    Horáček, J., Kreuzer, M.: On conversions from CNF to ANF. In: 2th International Workshop on Satisfiability Checking and Symbolic Computation, SC-square, Kaiserslautern (2017)Google Scholar
  9. 9.
    Horáček, J., Kreuzer, M., Messeng Ekossono, A.S.: Computing Boolean border bases. In: 18th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC, Timisoara, pp. 465–472. IEEE (2016)Google Scholar
  10. 10.
    Horáček, J., Kreuzer, M., Messeng Ekossono, A.S.: A signature based border basis algorithm. In: Conference on Algebraic Informatics, CAI, Kalamata (2017)Google Scholar
  11. 11.
    Hovinen, B., Martani, F.: LELA: library for exact linear algebra (2011). https://github.com/Singular/LELA
  12. 12.
    Kehrein, A., Kreuzer, M.: Computing border bases. J. Pure Appl. Algebra 205(2), 279–295 (2006)MathSciNetCrossRefGoogle Scholar
  13. 13.
    Schubert, T., Reimer, S.: antom (2016). https://projects.informatik.uni-freiburg.de/projects/antom
  14. 14.
    The ApCoCoA Team. ApCoCoA: Applied Computations in Commutative Algebra. http://apcocoa.uni-passau.de

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  1. 1.Faculty of Informatics and MathematicsUniversity of PassauPassauGermany

Personalised recommendations