Home

 

The classic NP-complete problem of SAT [GaJo1979] is defined as follows: Given a propositional logic formula in conjunctive normal form where each clause has exactly three Boolean variables, is there an assignment of true/false values to the variables in the formula that makes the formula evaluate to true? We propose to develop an open-source multithreaded parallel SAT solver, Msat, for a dual-core personal computer. A parallel SAT solver takes advantage of multiple processors simultaneously.  This is done by using separate threads that solve different parts of the problem at the same time. Solver features will include the Davis-Logemann-Loveland (DLL) algorithm [DaEA1962, BaSc1997], unit propagation [ZhSt2000] and clause learning[MoEA2001]. The solver source will be made publicly available. Future work may include extensions for computers with more processors.