Satisfiability to Coverage in Presence of Fairness, Matroid, and Global Constraints

In MaxSAT with Cardinality Constraint problem (CC-MaxSAT), we are given a CNF-formula Φ, and k ≥ 0, and the goal is to find an assignment β with at most k variables set to true (also called a weight k-assignment) such that the number of clauses satisfied by β is maximized. MaxCov can be seen as a special case of CC-MaxSAT, where the formula Φ is monotone, i.e., does not contain any negative literals. CC-MaxSAT and MaxCov are extremely well-studied problems in the approximation algorithms as well as parameterized complexity literature. Our first contribution is that the two problems are equivalent to each other in the context of FPT-Approximation parameterized by k (approximation is in terms of number of clauses satisfied/elements covered). We give a randomized reduction from CC-MaxSAT to MaxCov in time O(1/ε)ᵏ · (m+n)O(1) that preserves the approximation guarantee up to a factor of 1-ε. Furthermore, this reduction also works in the presence of fairness and matroid constraints. Armed with this reduction, we focus on designing FPT-Approximation schemes (FPT-ASes) for MaxCov and its generalizations. Our algorithms are based on a novel combination of a variety of ideas, including a carefully designed probability distribution that exploits sparse coverage functions. These algorithms substantially generalize the results in Jain et al. [SODA 2023] for CC-MaxSAT and MaxCov for Kd,d-free set systems (i.e., no d sets share d elements), as well as a recent FPT-AS for Matroid-Constrained MaxCov by Sellier [ESA 2023] for frequency-d set systems.