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 $\phi$ on $n$ variables, decide whether $\phi$ 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.

翻译：我们在多样性框架下研究布尔可满足性问题（SAT），该框架要求为给定的解之间距离/相异性的适当度量，寻找多个相互远离（即彼此充分不相似）的解。将赋值解释为比特向量，我们采用其汉明距离来量化相异性，并专注于寻找两个解的问题。具体而言，我们定义MAX DIFFER SAT（以及EXACT DIFFER SAT）问题如下：给定一个包含n个变量的布尔公式φ，判定φ是否存在两个可满足赋值，使得它们在至少（或恰好）d个变量上取值不同。我们研究了当限制在SAT已知为多项式时间可解的某些公式类上时，MAX DIFFER SAT和EXACT DIFFER SAT的经典复杂性及参数化（以参数d和n-d）复杂性。特别地，我们考虑了仿射公式、2-CNF公式和命中公式。对于仿射公式，我们展示了以下结果：当每个方程至多包含两个变量时，两个问题均为多项式时间可解。EXACT DIFFER SAT是NP-难的，即使每个方程至多包含三个变量且每个变量至多出现在四个方程中。同时，MAX DIFFER SAT也是NP-难的，即使每个方程至多包含四个变量。在参数n-d下，两个问题均为W[1]-难的。相反，当以d为参数时，EXACT DIFFER SAT是W[1]-难的，但MAX DIFFER SAT允许一个单指数时间的FPT算法和一个多项式核。对于2-CNF公式，我们展示了以下结果：当每个变量至多出现在两个子句中时，两个问题均为多项式时间可解。此外，即使在单调输入（即无非文字公式）上，两个问题在参数d下也是W[1]-难的（因此，结果也表明它们是NP-难的）。最后，对于命中公式，我们证明两个问题均为多项式时间可解。