@COMMENT This file was generated by bib2html.pl <https://sourceforge.net/projects/bib2html/> version 0.94
@COMMENT written by Patrick Riley <http://sourceforge.net/users/patstg/>
@COMMENT This file came from Kuldeep S. Meel's publication pages at
@COMMENT http://www.comp.nus.edu.sg/~meel/publications/
@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.
  },
}