Computing Small Rainbow Cycle Numbers with SAT Modulo Symmetries

Explore the computation of small Rainbow Cycle Numbers using SAT modulo Symmetries in this 40-minute lecture by Stefan Szeider from TU Wien. Delve into the concept of envy-freeness up to any good (EFX) in Computational Social Choice for fair division of indivisible goods. Examine how the rainbow cycle number ($R_f(d)$) relates to EFX allocations and their feasibility. Learn about the SAT modulo Symmetries (SMT) framework and its application in constraint-based isomorph-free synthesis of combinatorial structures. Discover efficient encoding techniques for the rainbow cycle number, comparing eager and lazy approaches. Understand the implementation of invariant pruning, a novel method to accelerate computation in large search spaces. Gain insights from this joint work with Markus Kirchweger, presented as part of the Games and Equilibria in System Design and Analysis series at the Simons Institute.