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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Balyo, T., Heule, M. J., Järvisalo, M., et al.: Proceedings of SAT Competition 2016. Department of Computer Science, University of Helsinki (2016)
Balyo, T., Heule, M.J., Järvisalo, M., et al.: Proceedings of SAT Competition 2017. Department of Computer Science, University of Helsinki (2017)
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)
Brickenstein, M., Dreyer, A.: PolyBoRi: a framework for Gröbner basis computations with Boolean polynomials. J. Symbolic Comput. 44, 1326–1345 (2009)
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_17
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)
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_11
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)
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)
Horáček, J., Kreuzer, M., Messeng Ekossono, A.S.: A signature based border basis algorithm. In: Conference on Algebraic Informatics, CAI, Kalamata (2017)
Hovinen, B., Martani, F.: LELA: library for exact linear algebra (2011). https://github.com/Singular/LELA
Kehrein, A., Kreuzer, M.: Computing border bases. J. Pure Appl. Algebra 205(2), 279–295 (2006)
Schubert, T., Reimer, S.: antom (2016). https://projects.informatik.uni-freiburg.de/projects/antom
The ApCoCoA Team. ApCoCoA: Applied Computations in Commutative Algebra. http://apcocoa.uni-passau.de
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).
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer International Publishing AG, part of Springer Nature
About this paper
Cite this paper
Horáček, J., Kreuzer, M. (2018). 3BA: A Border Bases Solver with a SAT Extension. In: Davenport, J., Kauers, M., Labahn, G., Urban, J. (eds) Mathematical Software – ICMS 2018. ICMS 2018. Lecture Notes in Computer Science(), vol 10931. Springer, Cham. https://doi.org/10.1007/978-3-319-96418-8_25
Download citation
DOI: https://doi.org/10.1007/978-3-319-96418-8_25
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-96417-1
Online ISBN: 978-3-319-96418-8
eBook Packages: Computer ScienceComputer Science (R0)