Computing diverse pair of solutions for tractable SAT
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.
Cite
@article{arxiv.2412.04016,
title = {Computing diverse pair of solutions for tractable SAT},
author = {Tatsuya Gima and Yuni Iwamasa and Yasuaki Kobayashi and Kazuhiro Kurita and Yota Otachi and Rin Saito},
journal= {arXiv preprint arXiv:2412.04016},
year = {2024}
}
Comments
14 pages, 1 figure