Incremental Encoding of Pseudo-Boolean Goal Functions Based on Comparator Networks

Incremental techniques have been widely used in solving problems reducible to SAT and MaxSAT instances. When an algorithm requires making subsequent runs of a SAT-solver on a slightly changing input formula, it is usually beneficial to change the strategy, so that the algorithm only operates on a single instance of a SAT-solver. One way to do this is via a mechanism called assumptions, which allows to accumulate and reuse knowledge from one iteration to the next and, in consequence, the provided input formula need not to be rebuilt during computation. In this paper we propose an encoding of a Pseudo-Boolean goal function that is based on sorting networks and can be provided to a SAT-solver only once. Then, during an optimization process, different bounds on the value of the function can be given to the solver by appropriate sets of assumptions. The experimental results show that the proposed technique is sound, that is, it increases the number of solved instances and reduces the average time and memory used by the solver on solved instances.