Parallelization of stochastic algorithm for boolean satisfiability on GPGPU architecture
Conference proceedings article
ผู้เขียน/บรรณาธิการ
กลุ่มสาขาการวิจัยเชิงกลยุทธ์
ไม่พบข้อมูลที่เกี่ยวข้อง
รายละเอียดสำหรับงานพิมพ์
รายชื่อผู้แต่ง: Nimnon S., Phadoongsidhi M., Utamaphethai N.
ผู้เผยแพร่: Hindawi
ปีที่เผยแพร่ (ค.ศ.): 2012
ISBN: 9781467320245
นอก: 0146-9428
eISSN: 1745-4557
ภาษา: English-Great Britain (EN-GB)
บทคัดย่อ
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.
คำสำคัญ
Algorithm, Boolean satisfiability, CUDA, GPGPU
ติดต่อสอบถามเพิ่มเติมได้ที่