Solution Space Partitioning for Extremal Set Theory

Abstract

We present a method for partitioning the solution space of statements in extremal set theory. Compared with domain-agnostic partitioning methods like look-ahead, we perform case analysis on the strategies by which a candidate solution can be constructed. We demonstrate that our approach can decompose problems in extremal set theory more effectively than look-ahead. Combining this new partitioning strategy with an exact proof-producing MILP solver, we are able to verify larger finite cases of Chvátal's Conjecture---a long-standing open question in extremal combinatorics---compared to previous work.

14 pages; corrected the interchanged "max solve time (s)" values for "symbreak (1s)" and "symbreak (3s)" in Table II (p. 9)