[PRL] Torture Chamber tomorrow 1:30-2:30

[Ben Chambers]

I will be practicing a 25-minute presentation on CNF Generation which
I will giving at DATE (Design, Automation and Test in Europe) tomorrow
(Friday) from 1:30-1:55 in WVH 164.  I have reserved the room until
3:00 for comments and suggestions, etc.  I appreciate anyone sparing
the time to come and provide some feedback.

Thanks!

- Ben
-----------------

Faster SAT Solving with Better CNF Generation

Boolean satisfiability (SAT) solving has become an enabling technology
with wide-ranging applications in numerous disciplines.  These
applications tend to be most naturally encoded using arbitrary Boolean
expressions, but to use modern SAT solvers, one has to generate
expressions in Conjunctive Normal Form (CNF).  This process can
significantly affect SAT solving times.  In this paper, we introduce a
new linear-time CNF generation algorithm.  We have implemented our
algorithm and have conducted extensive experiments which show that our
algorithm leads to faster SAT solving times, and smaller CNF than
existing approaches.