CNF Satisfiability in a Subspace and Related Problems
share
We introduce the problem of finding a satisfying assignment to a CNF formula that must further belong to a prescribed input subspace. Equivalent formulations of the problem include finding a point outside a union of subspaces (the Union-of-Subspace Avoidance (USA) problem), and finding a common zero of a system of polynomials over _2 each of which is a product of affine forms. We focus on the case of k-CNF formulas (the k-SUB-SAT problem). Clearly, it is no easier than k-SAT, and might be harder. Indeed, via simple reductions we show NP-hardness for k=2 and W[1]-hardness parameterized by the co-dimension of the subspace. We also prove that the optimization version Max-2-SUB-SAT is NP-hard to approximate better than the trivial 3/4 ratio even on satisfiable instances. On the algorithmic front, we investigate fast exponential algorithms which give non-trivial savings over brute-force algorithms. We give a simple branching algorithm with runtime 1.5^r for 2-SUB-SAT, where r is the subspace dimension and an O^*(1.4312)^n time algorithm where n is the number of variables. For k more than 2, while known algorithms for solving a system of degree k polynomial equations already imply a solution with runtime 2^r(1-1/2k), we explore a more combinatorial approach. For instance, based on the notion of critical variables, we give an algorithm with running time n≤ t 2^n-n/k, where n is the number of variables and t is the co-dimension of the subspace. This improves upon the running time of the polynomial equations approach for small co-dimension. Our algorithm also achieves polynomial space in contrast to the algebraic approach that uses exponential space.
READ FULL TEXT