In the paper, SWORD is described – a decision procedure for bit-vector logic that uses SAT techniques and exploits word level information. The main idea of SWORD is based on the following observation: While current SAT solvers perform very well on instances with a large number of logic operations, their performance on arithmetic operations degrades with increasing data-path width. In contrast, pure word-level approaches are able to handle arithmetic operations very fast, but suffer from irregularities in the word-level structure (e.g. bit slicing). SWORD tries to combine the best of both worlds: On the one hand, it includes fast propagation, sophisticated data structures, as well as advanced techniques like non-chronological backtracking and learning from modern SAT solvers. On the other hand word-level information is exploited in the decision heuristic and during propagation.
@InProceedings{wille_et_al:DagSemProc.09461.5, author = {Wille, Robert and Jung, Jean Christoph and S\"{u}lflow, Andre and Drechsler, Rolf}, title = {{SWORD – Module-based SAT Solving}}, booktitle = {Algorithms and Applications for Next Generation SAT Solvers}, pages = {1--2}, series = {Dagstuhl Seminar Proceedings (DagSemProc)}, ISSN = {1862-4405}, year = {2010}, volume = {9461}, editor = {Bernd Becker and Valeria Bertacoo and Rolf Drechsler and Masahiro Fujita}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09461.5}, URN = {urn:nbn:de:0030-drops-25069}, doi = {10.4230/DagSemProc.09461.5}, annote = {Keywords: SAT Solver, Word Level, SAT Modulo Theories} }
Feedback for Dagstuhl Publishing