On conversions from CNF to ANF.

In this paper we discuss conversion methods from the conjunctive normal form (CNF) to the algebraic normal form (ANF) of a Boolean function. Whereas the reverse conversion has been studied before, the CNF to ANF conversion has been achieved predominantly via a standard method which tends to produce many polynomials of high degree. Based on a block-building mechanism, we design a new blockwise algorithm for the CNF to ANF conversion which is geared towards producing fewer and lower degree polynomials. In particular, we look for as many linear polynomials as possible in the converted system and check that our algorithm finds them. As an application, we suggest a new algebraic extension of the resolution calculus which is tailored to the output of the standard CNF to ANF conversion algorithm. Experiments show that the ANF produced by our algorithm outperforms the standard conversion in "real life" examples originating from cryptographic attacks, and that our algebraic resolution algorithm solves some SAT instances which are notoriously hard for SAT solvers. [ABSTRACT FROM AUTHOR]