Abstract
There are deep connections between logic, optimization, and constraint programming (CP) that underlie some of the most effective solution methods. Conflict clause generation in SAT algorithms, as well as SAT modulo theories, are forms of Benders decomposition, a classical optimization method that can itself be generalized by viewing it as based on logical inference. The resolution method for logical inference is intimately related to the core concept of cutting planes in integer programming (IP), as well as to Fourier-Motzkin elimination, which lies at the root of linear programming (LP) and ultimately network flow models that play an essential role in CP’s filtering techniques. In first order logic, Herbrand’s theorem is based on a compactness property that is perfectly mirrored in IP, while CP is based on a generalization of unification. Boole’s probability logic poses an LP problem that can be solved by column generation, while default and nonmonotonic logics have natural IP models. Binary decision diagrams, used for logic circuit design, provide the basis for recent developments in both CP and combinatorial optimization. The concept of consistency in CP inspires a reinterpretation of cutting planes in IP. The talk is intended for a diverse audience with multiple backgrounds.