Print Email Facebook Twitter Parallel SAT Solving using Bit-level Operations Title Parallel SAT Solving using Bit-level Operations Author Heule, M.J.H. Van Maaren, H. Faculty Electrical Engineering, Mathematics and Computer Science Department Software Technology Date 2008-09-01 Abstract We show how to exploit the 32/64 bit architecture of modern computers to accelerate some of the algorithms used in satisfiability solving by modifying assignments to variables in parallel on a single processor. Techniques such as random sampling demonstrate that while using bit vectors instead of Boolean values solutions to satisfiable formulae can be obtained faster. Here, we reveal that more complex algorithms, like unit propagation and detection of autarkies, can be parallelized efficiently, as well. We capitalize on the developed parallel algorithms by modifying the state-of-the-art local search Sat solver UnitWalk accordingly. Experiments show that the parallel version performs much faster than the original implementation. Subject local searchparallel computingBoolean Algebra To reference this document use: http://resolver.tudelft.nl/uuid:e4e65262-6c0c-4c19-ad75-80dc56380dd5 ISSN 1574-0617 Source Journal on Satisfiability, Boolean Modeling and Computation 4 (2008) Part of collection Institutional Repository Document type journal article Rights (c) 2008 M.J.H. HeuleH. van Maaren Files PDF JSAT4_6_Heule.pdf 415.75 KB Close viewer /islandora/object/uuid:e4e65262-6c0c-4c19-ad75-80dc56380dd5/datastream/OBJ/view