Search

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., Comment: Accepted to ICTAI 2022

Boolean cardinality constraints state that at most (at least, or exactly) $k$ out of $n$ propositional literals can be true. We propose a new class of selection networks that can be used for an efficient encoding of them. Several comparator networks have been proposed recently for encoding cardinality constraints and experiments have proved their efficiency. Those were based mainly on the odd-even or pairwise comparator networks. We use similar ideas, but we extend the model of comparator networks so that the basic components are not only comparators (2-sorters) but more general $m$-sorters, for $m \geq 2$. The inputs are organized into $m$ columns, in which elements are recursively selected and, after that, columns are merged using an idea of multi-way merging. We present two algorithms parametrized by $m \geq 2$. We call those networks $m$-Wise Selection Network and $m$-Odd-Even Selection Network. We give detailed construction of the mergers when $m=4$. The construction can be directly applied to any values of $k$ and $n$. The proposed encoding of sorters is standard, therefore the arc-consistency is preserved. We prove correctness of the constructions and present the theoretical and experimental evaluation, which show that the new encodings are competitive to the other state-of-art encodings.

Selection comparator networks have been studied for many years. Recently, they have been successfully applied to encode cardinality constraints for SAT-solvers. To decrease the size of generated formula there is a need for constructions of selection networks that can be efficiently generated and produce networks of small sizes for the practical range of their two parameters: n - the number of inputs (boolean variables) and k - the number of selected items (a cardinality bound). In this paper we give and analyze a new construction of smaller selection networks that are based on the pairwise selection networks introduced by Codish and Zanon-Ivry. We prove also that standard encodings of cardinality constraints with selection networks preserve arc-consistency., Comment: Extended version of the paper sent to CP2015