Trustworthy and Distributed Automated Reasoning

Abstrat

This presentation will give an introduction to the use of decision diagrams for combinatorial optimization.  It will focus on developing a novel generic branch-and-bound framework based on decision diagrams.  Working from a state-based formulation (e.g., a dynamic program), relaxed decision diagrams provide dual bounds, restricted decision diagrams provide primal bounds, and an exact search is defined based on the nodes of the diagrams.  We demonstrate that this approach outperforms or is competitive with the state of the art on various problem domains.  We will also discuss how an extension of this method called 'column elimination' can be integrated with a linear programming solver to obtain strong dual bounds for integer programming problems.