3BA: A Border Bases Solver with a SAT Extension

摘要

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.