Solving hybrid decision-control problems through conflict-directed branch & bound

Abstract

There exists a large class of problems that incorporate both logical decision and algebraic constraints. For example, in cooperative path planning (CPP) problem, obstacle avoidance can be achieved by selecting a direction in which to avoid every obstacle, which in turn imposes an inequality constraint. Traditionally, these hybrid decision-control problems (HDCPs) are encoded in a binary integer program (BIP). These BIPs are solved using Branch and Bound (B&B) techniques. Two problems arise with this approach. First, binary arithmetic is not a natural representation for expressing complex logical choices. Propositional and higher order logics offer a more natural encoding, and computational methods exploit this encoding. Second, current BIP solution methods are to slow to solve large HDCPs online. To address these problems, this thesis introduces an approach that unifies representations and solution methods for logic and mathematical programming. To address representational adequacy, this thesis introduces the Clausal Linear Program (CLP) formulation, which encodes logical choice using propositional clauses and continuous control decisions using linear inequalities. CLPs offer a more compact and natural encoding than BIPs for many problems of logical choice. To address computational efficiency, this thesis introduces a branch and bound method for solving CLPs, analogous to BIP-B&B. This method is then unified with conflict-directed search and unit propagation. The resulting method, CDCL-B&B, searches in a best first order, while using conflicts to steer the search away from inconsistencies. Randomized experiments on CPP problems were performed using CDCL-B&B and a BIP-B&B algorithm. Results showed that CDCL-B&B improved time efficiency by