Construction of an ROBDD for a PB-constraint in band form and related techniques for PB-solvers

Abstract

Pseudo-Boolean (PB) problems are Integer Linear Problem restricted to 0-1 variables. This paper discusses on acceleration techniques of PB-solvers that employ SAT-solving of combined CNFs each of which is produced from each PB-constraint via a binary decision diagram (BDD). Specifically, we show (i) an efficient construction of a reduced ordered BDD (ROBDD) from a constraint in band form l ≤ Linear term ≤ h, (ii) a CNF coding that produces two clauses for some nodes in an ROBDD obtained by (i), and (iii) an incremental SAT-solving of the binary/ alternative search for minimizing values of a given goal function. We implemented the proposed constructions and report on experimental results.