×

zbMATH — the first resource for mathematics

From idempotent generalized Boolean assignments to multi-bit search. (English) Zbl 1214.68355
Marques-Silva, João (ed.) et al., Theory and applications of satisfiability testing – SAT 2007. 10th international conference, Lisbon, Portugal, May 28–31, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-72787-3/pbk). Lecture Notes in Computer Science 4501, 134-147 (2007).
Summary: This paper shows that idempotents in finite rings of integers can act as Generalized Boolean Assignments (GBA’s) by providing a completeness theorem. We introduce the notion of a generic Generalized Boolean Assignment. The mere propagation of such an assignment reveals feasibility (existence of a solution) of a formula in propositional logic. Then, we demystify this general concept by formulating the process on the bit-level: It turns out that propagation of a GBA only simulates bitwise (non-communicating) parallel computing. We capitalize on this by modifying the state-of-the-art local search Sat solver UnitWalk accordingly. This modification involves a more complicated parallelism.
For the entire collection see [Zbl 1120.68007].
MSC:
68T20 Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.)
Software:
UnitWalk
PDF BibTeX XML Cite
Full Text: DOI