2026-07-23T03:49:23Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:2506 2024-03-06T11:09:03Z ddc:004 open_access

SWORD – Module-based SAT Solving Wille, Robert Jung, Jean Christoph Sülflow, Andre Drechsler, Rolf SAT Solver Word Level SAT Modulo Theories 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Robert Wille and Jean Christoph Jung and Andre Sülflow and Rolf Drechsler 2010 Is Part Of Dagstuhl Seminar Proceedings, Volume 9461, Algorithms and Applications for Next Generation SAT Solvers (2010) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DagSemProc.09461.5 urn:nbn:de:0030-drops-25069 https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09461.5 eng https://creativecommons.org/licenses/by/4.0/legalcode