Open Collections

Description

Over the past few decades, astonishing progress has been made in SAT solving. A key ingredient in this is conflict-driven search and learning, which has led to exponential improvements. SAT decision engines are also used as backends for increasingly powerful optimization tools. And finally, SAT solvers are extremely reliable because the correctness of the results they compute can be certified using a machine-verifiable certificate. Can we generalize all of this to the much more expressive paradigm of 0-1 integer linear programming? In this talk, I will discuss some recent and ongoing research in this area by the Mathematical Insights into Algorithms for Optimization (MIAO) group and its collaborators. I will first explain how pseudo-Boolean conflict analysis generalizes conflict analysis for SAT solving and why it is necessary to apply cuts (e.g., Chvátal-Gomory cuts or mixed-integer rounding cuts) rather than just applying generalized resolution steps. Next, I will explain some optimization techniques, including core-guided search and implicit hitting set solving. For all of our work, we also ensure that our solver is certifying by outputting proofs in the VeriPB format.