Document Open Access Logo

CNF Satisfiability in a Subspace and Related Problems

Authors Vikraman Arvind, Venkatesan Guruswami

PDF
Thumbnail PDF

File

LIPIcs.IPEC.2021.5.pdf
  • Filesize: 0.78 MB
  • 15 pages

Document Identifiers

Author Details

Vikraman Arvind
  • The Institute of Mathematical Sciences (HBNI), Chennai, India
Venkatesan Guruswami
  • Computer Science Department, Carnegie Mellon University, Pittsburgh, PA, USA

Funding

  • Guruswami, Venkatesan: 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.

Acknowledgements

We thank anonymous reviewers for useful comments and pointers to the literature.

Cite AsGet BibTex

Vikraman Arvind and Venkatesan Guruswami. CNF Satisfiability in a Subspace and Related Problems. In 16th International Symposium on Parameterized and Exact Computation (IPEC 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 214, pp. 5:1-5:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.IPEC.2021.5

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 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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Parameterized complexity and exact algorithms
Keywords
  • CNF Satisfiability
  • Exact exponential algorithms
  • Hardness results

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Vikraman Arvind and Venkatesan Guruswami. Cnf satisfiability in a subspace and related problems, 2021. URL: http://arxiv.org/abs/2108.05914.
  2. 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. Google Scholar
  3. 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. Google Scholar
  4. 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. Google Scholar
  5. 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. Google Scholar
  6. 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. Google Scholar
  7. 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. Google Scholar
  8. 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. Google Scholar
  9. 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. Google Scholar
  10. Rodney G. Downey and M. R. Fellows. Parameterized Complexity. Springer Publishing Company, Incorporated, 2012. Google Scholar
  11. J. Flum and M. Grohe. Parameterized Complexity Theory (Texts in Theoretical Computer Science. An EATCS Series). Springer-Verlag, 2006. Google Scholar
  12. 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. Google Scholar
  13. Russell Impagliazzo and Ramamohan Paturi. On the complexity of k-sat. J. Comput. Syst. Sci., 62(2):367-375, 2001. Google Scholar
  14. Russell Impagliazzo, Ramamohan Paturi, and Francis Zane. Which problems have strongly exponential complexity? J. Comput. Syst. Sci., 63(4):512-530, 2001. Google Scholar
  15. 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. Google Scholar
  16. 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. Google Scholar
  17. 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.
  18. 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. Google Scholar
  19. Burkhard Monien and Ewald Speckenmeyer. Solving satisfiability in less than 2ⁿ steps. Discret. Appl. Math., 10(3):287-295, 1985. Google Scholar
  20. 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. Google Scholar
  21. 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. Google Scholar
  22. 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. Google Scholar
  23. 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. Google Scholar
  24. Rainer Schuler. An algorithm for the satisfiability problem of formulas in conjunctive normal form. J. Algorithms, 54(1):40-44, 2005. Google Scholar
  25. 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. Google Scholar
  26. 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. Google Scholar
  27. Leslie G. Valiant and Vijay V. Vazirani. NP is as easy as detecting unique solutions. Theor. Comput. Sci., 47(3):85-93, 1986. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact