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: | 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. |
Pages: | 14 |
Talk: | Jul 07 11:30 (Session 26M: Pseudo-Boolean and Proofs) |
Paper: |