On Optimizing a Generic Function in SAT
Alexander Nadel · 2020
The goal of this study is to improve the scalability of today's SAT-based solutions for optimization problems and to pave the way towards extending the range of optimization problems solvable with SAT in practice.Let OptSAT be the problem of optimizing a generic Pseudo-Boolean function, given a satisfiable propositional formula F .We introduce an incremental and anytime incomplete algorithm for solving OptSAT, called Polosat.We show that integrating Polosat into a state-of-theart open-source anytime MaxSAT solver significantly improves the solver's performance.Furthermore, we demonstrate that Polosat substantially improves the solution quality of an industrial placement tool, where placement is a sub-stage of the physical design stage of chip design.