Constructing Cover-Free Families with SAT Solvers

Cover-Free Families (CFF) are combinatorial structures that have many applications, including combinatorial group testing, cryptography, and communication networks. This paper presents a SAT-based system for constructing d-CFF(t,n) instances and related constrained variants. We model the incidence matrix of a CFF as a Boolean formula and develop multiple CNF encodings: a baseline set-inclusion encoding, an equivalent disjunct-matrix encoding, a row-weight-constrained model, and a cyclic consecutive-constrained variant. These types of encodings allow modern SAT solvers to search through possible incidence matrices without imposing algebraic constraints on the parameters. We report computational tests showing that the cyclic formulation substantially improves scalability, while row-weight constraints greatly increase complexity. Overall, our results show that SAT-solving methods provide a practical and flexible approach to producing small CFFs and determining structural variants of CFFs in real-world applications.