Parallelization of stochastic algorithm for boolean satisfiability on GPGPU architecture

Conference proceedings article

Authors/Editors

Strategic Research Themes

No matching items found.

Publication Details

Author list: Nimnon S., Phadoongsidhi M., Utamaphethai N.

Publisher: Hindawi

Publication year: 2012

ISBN: 9781467320245

ISSN: 0146-9428

eISSN: 1745-4557

URL: https://www.scopus.com/inward/record.uri?eid=2-s2.0-84866772601&doi=10.1109%2fECTICon.2012.6254246&partnerID=40&md5=322da4ca27ca9601b8e417f76b92f671

Languages: English-Great Britain (EN-GB)

View on publisher site

Abstract

Boolean satisfiability problem (SAT) is an NP-complete decision problem for determining whether there exists a variable assignment making a Boolean expression satisfiable (TRUE). SAT has been the cornerstone for various Computer Engineering applications. Numerous algorithms for solving SAT exist with varying degrees of completeness and complexity. A class of SAT algorithms based on stochastic local search (SLS) is generally easier to implement than backtracking search procedures. This paper discusses cwSAT, a parallel implementation of an SLS procedure, WalkSAT, on a GPGPU architecture. The performance of cwSAT is compared with that of WalkSAT using 200 benchmarks in Random class of SAT11 Competition. Experimental results showed that cwSAT can find satisfiable assignments for over 99% of the benchmarks while the average improvement of cwSAT is approximately 33% to 98% over WalkSAT. ฉ 2012 IEEE.

Keywords

Algorithm, Boolean satisfiability, CUDA, GPGPU