On conversions from CNF to ANF. (September 2020)

• Record Type: Journal Article
• Authors: Horáček, Jan; Kreuzer, Martin
• Is Part Of: Journal of symbolic computation. Volume 100(2020)
• Page Start: 164
• Page End: 186
• Publication Date: 2020-09
• Subjects: Conjunctive normal form -- Algebraic normal form -- Boolean polynomial -- Boolean Gröbner basis -- SAT solving -- Resolution; Mathematics -- Data processing -- Periodicals; Numerical analysis -- Data processing -- Periodicals; Automatic programming (Computer science) -- Periodicals; Mathématiques -- Informatique -- Périodiques; Analyse numérique -- Informatique -- Périodiques; Programmation automatique -- Périodiques; Automatic programming (Computer science); Mathematics -- Data processing; Numerical analysis -- Data processing; Periodicals; Electronic journals; 510.285
• DOI: 10.1016/j.jsc.2019.07.023
• Languages: English
• ISSNs: 0747-7171

Abstract

Abstract: 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.