Parsat project


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, GPUs, etc), are a promising 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.