-Parallel Satisfiability Algorithms and its Applications (IE02032) (Project Link)
Acronym: ParSat
Paulo Ferreira Godinho Flores
From 04-Apr-2010 to 04-Apr-2013
Prime Contractor: INESC-ID (Other)
Financed by: FCT (PTDC/EIA-EIA/103532/2008) (Other) -Portugal
Partnerships: INESC-ID (Other)
Members: Paulo Ferreira Godinho Flores, José Carlos Alves Pereira Monteiro, Luís Jorge Brás Monteiro Guerra e Silva, Luis Miguel Teixeira D Avila Pinto da Silveira, Maria Inês Camarate de Campos Lynce de Faria, Vasco Miguel Gomes Nunes Manquinho

The Boolean Satisfiability Problem (SAT) is a fundamental problem in computer science. It is not only of theoretical interest but also of practical relevance for several industries. For instance, in EDA area, SAT has been successfully used for automatic test pattern generation, combinational equivalence checking, symbolic model checking, timing analysis and FPGA routing. Our goal in this project, is to research and develop techniques to speedup the solution of SAT problems. Distributed SAT algorithms, using parallel computing environments ( such as multicores, GPU´s, etc...) are a promissing approach to reach this goal. Using these new computing platforms, we plan to explore techniques both at the algorithmic level and at the implementation level. In the former we will consider how SAT algorithms can be modified to explore the search space in parallel, and in the latter we will identify code sections that can be efficiently executed in parallel. Moreover, the different characteristics of the parallel computational platforms, MIMD versus SIMD, will for sure lead us to different approaches in the exploration of the various algorithmic levels of parallelism.