Computing Small Rainbow Cycle Numbers with SAT Modulo Symmetries

Abstract

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 (Rf (d)), the largest number of independent sets in a certain class of directed graphs. Upper bounds on Rf (d) provide guarantees to the feasibility of EFX allocations (Chaudhury et al., EC 2021). In this work, we precisely compute the numbers Rf (d) for small values of d, employing the SAT modulo Symmetries framework (Kirchweger and Szeider, CP 2021). SAT modulo Symmetries is tailored specifically for the constraint-based isomorph-free generation 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.