From Idempotent Generalized Boolean Assignments to Multi-bit Search

Abstract. 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.

• Type: Conference
• Year: 2007
• Where: SAT
• Authors: Marijn Heule, Hans van Maaren
• Keywords: Assignment Reveals Feasibility, Completeness Theorem, Generalized Boolean Assignment, SAT 2007