SWORD – Module-based SAT Solving

Authors Robert Wille, Jean Christoph Jung, Andre Sülflow, Rolf Drechsler



PDF
Thumbnail PDF

File

DagSemProc.09461.5.pdf
  • Filesize: 85 kB
  • 2 pages

Document Identifiers

Author Details

Robert Wille
Jean Christoph Jung
Andre Sülflow
Rolf Drechsler

Cite AsGet BibTex

Robert Wille, Jean Christoph Jung, Andre Sülflow, and Rolf Drechsler. SWORD – Module-based SAT Solving. In Algorithms and Applications for Next Generation SAT Solvers. Dagstuhl Seminar Proceedings, Volume 9461, pp. 1-2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)
https://doi.org/10.4230/DagSemProc.09461.5

Abstract

In the paper, SWORD is described – a decision procedure for bit-vector logic that uses SAT techniques and exploits word level information. The main idea of SWORD is based on the following observation: While current SAT solvers perform very well on instances with a large number of logic operations, their performance on arithmetic operations degrades with increasing data-path width. In contrast, pure word-level approaches are able to handle arithmetic operations very fast, but suffer from irregularities in the word-level structure (e.g. bit slicing). SWORD tries to combine the best of both worlds: On the one hand, it includes fast propagation, sophisticated data structures, as well as advanced techniques like non-chronological backtracking and learning from modern SAT solvers. On the other hand word-level information is exploited in the decision heuristic and during propagation.
Keywords
  • SAT Solver
  • Word Level
  • SAT Modulo Theories

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail