Document Open Access Logo

New Algorithms for Parity-SAT and Its Bounded-Occurrence Versions

Authors Sanjay Jain , Junqiang Peng , Frank Stephan , Haoyun Tang , Mingyu Xiao

PDF

File

Thumbnail PDF
PDF
LIPIcs.SAT.2026.20.pdf
  • Filesize: 1.04 MB
  • 20 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Design and analysis of algorithms
Keywords
  • Parity-SAT
  • Exact Exponential Algorithms

Metrics

Abstract

Parity-SAT is the problem of determining whether a given CNF formula has an odd number of satisfying assignments. As a canonical ⊕P-complete problem, it represents a fundamental variant of the exact model counting problem (#SAT). Under the Strong Exponential Time Hypothesis (SETH), Parity-SAT admits no O^*((2-ε)ⁿ)-time or O^*((2-ε)^m)-time algorithm for any constant ε > 0, where n and m denote the numbers of variables and clauses, respectively. Thus, breaking the 2ⁿ or 2^m barrier appears impossible in full generality.
In this work, we revisit this barrier through structural restrictions and a refined exploitation of parity. We study Parity-d-occ-SAT, where each variable appears in at most d clauses, and obtain three main results. First, we design {a randomized} O^*(2^{m(1-1/O(d))})-time algorithm, thereby breaking the 2^m barrier for every fixed d. Second, for the special case d = 2, we develop a significantly sharper branching algorithm running in O^*(1.1193ⁿ) time or O^*(1.3248^m) time. Third, leveraging the structural insights underlying the d = 2 case, we obtain an O^*(1.1052^L)-time algorithm for general Parity-SAT, where L denotes the formula length. All algorithms use only polynomial space. Notably, our running-time bounds are better than the best known bounds for the corresponding exact counting counterparts, highlighting a genuine algorithmic advantage of parity over counting. Conceptually, our results demonstrate that parity admits finer structural reductions and more efficient branching than exact model counting, and that bounded occurrence can be systematically leveraged to circumvent classical exponential barriers.

Cite As Get BibTex

Sanjay Jain, Junqiang Peng, Frank Stephan, Haoyun Tang, and Mingyu Xiao. New Algorithms for Parity-SAT and Its Bounded-Occurrence Versions. In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 20:1-20:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.SAT.2026.20

Author Details

Sanjay Jain
  • School of Computing, National University of Singapore, Singapore
Junqiang Peng
  • University of Electronic Science and Technology of China, Chengdu, China
Frank Stephan
  • Department of Mathematics, National University of Singapore, Singapore
  • School of Computing, National University of Singapore, Singapore
Haoyun Tang
  • School of Computing, National University of Singapore, Singapore
Mingyu Xiao
  • University of Electronic Science and Technology of China, Chengdu, China

Funding

Junqiang Peng and Mingyu Xiao were supported by the National Natural Science Foundation of China, under the grants 62372095 and 62502078. Sanjay Jain and Frank Stephan were supported by Singapore Ministry of Education (MOE) AcRF Tier 2 grant MOE-000538-01. Additionally, Sanjay Jain was supported by NUS grant E-252-00-0021-01. Additionally, Frank Stephan was supported by AcRF Tier 1 grants A-0008454-00-00 and A-0008494-00-00.

References

  1. Amir Abboud, Shon Feller, and Oren Weimann. On the fine-grained complexity of parity problems. In Proceedings of the 47th International Colloquium on Automata, Languages, and Programming (ICALP 2020), pages 5:1-5:19, 2020. URL: https://doi.org/10.4230/LIPIcs.ICALP.2020.5.
  2. Vikraman Arvind and Piyush P. Kurur. Graph isomorphism is in SPP. Inf. Comput., 204(5):835-852, 2006. URL: https://doi.org/10.1016/J.IC.2006.02.002.
  3. Fahiem Bacchus, Shannon Dalmao, and Toniann Pitassi. Algorithms and complexity results for #sat and bayesian inference. In Proceedings of the 44th Annual Symposium on Foundations of Computer Science (FOCS 2003), pages 340-351, 2003. URL: https://doi.org/10.1109/SFCS.2003.1238208.
  4. Max Bannach, Erik D. Demaine, Timothy Gomez, and Markus Hecher. #p is sandwiched by one and two #2dnf calls: Is subtraction stronger than we thought? In Proceedings of the 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS 2025), pages 31-43, 2025. URL: https://doi.org/10.1109/LICS65433.2025.00010.
  5. Max Bannach, Erik D. Demaine, Timothy Gomez, and Markus Hecher. A novel reduction from #sat to #2sat based on symmetry: Simply Drop the Large Clauses. In Proceedings of the 2026 Symposium on Simplicity in Algorithms (SOSA 2026), pages 254-265, 2026. URL: https://doi.org/10.1137/1.9781611978964.19.
  6. Andreas Björklund, Holger Dell, and Thore Husfeldt. The parity of set systems under random restrictions with applications to exponential time problems. In Proceedings of the 42nd International Colloquium on Automata, Languages, and Programming (ICALP 2015), pages 231-242, 2015. URL: https://doi.org/10.1007/978-3-662-47672-7_19.
  7. Andreas Björklund and Thore Husfeldt. The parity of directed hamiltonian cycles. In Proceedings of the 54th Annual IEEE Symposium on Foundations of Computer Science (FOCS 2013), pages 727-735, 2013. URL: https://doi.org/10.1109/FOCS.2013.83.
  8. Chris Calabro, Russell Impagliazzo, Valentine Kabanets, and Ramamohan Paturi. The complexity of unique k-sat: An isolation lemma for k-cnfs. J. Comput. Syst. Sci., 74(3):386-393, 2008. URL: https://doi.org/10.1016/J.JCSS.2007.06.015.
  9. Chris Calabro, Russell Impagliazzo, and Ramamohan Paturi. A duality between clause width and clause density for SAT. In Proceedings of the 21st Annual IEEE Conference on Computational Complexity (CCC 2006), pages 252-260, 2006. URL: https://doi.org/10.1109/CCC.2006.6.
  10. Timothy M. Chan and Ryan Williams. Deterministic apsp, orthogonal vectors, and more: Quickly derandomizing razborov-smolensky. In Proceedings of the 27th Annual ACM-SIAM Symposium on Discrete Algorithms (SODA 2016), pages 1246-1255, 2016. URL: https://doi.org/10.1137/1.9781611974331.CH87.
  11. Mark Chavira and Adnan Darwiche. On probabilistic inference by weighted model counting. Artif. Intell., 172(6-7):772-799, 2008. URL: https://doi.org/10.1016/J.ARTINT.2007.11.002.
  12. Huairui Chu, Mingyu Xiao, and Zhe Zhang. An improved upper bound for SAT. Theor. Comput. Sci., 887:51-62, 2021. URL: https://doi.org/10.1016/J.TCS.2021.06.045.
  13. Stephen A. Cook. The complexity of theorem-proving procedures. In Proceedings of the 3rd Annual ACM Symposium on Theory of Computing (STOC 1971), pages 151-158, 1971. URL: https://doi.org/10.1145/800157.805047.
  14. Radu Curticapean, Holger Dell, and Thore Husfeldt. Modular counting of subgraphs: Matchings, matching-splittable graphs, and paths. In Proceedings of the 29th Annual European Symposium on Algorithms (ESA 2021), pages 34:1-34:17, 2021. URL: https://doi.org/10.4230/LIPIcs.ESA.2021.34.
  15. Marek Cygan, Holger Dell, Daniel Lokshtanov, Dániel Marx, Jesper Nederlof, Yoshio Okamoto, Ramamohan Paturi, Saket Saurabh, and Magnus Wahlström. On problems as hard as CNF-SAT. ACM Trans. Algorithms, 12(3):41:1-41:24, 2016. URL: https://doi.org/10.1145/2925416.
  16. Evgeny Dantsin and Edward A. Hirsch. Worst-case upper bounds. In Handbook of Satisfiability - Second Edition, pages 669-692. IOS Press, 2021. URL: https://doi.org/10.3233/FAIA200999.
  17. Holger Dell, Thore Husfeldt, Dániel Marx, Nina Taslaman, and Martin Wahlen. Exponential time complexity of the permanent and the tutte polynomial. ACM Trans. Algorithms, 10(4):21:1-21:32, 2014. URL: https://doi.org/10.1145/2635812.
  18. Leonardo Dueñas-Osorio, Kuldeep S. Meel, Roger Paredes, and Moshe Y. Vardi. Counting-based reliability estimation for power-transmission grids. In Proceedings of the 31st AAAI Conference on Artificial Intelligence (AAAI 2017), pages 4488-4494, 2017. URL: https://doi.org/10.1609/AAAI.V31I1.11178.
  19. Fedor V. Fomin, Fabrizio Grandoni, and Dieter Kratsch. A measure & conquer approach for the analysis of exact algorithms. J. ACM, 56(5):25:1-25:32, 2009. URL: https://doi.org/10.1145/1552285.1552286.
  20. Fedor V. Fomin and Kjartan Høie. Pathwidth of cubic graphs and exact algorithms. Inf. Process. Lett., 97(5):191-196, 2006. URL: https://doi.org/10.1016/J.IPL.2005.10.012.
  21. Fedor V. Fomin and Dieter Kratsch. Exact Exponential Algorithms. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2010. URL: https://doi.org/10.1007/978-3-642-16533-7.
  22. Serge Gaspers and Gregory B. Sorkin. Separate, measure and conquer: Faster polynomial-space algorithms for max 2-csp and counting dominating sets. ACM Trans. Algorithms, 13(4):44:1-44:36, 2017. URL: https://doi.org/10.1145/3111499.
  23. Leslie Ann Goldberg and Marc Roth. Parameterised and fine-grained subgraph counting, modulo 2. Algorithmica, 86(4):944-1005, 2024. URL: https://doi.org/10.1007/S00453-023-01178-0.
  24. Gordon Hoi, Sanjay Jain, Ammar Fathin Sabili, and Frank Stephan. A bisection approach to subcubic maximum induced matching. In Proceedings of the 18th International Conference and Workshops on Algorithms and Computation (WALCOM 2024), pages 257-272, 2024. URL: https://doi.org/10.1007/978-981-97-0566-5_19.
  25. Gordon Hoi, Sanjay Jain, and Frank Stephan. A faster exact algorithm to count X3SAT solutions. In Proceedings of the 26th International Conference on Principles and Practice of Constraint Programming (CP 2020), pages 375-391, 2020. URL: https://doi.org/10.1007/978-3-030-58475-7_22.
  26. Russell Impagliazzo, William Matthews, and Ramamohan Paturi. A satisfiability algorithm for ac^0. In Proceedings of the 23rd Annual ACM-SIAM Symposium on Discrete Algorithms (SODA 2012), pages 961-972, 1992. URL: https://doi.org/10.1137/1.9781611973099.77.
  27. Russell Impagliazzo and Ramamohan Paturi. On the complexity of k-sat. J. Comput. Syst. Sci., 62(2):367-375, 2001. URL: https://doi.org/10.1006/JCSS.2000.1727.
  28. Kazuo Iwama. CNF satisfiability test by counting and polynomial average time. SIAM J. Comput., 18(2):385-391, 1989. URL: https://doi.org/10.1137/0218026.
  29. Sixue Liu. Chain, generalization of covering code, and deterministic algorithm for k-SAT. In Proceedings of the 45th International Colloquium on Automata, Languages, and Programming (ICALP 2018), pages 88:1-88:13, 2018. URL: https://doi.org/10.4230/LIPIcs.ICALP.2018.88.
  30. Eliezer L. Lozinskii. Counting propositional models. Inf. Process. Lett., 41(6):327-332, 1992. URL: https://doi.org/10.1016/0020-0190(92)90160-W.
  31. Burkhard Monien and Robert Preis. Upper bounds on the bisection width of 3- and 4-regular graphs. J. Discrete Algorithms, 4(3):475-498, 2006. URL: https://doi.org/10.1016/J.JDA.2005.12.009.
  32. Nina Narodytska, Aditya A. Shrotri, Kuldeep S. Meel, Alexey Ignatiev, and João Marques-Silva. Assessing heuristic machine learning explanations with model counting. In Proceedings of the 22nd International Conference on Theory and Applications of Satisfiability Testing (SAT 2019), pages 267-278, 2019. URL: https://doi.org/10.1007/978-3-030-24258-9_19.
  33. Christos H. Papadimitriou and Stathis Zachos. Two remarks on the power of counting. In Proceedings of the 6th GI Conference on Theoretical Computer Science, pages 269-276, 1983. URL: https://doi.org/10.1007/BFb0009651.
  34. Ramamohan Paturi, Pavel Pudlák, Michael E. Saks, and Francis Zane. An improved exponential-time algorithm for k-sat. J. ACM, 52(3):337-364, 2005. URL: https://doi.org/10.1145/1066100.1066101.
  35. Ramamohan Paturi, Pavel Pudlák, and Francis Zane. Satisfiability coding lemma. In Proceedings of the 38th Annual Symposium on Foundations of Computer Science (FOCS 1997), pages 566-574, 1997. URL: https://doi.org/10.1109/SFCS.1997.646146.
  36. Junqiang Peng, Zimo Sheng, and Mingyu Xiao. New algorithms for #2-sat and #3-sat. In Proceedings of the 34th International Joint Conference on Artificial Intelligence (IJCAI 2025), pages 2666-2674, 2025. URL: https://doi.org/10.24963/IJCAI.2025/297.
  37. Junqiang Peng and Mingyu Xiao. Further improvements for SAT in terms of formula length. Inf. Comput., 294:105085, 2023. URL: https://doi.org/10.1016/J.IC.2023.105085.
  38. Dan Roth. On the hardness of approximate reasoning. Artif. Intell., 82(1-2):273-302, 1996. URL: https://doi.org/10.1016/0004-3702(94)00092-1.
  39. Tian Sang, Paul Beame, and Henry A. Kautz. Performing bayesian inference by weighted model counting. In Proceedings of the 20th National Conference on Artificial Intelligence (AAAI 2005), pages 475-482, 2005. URL: http://www.aaai.org/Library/AAAI/2005/aaai05-075.php.
  40. Dominik Scheder. PPSZ is better than you think. In Proceedings of the 62nd IEEE Annual Symposium on Foundations of Computer Science (FOCS 2021), pages 205-216, 2021. URL: https://doi.org/10.1109/FOCS52979.2021.00028.
  41. Uwe Schöning. A probabilistic algorithm for k-sat and constraint satisfaction problems. In Proceedings of the 40th Annual Symposium on Foundations of Computer Science (FOCS 1999), pages 410-414, 1999. URL: https://doi.org/10.1109/SFFCS.1999.814612.
  42. Seinosuke Toda. PP is as hard as the polynomial-time hierarchy. SIAM Journal on Computing, 20(5):865-877, 1991. URL: https://doi.org/10.1137/0220053.
  43. Patrick Traxler. The time complexity of constraint satisfaction. In Proceedings of the 3rd International Workshop on Parameterized and Exact Computation (IWPEC 2008), pages 190-201, 2008. URL: https://doi.org/10.1007/978-3-540-79723-4_18.
  44. Leslie G. Valiant. The complexity of computing the permanent. Theor. Comput. Sci., 8:189-201, 1979. URL: https://doi.org/10.1016/0304-3975(79)90044-6.
  45. Leslie G. Valiant. Accidental algorithms. In Proceedings of the 47th Annual IEEE Symposium on Foundations of Computer Science (FOCS 2006), pages 509-517, 2006. URL: https://doi.org/10.1109/FOCS.2006.7.
  46. Leslie G. Valiant and Vijay V. Vazirani. NP is as easy as detecting unique solutions. Theor. Comput. Sci., 47(3):85-93, 1986. URL: https://doi.org/10.1016/0304-3975(86)90135-0.
  47. Magnus Wahlström. A tighter bound for counting max-weight solutions to 2sat instances. In Proceedings of the 3rd International Workshop on Parameterized and Exact Computation (IWPEC 2008), pages 202-213, 2008. URL: https://doi.org/10.1007/978-3-540-79723-4_19.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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