Decision Diagrams for Combinatorial Optimization and Satisfaction

• Main Author: Kell, Brian
• Format: Others
• Published: Research Showcase @ CMU 2015
• Online Access: http://repository.cmu.edu/dissertations/521; http://repository.cmu.edu/cgi/viewcontent.cgi?article=1521&context=dissertations

In this thesis we develop techniques for applying binary decision diagrams (BDDs) and multivalued decision diagrams (MDDs) to combinatorial optimization and satisfaction problems, in particular multidimensional bin packing problems and the Boolean satisfiability problem. In the multidimensional bin packing problem, each bin has a multidimensional capacity and each item has an associated multidimensional size. We develop several MDD representations for this problem and explore different MDD construction methods including a new heuristic-driven depth-first compilation scheme. We also derive MDD restrictions and relaxations, using a novel application of a clustering algorithm to identify approximate equivalence classes among MDD nodes. Our experimental results show that these techniques can significantly outperform solvers using current constraint programming and mixed-integer programming methods. The Boolean satisfiability (SAT) problem is the problem of determining whether a given propositional formula defined on a set of Boolean variables has a satisfying assignment, that is, an assignment of truth values to the variables that makes the formula true. We present a generic method for deducing valid clauses from a SAT instance using BDDs, with the aim of finding clauses that are bottlenecks for SAT solvers using conflict-directed clause learning. We formally characterize the strength of these generated clauses and show that any clause learned from SAT conflict analysis can also be generated using our method, while our method can additionally generate stronger clauses than those that are derivable using one application of conflict analysis. The method remains valid for approximate BDDs, which is important for SAT instances that are too large for an exact BDD representation. Our experimental results show that the clauses generated from BDDs can signicantly reduce the numbers of decisions and conflicts encountered by a SAT solver. In order to extend these clause generation techniques to larger SAT instances, we propose several methods to decompose a SAT instance into smaller subinstances. These methods are based on the identification of clauses that arise from the application of the widely used Tseitin transformation, the analysis of the structure of the constraint graph corresponding to the instance, and the modeling of the instance as a resistive electrical network. Preliminary experiments demonstrate that these techniques are promising areas for future research.