Competitive Sorter-based Encoding of PB-Constraints into SAT

by Michał Karpiński and Marek Piotrów

Here we present detailed results of the experiments section of our paper called Competitive Sorter-based Encoding of PB-Constraints into SAT, currently submitted for publication. In the paper we present a novel encoding based on selection networks: 4-Way Merge Selection Network, which we implemented in the KP-MiniSat+ solver, based on the newest version of the MiniSat+. Underlying SAT-solver used in our system is COMiniSatPS.

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 uses 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 selection network called 4-Odd-Even 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.

Solvers used in the evaluation:

• KP-MiniSat+
• PBLib
• NaPS
• MiniSat+ (original)
• MiniSat+ with COMiniSatPS as an underlying solver

All experiments were carried out on the machines with Intel(R) Core(TM) i7-2600 CPU @ 3.40GHz. Timeout limit is set to 1800 seconds and memory limit is 15 GB. Description of benchmarks and the results now follows.

Pseudo-Boolean Competition 2016 benchmarks:

The set of benchmarks we use is a set of instances from the Pseudo-Boolean Competition 2016. We use instances with linear, Pseudo-Boolean constraints that encode either decision or optimization problems. To this end, three categories from the competition have been selected:

• DEC-SMALLINT-LIN - 1783 instances of decision problems with small coefficients in the constraints (no constraint with sum of coefficients greater than 2^20). No objective function to optimize. The solver must simply find a solution.
• OPT-BIGINT-LIN - 1109 instances of optimization problems with big coefficients in the constraints (at least one constraint with a sum of coefficients greater than 2^20). An objective function is present. The solver must find a solution with the best possible value of the objective function.
• OPT-SMALLINT-LIN - 1600 instances of optimization problems. Similar OPT-BIGINT-LIN but with small coefficients (as in DEC-SMALLINT-LIN) in the constraints.

Detalied results:

• DEC-SMALLINT-LIN: KP-MS+, NaPS, PBLib, MS+, MS+COM.
• OPT-BIGINT-LIN: KP-MS+, NaPS, MS+, MS+COM.
• OPT-SMALLINT-LIN: KP-MS+, NaPS, PBLib, MS+, MS+COM.

Cactus plots:

DEC-SMALLINT-LIN:

OPT-BIGINT-LIN:

OPT-SMALLINT-LIN: