cover.set_cover_sat

cover.set_cover_sat(subsets, weights=None, full_output=False, **kwargs)

Computes an approximate solution to the weighted set cover problem via weighted MaxSAT.

This function converts the problem of finding a minimum weight set cover to a weighted MaxSAT instance:

\[ \max_{\mathcal{C} \subseteq \mathcal{S}} \sum_{S_i \in \mathcal{C}} -w_i x_i \quad \text{subject to} \quad \bigvee_{x_i \in N_j} x_i = 1 \quad \forall j \in U \]

where \(x_i \in \{0,1\}\) is an indicator of cover membership and \(N_j\) represents the subsets of \(\mathcal{S}\) that the element \(j \in U\) intersects. The MaxSAT approximation is known to achieve at least an (8/7)-approximation of the optimal solution.

The default solver is the Relaxed Cardinality Constraint solver (RC2), with Boolean lexicographic optimization (BLO) stratification options turned on. RC2 requires python-sat to be installed.

Parameters

Name	Type	Description	Default
subsets	sparray	(n x J) sparse matrix of J subsets whose union forms a cover over n points.	required
weights	Optional[ArrayLike]	(J)-length array of subset weights.	None
full_output	bool	whether to return the SAT-solver instance. Defaults to False.	False
**kwargs	dict	additional keyword arguments to pass to the solver.	{}

Returns

Type	Description
tuple	pair (s, c) where s is an array indicating cover membership and c its cost.