Homepage Sitemap Contact

Group
Reasearch
Studies
Publications
Software
Service
Contact




Home « Service « Software
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]


Contact
Please contact us in case of questions and/or problems at sword@informatik.uni-bremen.de

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



Add to Favorites
Deutsch


Team





Sitemap Kontakt

ISMVL2014 DUHDE