On the Parameterized Complexity of Diverse SAT

TL;DR

This work initiates a parameterized complexity study of SAT under the lens of solution diversity, focusing on two-solution variants where the two satisfying assignments must differ on a specified number of variables. The authors comprehensively analyze affine, $2$-CNF, and hitting formula classes, showing NP-hardness in general and identifying precise boundaries: polynomial-time solvability for $2$-affine and for hitting formulas, with nuanced parameterized results such as MAX DIFFER AFFINE-SAT being FPT in $d$ (and possessing a polynomial kernel) while EXACT DIFFER AFFINE-SAT is W[1]-hard in $d$ and both variants are W[1]-hard in the dual parameter $n-d$. In the $2$-CNF setting, the problems are poly-time on $(2,2)$-CNF but W[1]-hard in $d$ (even for monotone inputs). The paper leverages reductions from Independent Set and Multicolored Clique, Gaussian elimination, bipartiteness tests, and Subset Sum to establish these results, and discusses practical extensions and open questions such as outputting a diverse solution pair and extending to more than two solutions.

Abstract

We study the Boolean Satisfiability problem (SAT) in the framework of diversity, where one asks for multiple solutions that are mutually far apart (i.e., sufficiently dissimilar from each other) for a suitable notion of distance/dissimilarity between solutions. Interpreting assignments as bit vectors, we take their Hamming distance to quantify dissimilarity, and we focus on problem of finding two solutions. Specifically, we define the problem MAX DIFFER SAT (resp. EXACT DIFFER SAT) as follows: Given a Boolean formula $φ$ on $n$ variables, decide whether $φ$ has two satisfying assignments that differ on at least (resp. exactly) $d$ variables. We study classical and parameterized (in parameters $d$ and $n-d$) complexities of MAX DIFFER SAT and EXACT DIFFER SAT, when restricted to some formula-classes on which SAT is known to be polynomial-time solvable. In particular, we consider affine formulas, $2$-CNF formulas and hitting formulas. For affine formulas, we show the following: Both problems are polynomial-time solvable when each equation has at most two variables. EXACT DIFFER SAT is NP-hard, even when each equation has at most three variables and each variable appears in at most four equations. Also, MAX DIFFER SAT is NP-hard, even when each equation has at most four variables. Both problems are W[1]-hard in the parameter $n-d$. In contrast, when parameterized by $d$, EXACT DIFFER SAT is W[1]-hard, but MAX DIFFER SAT admits a single-exponential FPT algorithm and a polynomial-kernel. For 2-CNF formulas, we show the following: Both problems are polynomial-time solvable when each variable appears in at most two clauses. Also, both problems are W[1]-hard in the parameter $d$ (and therefore, it turns out, also NP-hard), even on monotone inputs (i.e., formulas with no negative literals). Finally, for hitting formulas, we show that both problems are polynomial-time solvable.

Theorems & Definitions (11)

• Theorem 1
• Theorem 2
• Theorem 3
• Theorem 4
• Theorem 5
• Theorem 6
• Theorem 7
• Theorem 8
• Theorem 9
• Theorem 10