BOSPHORUS：桥接ANF和CNF求解器
BOSPHORUS: Bridging ANF and CNF Solvers
摘要：
代数范式（ANF）和合取范式（CNF）是布尔代数中常用的编码问题。ANF通常通过Gr 'obner基算法求解，通常使用比可行的更多的内存;而CNF使用SAT求解器求解，这无法自然地利用多项式代数。我们提出了一个范例，ANF和CNF解决技术之间的桥梁：技术应用在迭代的方式来学习事实，以增加原来的问题。对来自四个不同应用领域的1,100多个基准测试的实验表明，学习事实可以显着提高运行时间，并使更多的基准测试得以解决。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
