Bosphorus: Bridging ANF and CNF Solvers
2019 Design, Automation & Test in Europe Conference & Exhibition (DATE)(2019)
摘要
Algebraic Normal Form (ANF) and Conjunctive Normal Form (CNF) are commonly used to encode problems in Boolean algebra. ANFs are typically solved via Grobner 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 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.
更多查看译文
关键词
CNF solving techniques,bosphorus,CNF solvers,Boolean algebra,Grobner basis algorithms,SAT solvers,algebraic normal form,conjunctive normal form,ANF solvers
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要