zbMATH — the first resource for mathematics

3BA: a border bases solver with a SAT extension. (English) Zbl 1395.68345
Davenport, James H. (ed.) et al., Mathematical software – ICMS 2018. 6th international conference, South Bend, IN, USA, July 24–27, 2018. Proceedings. Cham: Springer (ISBN 978-3-319-96417-1/pbk; 978-3-319-96418-8/ebook). Lecture Notes in Computer Science 10931, 209-217 (2018).
Summary: 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.
For the entire collection see [Zbl 1391.68004].
68W30 Symbolic computation and algebraic computation
68T15 Theorem proving (deduction, resolution, etc.) (MSC2010)
Full Text: DOI