Reusing Comparator Networks in Pseudo-Boolean Encodings

TL;DR

This paper introduces a method to reuse parts of pseudo-Boolean encodings using comparator networks, reducing SAT instance size and improving solver performance.

Contribution

It presents a novel reuse technique for comparator networks in pseudo-Boolean encodings, enhancing efficiency and solving more instances.

Findings

Increased number of solved instances with the new method

Reduced size of SAT encodings

Improved efficiency of solving pseudo-Boolean problems

Abstract

A Pseudo-Boolean (PB) constraint is a linear inequality constraint over Boolean literals. One of the popular, efficient ideas used to solve PB-problems (a set of PB-constraints) is to translate them to SAT instances (encodings) via, for example, sorting networks, then to process those instances using state-of-the-art SAT-solvers. In this paper we show an improvement of such technique. By using a variation of a greedy set cover algorithm, when adding constraints to our encoding, we reuse parts of the already encoded PB-instance in order to decrease the size (the number of variables and clauses) of the resulting SAT instance. The experimental evaluation shows that the proposed method increases the number of solved instances.