Computing diverse pair of solutions for tractable SAT

TL;DR

This paper explores algorithms for efficiently finding diverse pairs of solutions in tractable SAT problems, focusing on parameterized complexity and providing both tractable and intractable results.

Contribution

It introduces new fixed-parameter tractable algorithms for finding diverse solutions in certain classes of SAT, especially for 2CNF formulas.

Findings

FPT algorithm for almost disjoint pairs in 2CNF formulas

Identification of parameterized intractability results

Enhanced understanding of solution diversity in tractable SAT instances

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.