SWORD – Module-based SAT Solving

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

Thumbnail 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)


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.
  • SAT Solver
  • Word Level
  • SAT Modulo Theories


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads