BOSPHORUS: Bridging ANF and CNF Solvers

TL;DR

This paper introduces a novel paradigm that combines ANF and CNF solving techniques through iterative fact learning, significantly improving solver performance across diverse benchmarks.

Contribution

It proposes a new bridging approach that leverages iterative fact learning to enhance algebraic and SAT solving methods, enabling better problem-solving efficiency.

Findings

Learnt facts improve runtime performance.

More benchmarks are solvable with the new approach.

Significant performance gains across multiple domains.

Abstract

Algebraic Normal Form (ANF) and Conjunctive Normal Form (CNF) are commonly used to encode problems in Boolean algebra. ANFs are typically solved via Gr"obner basis algorithms, often using more memory than is feasible; while CNFs are solved using SAT solvers, which cannot exploit the algebra of polynomials naturally. We propose a paradigm that bridges between ANF and CNF solving techniques: the techniques are applied in an iterative manner to emph{learn facts} to augment the original problems. Experiments on over 1,100 benchmarks arising from four different applications domains demonstrate that learnt facts can significantly improve runtime and enable more benchmarks to be solved.