Title :
Automatic parallel SAT solving using MTSS
Author :
Vander-Swalmen, Pascal ; Krajecki, Michal ; Dequen, Gilles
Author_Institution :
CreSTIC & MIS, Univ. of Reims Champagne, Reims, France
Abstract :
Satisfiability Problem is a great and competitive practical approach to solve a wide range of industrial and academic problems. The size and difficulty of the SAT instances have grown significantly over years thanks to solvers always more competitive. Among the recent solvers, the main part of them are sequential. Even if all of them include a very interesting innovation to improve performances, they can not take advantage of new multicore processors widely available today. To overcome this situation, MTSS (Multi-Threaded Sat Solver) allows to parallelize an existing sequential SAT solver by introducing the principle of guiding tree in shared memory.
Keywords :
computability; multi-threading; optimisation; tree searching; MTSS; Multi-Threaded Sat Solver; Satisfiability Problem; automatic parallel SAT; combinatorial optimization; principle of guiding tree; sequential SAT solver; Artificial intelligence; Cryptography; Design optimization; Memory management; Message passing; Multicore processing; NP-complete problem; Technological innovation; Very large scale integration; Yarn; combinatorial optimization; parallel; satisfiability;
Conference_Titel :
High Performance Computing & Simulation, 2009. HPCS '09. International Conference on
Conference_Location :
Leipzig
Print_ISBN :
978-1-4244-4906-4
Electronic_ISBN :
978-1-4244-4907-1
DOI :
10.1109/HPCSIM.2009.5191794
