CNF Satisfiability in a Subspace and Related Problems
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 𝔽₂ each of which is a product of affine forms.
We focus on the case of k-CNF formulas (the k-Sub-Sat problem). Clearly, k-Sub-Sat is no easier than k-SAT, and might be harder. Indeed, via simple reductions we show that 2-Sub-Sat is NP-hard, and W[1]-hard when 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 running time (1.5)^r for 2-Sub-Sat, where r is the subspace dimension, as well as an O^*(1.4312)ⁿ time algorithm where n is the number of variables.
Turning to k-Sub-Sat for k ⩾ 3, while known algorithms for solving a system of degree k polynomial equations already imply a solution with running time ≈ 2^{r(1-1/2k)}, we explore a more combinatorial approach. Based on an analysis of critical variables (a key notion underlying the randomized k-SAT algorithm of Paturi, Pudlak, and Zane), we give an algorithm with running time ≈ {n choose {⩽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 combinatorial approach also achieves polynomial space in contrast to the algebraic approach that uses exponential space. We also give a PPZ-style algorithm for k-Sub-Sat with running time ≈ 2^{n-n/2k}. This algorithm is in fact oblivious to the structure of the subspace, and extends when the subspace-membership 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.
CNF Satisfiability
Exact exponential algorithms
Hardness results
Theory of computation~Parameterized complexity and exact algorithms
5:1-5:15
Regular Paper
https://arxiv.org/abs/2108.05914
We thank anonymous reviewers for useful comments and pointers to the literature.
Vikraman
Arvind
Vikraman Arvind
The Institute of Mathematical Sciences (HBNI), Chennai, India
Venkatesan
Guruswami
Venkatesan Guruswami
Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA
Portions of this work were done during visits to the Institute of Mathematical Sciences, Chennai. Research supported in part by the National Science Foundation grant CCF-1908125 and a Simons Investigator Award.
10.4230/LIPIcs.IPEC.2021.5
Vikraman Arvind and Venkatesan Guruswami. Cnf satisfiability in a subspace and related problems, 2021. URL: http://arxiv.org/abs/2108.05914.
http://arxiv.org/abs/2108.05914
Andreas Björklund, Petteri Kaski, and Ryan Williams. Solving systems of polynomial equations over GF(2) by a parity-counting self-reduction. In Christel Baier, Ioannis Chatzigiannakis, Paola Flocchini, and Stefano Leonardi, editors, 46th International Colloquium on Automata, Languages, and Programming, ICALP 2019, July 9-12, 2019, Patras, Greece, volume 132 of LIPIcs, pages 26:1-26:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019.
Joshua Brakensiek, Sivakanth Gopi, and Venkatesan Guruswami. CSPs with global modular constraints: algorithms and hardness via polynomial representations. In Proceedings of the 51st Annual ACM Symposium on Theory of Computing (STOC), pages 590-601, 2019.
Joshua Brakensiek and Venkatesan Guruswami. Bridging between 0/1 and linear programming via random walks. In Proceedings of the 51st Annual ACM Symposium on Theory of Computing, pages 568-577, 2019.
Chris Calabro, Russell Impagliazzo, and Ramamohan Paturi. A duality between clause width and clause density for SAT. In 21st Annual IEEE Conference on Computational Complexity (CCC 2006), 16-20 July 2006, Prague, Czech Republic, pages 252-260. IEEE Computer Society, 2006.
Timothy M. Chan and R. Ryan Williams. Deterministic APSP, orthogonal vectors, and more: Quickly derandomizing Razborov-Smolensky. ACM Trans. Algorithms, 17(1):2:1-2:14, 2021.
Ruiwen Chen and Rahul Santhanam. Satisfiability on mixed instances. In Proceedings of the 2016 ACM Conference on Innovations in Theoretical Computer Science, pages 393-402, 2016.
Miguel Couceiro, Lucien Haddad, and Victor Lagerkvist. Fine-grained complexity of constraint satisfaction problems through partial polymorphisms: A survey. In 2019 IEEE 49th International Symposium on Multiple-Valued Logic (ISMVL), pages 170-175, 2019.
Itai Dinur. Improved algorithms for solving polynomial systems over GF(2) by multiple parity-counting. In Dániel Marx, editor, Proceedings of the 2021 ACM-SIAM Symposium on Discrete Algorithms, SODA 2021, Virtual Conference, January 10 - 13, 2021, pages 2550-2564. SIAM, 2021.
Rodney G. Downey and M. R. Fellows. Parameterized Complexity. Springer Publishing Company, Incorporated, 2012.
J. Flum and M. Grohe. Parameterized Complexity Theory (Texts in Theoretical Computer Science. An EATCS Series). Springer-Verlag, 2006.
Russell Impagliazzo, William Matthews, and Ramamohan Paturi. A satisfiability algorithm for AC^0. In Yuval Rabani, editor, Proceedings of the Twenty-Third Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2012, Kyoto, Japan, January 17-19, 2012, pages 961-972. SIAM, 2012.
Russell Impagliazzo and Ramamohan Paturi. On the complexity of k-sat. J. Comput. Syst. Sci., 62(2):367-375, 2001.
Russell Impagliazzo, Ramamohan Paturi, and Francis Zane. Which problems have strongly exponential complexity? J. Comput. Syst. Sci., 63(4):512-530, 2001.
Peter Jonsson, Victor Lagerkvist, Gustav Nordh, and Bruno Zanuttini. Strong partial clones and the time complexity of SAT problems. J. Comput. Syst. Sci., 84:52-78, 2017.
Peter Jonsson, Victor Lagerkvist, and Biman Roy. Fine-grained time complexity of constraint satisfaction problems. ACM Trans. Comput. Theory, 13(1):2:1-2:32, 2021.
Victor Lagerkvist and Magnus Wahlström. Which NP-hard SAT and CSP problems admit exponentially improved algorithms? CoRR, abs/1801.09488, 2018. URL: http://arxiv.org/abs/1801.09488.
http://arxiv.org/abs/1801.09488
Daniel Lokshtanov, Ramamohan Paturi, Suguru Tamaki, R. Ryan Williams, and Huacheng Yu. Beating brute force for systems of polynomial equations over finite fields. In Proceedings of the Twenty-Eighth Annual ACM-SIAM Symposium on Discrete Algorithms, pages 2190-2202, 2017.
Burkhard Monien and Ewald Speckenmeyer. Solving satisfiability in less than 2ⁿ steps. Discret. Appl. Math., 10(3):287-295, 1985.
Mihai Patrascu and Ryan Williams. On the possibility of faster SAT algorithms. In Proceedings of the Twenty-First Annual ACM-SIAM Symposium on Discrete Algorithms, pages 1065-1075, 2010.
Ramamohan Paturi, Pavel Pudlák, and Francis Zane. Satisfiability coding lemma. In 38th Annual Symposium on Foundations of Computer Science (FOCS), pages 566-574, 1997.
Thomas J. Schaefer. The complexity of satisfiability problems. In Richard J. Lipton, Walter A. Burkhard, Walter J. Savitch, Emily P. Friedman, and Alfred V. Aho, editors, Proceedings of the 10th Annual ACM Symposium on Theory of Computing, May 1-3, 1978, San Diego, California, USA, pages 216-226. ACM, 1978.
Uwe Schöning. A probabilistic algorithm for k-sat and constraint satisfaction problems. In 40th Annual Symposium on Foundations of Computer Science, pages 410-414, 1999.
Rainer Schuler. An algorithm for the satisfiability problem of formulas in conjunctive normal form. J. Algorithms, 54(1):40-44, 2005.
Mate Soos, Stephan Gocht, and Kuldeep S. Meel. Tinted, detached, and lazy CNF-XOR solving and its applications to counting and sampling. In Shuvendu K. Lahiri and Chao Wang, editors, Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part I, volume 12224 of Lecture Notes in Computer Science, pages 463-484. Springer, 2020.
Mate Soos and Kuldeep S. Meel. BIRD: engineering an efficient CNF-XOR SAT solver and its applications to approximate model counting. In The Thirty-Third AAAI Conference on Artificial Intelligence, AAAI 2019, The Thirty-First Innovative Applications of Artificial Intelligence Conference, IAAI 2019, The Ninth AAAI Symposium on Educational Advances in Artificial Intelligence, EAAI 2019, Honolulu, Hawaii, USA, January 27 - February 1, 2019, pages 1592-1599. AAAI Press, 2019.
Leslie G. Valiant and Vijay V. Vazirani. NP is as easy as detecting unique solutions. Theor. Comput. Sci., 47(3):85-93, 1986.
Vikraman Arvind and Venkatesan Guruswami
Creative Commons Attribution 4.0 International license
https://creativecommons.org/licenses/by/4.0/legalcode