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]

• SWORD 1.1, from November 1, 2009
  SWORD-1.1 (32bit Linux)
  SWORD-1.1 (64bit Linux)
  
  
• SWORD 1.0, from August 10, 2009
  SWORD-1.0 (32bit Linux)
  
  
• SWORD 0.2, from August 8, 2008
  SWORD-0.2 (32bit Linux)
  
  

• [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