• Classified by Research Topic • Sorted by Date • Classified by Publication Type •
Bosphorus: Bridging ANF and CNF Solvers.
Davin Choo, Mate Soos, Kian Ming A. Chai and Kuldeep S. Meel.
In Proceedings of Design, Automation, and Test in Europe(DATE), March 2019.
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 emphlearn 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.
@inproceedings{CSCM19,
title={Bosphorus: Bridging ANF and CNF Solvers},
author={
Choo, Davin and Soos, Mate and A. Chai, Kian Ming and Meel, Kuldeep S.
},
bib2html_pubtype={Refereed Conference},
bib2html_dl_pdf={../Papers/date-cscm19.pdf},
code={https://github.com/meelgroup/bosphorus},
month=mar,
booktitle=DATE,
year={2019},
bib2html_rescat={Solver Engineering},
abstract={
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.
},
}
Generated by bib2html.pl (written by Patrick Riley with layout from Sanjit A. Seshia ) on Thu Apr 30, 2026 09:22:03