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
Type
conference paper
DOI
10.1145/2489837.2489839
Author(s)
Blanc, Régis William  
Date Issued

2013

Publisher

ACM Press

Publisher place

New York, New York, USA

Journal
Proceedings of the 4th Workshop on Scala - SCALA '13
ISBN of the book

978-1-4503-2064-1

Start page

1

End page

4

Subjects

scala

•

sat solver

•

decision procedure

•

constraint solving

URL

URL

https://github.com/regb/scabolic
Peer reviewed

REVIEWED

Written at

EPFL

EPFL units
LARA  
Event nameEvent placeEvent date
the 4th Scala Workshop

Montpellier, France

02 07 2013

Available on Infoscience
July 30, 2013
Use this identifier to reference this record
https://infoscience.epfl.ch/handle/20.500.14299/93619
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