Back to Search Start Over

Reusing Comparator Networks in Pseudo-Boolean Encodings

Authors :
Karpiński, Michał
Piotrów, Marek
Publication Year :
2022
Publisher :
arXiv, 2022.

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

Details

Database :
OpenAIRE
Accession number :
edsair.doi.dedup.....9323ee278a67d6e7d5585cd0bc560f6e
Full Text :
https://doi.org/10.48550/arxiv.2205.04129