Abstract
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 UnionofSubspace Avoidance (USA) problem), and finding a common zero of a system of polynomials over 𝔽₂ each of which is a product of affine forms.
We focus on the case of kCNF formulas (the kSubSat problem). Clearly, kSubSat is no easier than kSAT, and might be harder. Indeed, via simple reductions we show that 2SubSat is NPhard, and W[1]hard when parameterized by the codimension of the subspace. We also prove that the optimization version Max2SubSat is NPhard to approximate better than the trivial 3/4 ratio even on satisfiable instances.
On the algorithmic front, we investigate fast exponential algorithms which give nontrivial savings over bruteforce algorithms. We give a simple branching algorithm with running time (1.5)^r for 2SubSat, where r is the subspace dimension, as well as an O^*(1.4312)ⁿ time algorithm where n is the number of variables.
Turning to kSubSat for k ⩾ 3, while known algorithms for solving a system of degree k polynomial equations already imply a solution with running time ≈ 2^{r(11/2k)}, we explore a more combinatorial approach. Based on an analysis of critical variables (a key notion underlying the randomized kSAT algorithm of Paturi, Pudlak, and Zane), we give an algorithm with running time ≈ {n choose {⩽t}} 2^{nn/k} where n is the number of variables and t is the codimension of the subspace. This improves upon the running time of the polynomial equations approach for small codimension. Our combinatorial approach also achieves polynomial space in contrast to the algebraic approach that uses exponential space. We also give a PPZstyle algorithm for kSubSat with running time ≈ 2^{nn/2k}. This algorithm is in fact oblivious to the structure of the subspace, and extends when the subspacemembership constraint is replaced by any constraint for which partial satisfying assignments can be efficiently completed to a full satisfying assignment. Finally, for systems of O(n) polynomial equations in n variables over 𝔽₂, we give a fast exponential algorithm when each polynomial has bounded degree irreducible factors (but can otherwise have large degree) using a degree reduction trick.
BibTeX  Entry
@InProceedings{arvind_et_al:LIPIcs.IPEC.2021.5,
author = {Arvind, Vikraman and Guruswami, Venkatesan},
title = {{CNF Satisfiability in a Subspace and Related Problems}},
booktitle = {16th International Symposium on Parameterized and Exact Computation (IPEC 2021)},
pages = {5:15:15},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959772167},
ISSN = {18688969},
year = {2021},
volume = {214},
editor = {Golovach, Petr A. and Zehavi, Meirav},
publisher = {Schloss Dagstuhl  LeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/15388},
URN = {urn:nbn:de:0030drops153886},
doi = {10.4230/LIPIcs.IPEC.2021.5},
annote = {Keywords: CNF Satisfiability, Exact exponential algorithms, Hardness results}
}
Keywords: 

CNF Satisfiability, Exact exponential algorithms, Hardness results 
Collection: 

16th International Symposium on Parameterized and Exact Computation (IPEC 2021) 
Issue Date: 

2021 
Date of publication: 

22.11.2021 