Logo Universtity of Bremen
LOGO AGRA | AG Rechnerarchitektur

Group of Computer Architecture / AGRA | Computer Science | Faculty 03 | University of Bremen


SWORD - A Module-based SMT Solver

by Rolf Drechsler , Finn Haedicke , Jean Christoph Jung , Andre Sülflow , and Robert Wille

SWORD is an SMT decision procedure that uses SAT techniques and facilitates word level information. Rewriting on bit level and word level is performed in a pre-process and reduce the instance size. The remaining instance is given to a hybrid solve engine.

The solve engine of SWORD employs well-known SAT techniques like unit propagation, non-chronological backtracking and learning. Modules are a special feature of SWORD to exploit word level information in the decision heuristic and during propagation.

On the one hand pre-defined modules for large arithmetic operations are provided, e.g. for multiplication and addition. On the other hand the user has the possibility to define own modules, e.g. a cardinality constraint.

SWORD already took part in SMT competitions 2008 and 2009 in the division of quantifier-free formulas over fixed-size bitvectors (QF_BV). More information about QF_BV and other divisions of SMT solving can be found at SMT-LIB.

Download  [Changes]

Please contact Rolf Drechsler in case of questions and/or problems.

  • [JSW+:2009] J. Jung, A. Sülflow, R. Wille, and R. Drechsler. SWORD v1.0. System Description for the SMTCOMP 2009, 2009.
    Download Paper | Download Slides
  • [WSD:2008] R. Wille, A. Sülflow, and R. Drechsler. SWORD v0.2 - Module-based SAT Solving. System Description for the SMTCOMP 2008, 2008.
    Download Paper | Download Slides
  • [WFG+:2007] R. Wille, G. Fey, D. Große, S. Eggersglüß, and R. Drechsler. SWORD: A SAT like Prover Using Word Level Information. VLSI-SoC, 88-93, 2007.
    Download Paper | Download Slides

©2023 | Group of Computer Architecture | Contact | Legal & Data Privacy