zbMATH — the first resource for mathematics

Integrating algebraic and SAT solvers. (English) Zbl 07036049
Blömer, Johannes (ed.) et al., Mathematical aspects of computer and information sciences. 7th international conference, MACIS 2017, Vienna, Austria, November 15–17, 2017. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10693, 147-162 (2017).
Summary: For solving systems of Boolean polynomials whose zeros are known to be contained in \(\mathbb{F}_2^n\), 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.
For the entire collection see [Zbl 1381.68002].

68-XX Computer science
PDF BibTeX Cite
Full Text: DOI