Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Conferences, Workshops, Symposiums, and Seminars
  4. CafeSat: a Modern SAT Solver for Scala
 
Loading...
Thumbnail Image
conference paper

CafeSat: a Modern SAT Solver for Scala

Blanc, Régis William  
2013
Proceedings of the 4th Workshop on Scala - SCALA '13
the 4th Scala Workshop

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.

  • Files
  • Details
  • Metrics
Loading...
Thumbnail Image
Name

main.pdf

Type

Postprint

Access type

openaccess

Size

212.25 KB

Format

Adobe PDF

Checksum (MD5)

6f9a07a697f016e02e860929e62850d8

Loading...
Thumbnail Image
Name

main_1.pdf

Access type

openaccess

Size

3.29 MB

Format

Adobe PDF

Checksum (MD5)

f71061f32b92c210f247a0fe48b6f460

Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés