Computing small Rainbow Cycle Numbers with SAT modulo Symmetries

Envy-freeness up to any good (EFX) is a key concept in Computational Social Choice for the fair division of indivisible goods, where no agent envies another's allocation after removing any single item. A deeper understanding of EFX allocations is facilitated by exploring the rainbow cycle number ($R_f(d)$), the largest number of independent sets in a certain class of directed graphs. Upper bounds on $R_f(d)$ provide guarantees the feasibility of EFX allocations (Chaudhury et al., EC 2021).
In this work, we precisely compute the numbers $R_f(d)$ for small values of d, employing the SAT modulo Symmetries (SMT) framework. SMT is specifically tailored for the constraint-based isomorph-free synthesis of combinatorial structures. We provide an efficient encoding for the rainbow cycle number, comparing eager and lazy approaches. To cope with the huge search space, we extend the encoding with invariant pruning, a new method that significantly speeds up computation.
[Joint work with Markus Kirchweger]