Integrating algebraic and SAT solvers

Abstract

For solving systems of Boolean polynomials whose zeros are known to be contained in F2n, algebraic solvers such as the Boolean Border Basis Algorithm (BBBA) and SAT solvers use very different and possibly complementary methods to create new information. Based on suitable implementations of these solvers and conversion methods from Boolean polynomials to SAT clauses and back, we describe an automatic framework integrating the two solving techniques and exchanging newly found information between them. Using examples derived from cryptographic attacks, we present some initial experiments indicating the efficiency of this combination.