Presentation
PRS: An Efficient Parallel SAT Framework
DescriptionThe propositional Satisfiability (SAT) problem is fundamental to many applications in Electronic Design Automation (EDA). This paper presents PRS, an efficient and comprehensive parallel SAT framework. We introduce two key techniques to enhance solver performance. The first is a lightweight preprocessing method called Resolution Checking, which efficiently simplifies circuit-encoded CNFs. The second is a new hybrid diversification strategy that combines a Regular Shifting method for the initial branching order with a parallel local search to generate diverse initial variable phases. PRS also supports extensive preprocessing, dynamic clause sharing, reproducible parallel solving, and parallel proof generation. Extensive experiments on the SAT Competition 2025 (SC25) benchmark demonstrate the effectiveness and scalability of our framework: PRS outperforms the SC25 Parallel-Track winner MallobSAT by solving 12 more instances with an 11.4% better PAR2 score, while also achieving a 4.7x speedup on 64 cores.
Event Type
Research Manuscript
TimeWednesday, July 2910:42am - 10:54am PDT
LocationMtg Room 202AB