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
Rolf Drechsler in case of questions and/or problems.
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
