SWORD - A Module-based SMT Solver
by Rolf Drechsler
, Finn Haedicke
, Jean Christoph Jung
, Andre Sülflow
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.
Please contact us in case of questions and/or problems at firstname.lastname@example.org
- [JSW+:2009] J. Jung, A. Sülflow, R. Wille, and R. Drechsler. SWORD v1.0. System Description for the SMTCOMP 2009, 2009.
- [WSD:2008] R. Wille, A. Sülflow, and R. Drechsler. SWORD v0.2 - Module-based SAT Solving. System Description for the SMTCOMP 2008, 2008.
- [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.