Tags:comparator network, constraints solver, odd-even network, Pseudo-Boolean, SAT and selection 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.
Competitive Sorter-based Encoding of PB-Constraints into SAT