CafeSat: a Modern SAT Solver for Scala

We present CafeSat, a SAT solver written in the Scala programming language. CafeSat is a modern solver based on DPLL and featuring many state-of-the-art techniques and heuristics. It uses two-watched literals for Boolean constraint propagation, conflict-driven learning along with clause deletion, a restarting strategy, and the VSIDS heuristics for choosing the branching literal. CafeSat is both sound and complete. In order to achieve reasonable performance, low level and hand-tuned data structures are extensively used. We report experiments that show that significant speedup can be obtained from translating a high level algorithm written in a relatively idiomatic Scala style to a more C-like programming style. These experiments also illustrate the importance of modern techniques used by SAT solver. Finally, we evaluate CafeSat against the reference SAT solver on the JVM: Sat4j.


Published in:
Proceedings of the 4th Workshop on Scala - SCALA '13, 1-4
Presented at:
the 4th Scala Workshop, Montpellier, France, 02 07 2013
Year:
2013
Publisher:
New York, New York, USA, ACM Press
ISBN:
978-1-4503-2064-1
Keywords:
Laboratories:




 Record created 2013-07-30, last modified 2018-03-17

Postprint:
Download fulltextPDF
presentation slides:
Download fulltextPDF
External link:
Download fulltextURL
Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)