Resolutions Meets Cutting Planes: Introducing Hypercube Linear Resolution

Speaker: Maarten Flippo (TU Delft) Title: Resolutions Meets Cutting Planes: Introducing Hypercube Linear Resolution Abstract: Modern combinatorial solvers can be understood as searching for proofs of unsatisfiability or optimality. The proof system implemented by a solver, therefore, fundamentally shapes solver performance. While propositional resolution is simple and complete for propositional formulas, no existing practical resolution-based system offers unrestricted complete reasoning over integer linear inequalities. We introduce hypercube linear resolution, a new proof system that is both sound and complete for integer linear reasoning. Hypercube linear resolution integrates propositional resolution with Fourier resolution through a new constraint type, the hypercube linear constraint, which captures linear relations within a discrete hypercube. In this talk we will introduce the hypercube linear constraint, as well as the resolution operators we defined. Without going too deep into the theory, we will go through some examples where hypercube resolution improves over propositional resolution. Additionally, we look at what future work is most promising to make hypercube linear resolution truly practical. Bio: Maarten Flippo is a fourth year PhD student at TU Delft in the Netherlands. His research is focused on constraint programming solvers, and in particular the proof systems they use to solve real world problems. Concretely, he is motivated in improving user confidence in the correctness of CP solvers, as well as explore different proof systems to increase solver performance. As part of the PhD, Maarten is one of the core contributors of the Pumpkin constraint programming solver.