Applying decision diagrams on Pseudo Boolean optimization problems

 

Description

Pseudo Boolean optimization is to find an assignment to minimize/maximize a target Boolean function while satisfying all the given Boolean constraints at the same time. The target function, as well as the constraints, is usually a linear equation or inequality. Therefore the problem is also known as the 0-1 ILP problem.

Algorithms to solve the PB optimization include CNF-SAT based (e.g. miniSat+), ILP-based, and hybrid approaches. Conceptually, it requires the PB solvers to exam all the potential solutions on the constraints and figure out the one that optimizes the target. This is not a natural application for SAT engine as it solves one solution at a time. The general ILP solver may be powerful, but it may be overkill for the special 0-1 ILP problem.

Decision diagrams (e.g. BDD, FDD, BMD, etc), on the other hand, are data structures to represent Boolean functions. When a Boolean function is successfully represented in DDs, all the satisfiable assignments can be easily obtained by enumerating the ¡§traces¡¨ to the terminal ¡§one¡¨ node. Therefore, DDs seem to be a good alternative for the PB optimization problem.

However, there is not much previous work on applying DDs for PB optimization problems [1]. This is probably because DDs are notorious for the memory explosion issue. In this project, you should survey different DDs and get acquainted with the PB optimization problem. Determine the type of DDs to adopt for PB optimization problem and compare its performance with the existing PB solvers.

 

Problem inputs

Ø          PB optimization problems. You can download the testcases form the PB evaluation website: http://www.cril.univ-artois.fr/PB07/

 

What you should do

1.        Implement PB solvers on some DD package(s).

2.        Compare your work with the state-of-the-art PB solvers.

 

Reference

1.          Yung-Te Lai, Massoud Pedram, Sarma B. K. Vrudhula: FGILP: an integer linear program solver based on function graphs. ICCAD 1993: 685-689