Skip to main content Skip to main navigation

Publikation

PolySAT: A Fast Cache-SAT Implementation for Solving Boolean Problems with Parameterized Complexity

Luca Müller; Marten Gollücke; Rolf Drechsler
In: IEEE Embedded Systems Letters (ESL), Pages 1-1, IEEE, 2026.

Zusammenfassung

We introduce PolySAT, a fast Cache-SAT implementation that ensures parameterized time complexity bounds for solving Boolean problems. We provide an algorithmic view of PolySAT, pointing out optimizations to existing Cache-SAT implementations. We prove that the time complexity of PolySAT is parameterized by the cutwidth of the SAT instance φ, resulting in a polynomial runtime for instances with at most logarithmic cutwidth in the number of variables of φ. These theoretical bounds are experimentally confirmed in a case study on the formal verification of arithmetic circuits, producing speed-ups of up to 8x compared to the state-of-the-art solver CaDiCaL.