Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Computing diverse pair of solutions for tractable SAT

Tatsuya Gima, Yuni Iwamasa, Yasuaki Kobayashi, Kazuhiro Kurita, Yota Otachi, Rin Saito

TL;DR

This work analyzes the problem of generating diverse pairs (and, more generally, dissimilar pairs) of satisfying assignments for SAT across tractable formula classes from a parameterized complexity perspective. It delivers a mixed landscape of hardness and tractability results: NP-hard and W[1]-hard instances for several classes, a concrete $FPT$ algorithm for Dissimilar Pair on $2$CNF via Almost $2$SAT with Hard Constraints and Vertex Cover above maximum matching, and a linear-algebra Based tractability for XOR formulas (Diverse) contrasted with W[1]-hardness (Dissimilar). It also provides a polynomial-time algorithm for double Horn formulas to maximize the sum of pairwise Hamming distances among $k$ solutions, leveraging lattice properties of the Horn solution space. Collectively, the results delineate when diverse solution sets are computationally feasible and inform strategies for producing diverse candidates in SAT-based decision-making workflows.

Abstract

In many decision-making processes, one may prefer multiple solutions to a single solution, which allows us to choose an appropriate solution from the set of promising solutions that are found by algorithms. Given this, finding a set of \emph{diverse} solutions plays an indispensable role in enhancing human decision-making. In this paper, we investigate the problem of finding diverse solutions of Satisfiability from the perspective of parameterized complexity with a particular focus on \emph{tractable} Boolean formulas. We present several parameterized tractable and intractable results for finding a diverse pair of satisfying assignments of a Boolean formula. In particular, we design an FPT algorithm for finding an ``almost disjoint'' pair of satisfying assignments of a $2$CNF formula.

Computing diverse pair of solutions for tractable SAT

TL;DR

This work analyzes the problem of generating diverse pairs (and, more generally, dissimilar pairs) of satisfying assignments for SAT across tractable formula classes from a parameterized complexity perspective. It delivers a mixed landscape of hardness and tractability results: NP-hard and W[1]-hard instances for several classes, a concrete algorithm for Dissimilar Pair on CNF via Almost SAT with Hard Constraints and Vertex Cover above maximum matching, and a linear-algebra Based tractability for XOR formulas (Diverse) contrasted with W[1]-hardness (Dissimilar). It also provides a polynomial-time algorithm for double Horn formulas to maximize the sum of pairwise Hamming distances among solutions, leveraging lattice properties of the Horn solution space. Collectively, the results delineate when diverse solution sets are computationally feasible and inform strategies for producing diverse candidates in SAT-based decision-making workflows.

Abstract

In many decision-making processes, one may prefer multiple solutions to a single solution, which allows us to choose an appropriate solution from the set of promising solutions that are found by algorithms. Given this, finding a set of \emph{diverse} solutions plays an indispensable role in enhancing human decision-making. In this paper, we investigate the problem of finding diverse solutions of Satisfiability from the perspective of parameterized complexity with a particular focus on \emph{tractable} Boolean formulas. We present several parameterized tractable and intractable results for finding a diverse pair of satisfying assignments of a Boolean formula. In particular, we design an FPT algorithm for finding an ``almost disjoint'' pair of satisfying assignments of a CNF formula.

Paper Structure

This paper contains 9 sections, 12 theorems, 19 equations, 1 figure, 1 table.

Table of Contents

  1. Introduction
  2. Independent work.
  3. Preliminaries
  4. Boolean formulas.
  5. Parameterized complexity.
  6. Hardness for 2CNF, Horn, and dual Horn formulas
  7. Fixed-parameter tractability of Dissimilar Pair of Solutions for $2$CNF formulas
  8. Fixed-parameter tractability and W[1]-hardness for XOR formulas
  9. Polynomial-time algorithm for double Horn formulas

Key Result

Theorem 1

Given a Boolean formula $\phi$, Max Hamming Distance SAT can be solved in polynomial time if $\phi$ is $01$-valid or even-affine; APX-complete if $\phi$ is affine; PolyAPX-complete if $\phi$ is strongly $0$-valid, strongly $1$-valid, Horn, dual Horn, or $2$CNF. Otherwise, this problem is NP-hard ev

Figures (1)

  • Figure 1: The figure depicts the graph $G_I$ for $\varphi = (w \lor \neg x) \land (x \lor y) \land (y \lor \neg z)$, $S = \{(x \lor y), (y \lor \neg z)\}$, and $s = 1$. Red and blue lines represent hard and soft-clause edges, respectively.

Theorems & Definitions (18)

  • Theorem 1: CrescenziR02
  • Theorem 2
  • proof
  • Theorem 3
  • Lemma 1
  • proof
  • Corollary 1
  • proof
  • Lemma 2
  • proof
  • ...and 8 more