Satisfiability with Index Dependency

Abstract
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 kSAT(m,A) denote the SAT problem restricted on instances of kCNF 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 A. For example, if A contains i_{3}=i_{1}+2i_{2} and i_{4}=i_{2}−i_{1}+1, then a clause of the input to 4SAT(2,A) has the form y_{i1} ∨ y_{i2} ∨ y_{i1}+2i_{2} ∨ y_{i2i1}+1, with y_{i} being x_{i} or x_{i}. We obtain the following results: 1) If m ≥ 2, then for any set A of linear constraints, the restricted problem kSAT(m,A) is either in P or NPcomplete assuming P ≠ NP. Moreover, the corresponding #SAT problem is always #Pcomplete, and the MaxSAT problem does not allow a polynomial time approximation scheme assuming P ≠ 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 polynomialtime algorithms for the restricted SAT problems. Using these, we prove that for any A, #2SAT(1,A) and Max2SAT(1,A) are both polynomialtime solvable, which is in sharp contrast with the hardness results of general #2SAT and Max2SAT. For fixed k ≥ 3, we obtain a large class of nontrivial constraints A, under which the problems kSAT(1,A), #kSAT(1,A) and MaxkSAT(1,A) can all be solved in polynomial time or quasipolynomial time.

