×

zbMATH — the first resource for mathematics

Satisfiability with index dependency. (English) Zbl 1310.68114
Cheong, Otfried (ed.) et al., Algorithms and computation. 21st international symposium, ISAAC 2010, Jeju Island, Korea, December 15–17, 2010. Proceedings, Part I. Berlin: Springer (ISBN 978-3-642-17516-9/pbk). Lecture Notes in Computer Science 6506, 49-60 (2010).
Summary: We study the Boolean Satisfiability Problem (SAT) restricted on input formulas for which there are linear arithmetic constraints imposed on the indices of variables occurring in the same clause. This can be seen as a structural counterpart of Schaefer’s dichotomy theorem which studies the SAT problem with additional constraints on the assigned values of variables in the same clause. More precisely, let \(k\)-SAT(\(m,\mathcal{A}\)) denote the SAT problem restricted on instances of \(k\)-CNF formulas, in every clause of which the indices of the last \(k - m\) variables are totally decided by the first \(m\) ones through some linear equations chosen from \(\mathcal{A}\). For example, if \(\mathcal{A}\) contains \(i _{3} = i _{1} + 2i _{2}\) and \(i _{4} = i _{2} - i _{1} + 1\), then a clause of the input to 4-SAT(\(2,\mathcal{A}\)) has the form \(y_{i_1}\lor y_{i_2} \lor y_{i_1+2i_2} \lor y_{i_2-i_1+1}\), with \(y _{i }\) being \(x _{i }\) or \(\overline{x_i}\). We obtain the following results:
1. If \(m \geq 2\), then for any set \(\mathcal{A}\) of linear constraints, the restricted problem \(k\)-SAT\((m,\mathcal{A})\) is either in P or NP-complete assuming \(\text{P} \neq \text{NP}\). Moreover, the corresponding #SAT problem is always #P-complete, and the Max-SAT problem does not allow a polynomial time approximation scheme assuming \(\text{P} \neq \text{NP}\).
2. \( m = 1\), that is, in every clause only one index can be chosen freely. In this case, we develop a general framework together with some techniques for designing polynomial-time algorithms for the restricted SAT problems. Using these, we prove that for any \(\mathcal{A}\), #2-SAT\((1,\mathcal{A})\) and Max-2-SAT\((1,\mathcal{A})\) are both polynomial-time solvable, which is in sharp contrast with the hardness results of general #2-SAT and Max-2-SAT. For fixed \(k \geq 3\), we obtain a large class of non-trivial constraints \(\mathcal{A}\), under which the problems \(k\)-SAT\((1,\mathcal{A})\), #\(k\)-SAT\((1,\mathcal{A})\) and Max-\(k\)-SAT\((1,\mathcal{A})\) can all be solved in polynomial time or quasi-polynomial time.
For the entire collection see [Zbl 1202.68002].
MSC:
68Q25 Analysis of algorithms and problem complexity
Software:
MAX-2-SAT
PDF BibTeX XML Cite
Full Text: DOI