Competitive Sorter-based Encoding of PB-Constraints into SAT

Authors: Michał Karpiński and Marek Piotrów

Paper Information

Title:Competitive Sorter-based Encoding of PB-Constraints into SAT
Authors:Michał Karpiński and Marek Piotrów
Proceedings:POS FLoC USB Stick
Editors: Daniel Le Berre and Matti Järvisalo
Keywords:Pseudo-Boolean, constraints solver, SAT, comparator network, selection network, odd-even network

ABSTRACT. A Pseudo-Boolean (PB) constraint is a linear inequality constraint over Boolean variables. A popular idea to solve PB-constraints is to transform them to CNFs (via BDDs, adders and sorting networks) and process them using -- increasingly improving -- state-of-the-art SAT-solvers. Recent research have favored the approach that use Binary Decision Diagrams (BDDs), which is evidenced by several new constructions and optimizations. We show that encodings based on comparator networks can still be very competitive. We present a system description of a PB-solver based on MiniSat+ which we extended by adding a new construction of a selection network called 4-Way Merge Selection Network, with a few optimizations based on other solvers. Experiments show that on many instances of popular benchmarks our technique outperforms other state-of-the-art PB-solvers.

Talk:Jul 07 11:30 (Session 26M: Pseudo-Boolean and Proofs)