期刊
JOURNAL OF SYMBOLIC COMPUTATION
卷 100, 期 -, 页码 164-186出版社
ACADEMIC PRESS LTD- ELSEVIER SCIENCE LTD
DOI: 10.1016/j.jsc.2019.07.023
关键词
Conjunctive normal form; Algebraic normal form; Boolean polynomial; Boolean Grobner basis; SAT solving; Resolution
资金
- DFG [KR 1907/6-2]
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. (c) 2019 Elsevier Ltd. All rights reserved.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据