Document Open Access Logo

Algorithms for the Diverse-k-SAT Problem: The Geometry of Satisfying Assignments

Authors Per Austrin , Ioana O. Bercea , Mayank Goswami , Nutan Limaye , Adarsh Srinivasan

PDF

File

Thumbnail PDF
PDF
LIPIcs.ICALP.2025.14.pdf
  • Filesize: 0.93 MB
  • 17 pages

Document Identifiers

Related Versions

Subject Classification

ACM Subject Classification
  • Theory of computation → Design and analysis of algorithms
Keywords
  • Exponential time algorithms
  • Satisfiability
  • k-SAT
  • PPZ
  • Schöning
  • Dispersion
  • Diversity

Metrics

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

Abstract

Given a k-CNF formula and an integer s ≥ 2, we study algorithms that obtain s solutions to the formula that are as dispersed as possible. For s = 2, this problem of computing the diameter of a k-CNF formula was initiated by Creszenzi and Rossi, who showed strong hardness results even for k = 2. The current best upper bound [Angelsmark and Thapper '04] goes to 4ⁿ as k → ∞. As our first result, we show that this quadratic blow up is not necessary by utilizing the Fast-Fourier transform (FFT) to give a O^*(2ⁿ) time exact algorithm for computing the diameter of any k-CNF formula. 
For s > 2, the problem was raised in the SAT community (Nadel '11) and several heuristics have been proposed for it, but no algorithms with theoretical guarantees are known. We give exact algorithms using FFT and clique-finding that run in O^*(2^{(s-1)n}) and O^*(s² |Ω_{𝐅}|^{ω ⌈ s/3 ⌉}) respectively, where |Ω_{𝐅}| is the size of the solutions space of the formula 𝐅 and ω is the matrix multiplication exponent.
However, current SAT algorithms for finding one solution run in time O^*(2^{ε_{k}n}) for ε_{k} ≈ 1-Θ(1/k), which is much faster than all above run times. As our main result, we analyze two popular SAT algorithms - PPZ (Paturi, Pudlák, Zane '97) and Schöning’s ('02) algorithms, and show that in time poly(s)O^*(2^{ε_{k}n}), they can be used to approximate diameter as well as the dispersion (s > 2) problem. While we need to modify Schöning’s original algorithm for technical reasons, we show that the PPZ algorithm, without any modification, samples solutions in a geometric sense. We believe this geometric sampling property of PPZ may be of independent interest.
Finally, we focus on diverse solutions to NP-complete optimization problems, and give bi-approximations running in time poly(s)O^*(2^{ε n}) with ε < 1 for several problems such as Maximum Independent Set, Minimum Vertex Cover, Minimum Hitting Set, Feedback Vertex Set, Multicut on Trees and Interval Vertex Deletion. For all of these problems, all existing exact methods for finding optimal diverse solutions have a runtime with at least an exponential dependence on the number of solutions s. Our methods show that by relaxing to bi-approximations, this dependence on s can be made polynomial.

Cite As Get BibTex

Per Austrin, Ioana O. Bercea, Mayank Goswami, Nutan Limaye, and Adarsh Srinivasan. Algorithms for the Diverse-k-SAT Problem: The Geometry of Satisfying Assignments. In 52nd International Colloquium on Automata, Languages, and Programming (ICALP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 334, pp. 14:1-14:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ICALP.2025.14

Author Details

Per Austrin
  • KTH Royal Institute of Technology, Stockholm, Sweden
Ioana O. Bercea
  • KTH Royal Institute of Technology, Stockholm, Sweden
Mayank Goswami
  • Queens College, City University of New York, NY, USA
Nutan Limaye
  • IT University of Copenhagen, Denmark
Adarsh Srinivasan
  • Rutgers University, Piscataway, NJ, USA

Funding

  • Bercea, Ioana O.: Received funding from Basic Algorithms Research Copenhagen(BARC), supported by VILLUM Foundation Grants 16582 and 54451.
  • Goswami, Mayank: Supported by NSF grant CCF-1910873 and received funding from Basic Algorithms Research Copenhagen(BARC), supported by VILLUM Foundation Grants 16582 and 54451.
  • Limaye, Nutan: Received funding from the Independent Research Fund Denmark (grant agreement No. 10.46540/3103-00116B) and is also supported by the Basic Algorithms Research Copenhagen (BARC), funded by VILLUM Foundation Grants 16582 and 54451. Was also supported by Digital Research Centre Denmark, project P40.
  • Srinivasan, Adarsh: Supported by the National Science Foundation under grants CCF-2313372 and CCF-2443697 and a grant from the Simons Foundation, Grant Number 825876, Awardee Thu D. Nguyen, and received funding from Basic Algorithms Research Copenhagen(BARC), supported by VILLUM Foundation Grants 16582 and 54451.

References

  1. Amir Abboud, Vincent Cohen-Addad, Euiwoong Lee, and Pasin Manurangsi. Improved approximation algorithms and lower bounds for search-diversification problems. In Mikolaj Bojanczyk, Emanuela Merelli, and David P. Woodruff, editors, 49th International Colloquium on Automata, Languages, and Programming, ICALP 2022, July 4-8, 2022, Paris, France, volume 229 of LIPIcs, pages 7:1-7:18. Schloss-Dagstuhl-Leibniz Zentrum für Informatik, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2022. URL: https://doi.org/10.4230/LIPIcs.ICALP.2022.7.
  2. Sabih Agbaria, Dan Carmi, Orly Cohen, Dmitry Korchemny, Michael Lifshits, and Alexander Nadel. Sat-based semiformal verification of hardware. In Roderick Bloem and Natasha Sharygina, editors, Proceedings of 10th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2010, Lugano, Switzerland, October 20-23, pages 25-32. IEEE, IEEE, 2010. URL: https://ieeexplore.ieee.org/document/5770929/.
  3. Josh Alman and Ryan Williams. Probabilistic polynomials and hamming nearest neighbors. In Venkatesan Guruswami, editor, IEEE 56th Annual Symposium on Foundations of Computer Science, FOCS 2015, Berkeley, CA, USA, 17-20 October, 2015, pages 136-150. IEEE, IEEE Computer Society, 2015. URL: https://doi.org/10.1109/FOCS.2015.18.
  4. Ola Angelsmark and Johan Thapper. Algorithms for the maximum Hamming distance problem. In Boi Faltings, Adrian Petcu, François Fages, and Francesca Rossi, editors, International Workshop on Constraint Solving and Constraint Logic Programming, volume 3419 of Lecture Notes in Computer Science, pages 128-141. Springer, 2004. URL: https://doi.org/10.1007/11402763_10.
  5. Ola Angelsmark and Johan Thapper. A microstructure based approach to constraint satisfaction optimisation problems. In Ingrid Russell and Zdravko Markov, editors, Proceedings of the Eighteenth International Florida Artificial Intelligence Research Society Conference, Clearwater Beach, Florida, USA, pages 155-160. AAAI Press, 2005. URL: http://www.aaai.org/Library/FLAIRS/2005/flairs05-026.php.
  6. Andrea Arcuri and Lionel C. Briand. Formal analysis of the probability of interaction fault detection using random testing. IEEE Trans. Software Eng., 38(5):1088-1099, 2012. URL: https://doi.org/10.1109/TSE.2011.85.
  7. Per Austrin, Ioana O Bercea, Mayank Goswami, Nutan Limaye, and Adarsh Srinivasan. Algorithms for the diverse-k-sat problem: the geometry of satisfying assignments. arXiv preprint arXiv:2408.03465, 2024. URL: https://doi.org/10.48550/arXiv.2408.03465.
  8. Nikhil Bansal, Kamal Jain, Anna Kazeykina, and Joseph Naor. Approximation algorithms for diversified search ranking. In Samson Abramsky, Cyril Gavoille, Claude Kirchner, Friedhelm Meyer auf der Heide, and Paul G. Spirakis, editors, Automata, Languages and Programming, 37th International Colloquium, ICALP 2010, Bordeaux, France, July 6-10, 2010, Proceedings, Part II, volume 6199 of Lecture Notes in Computer Science, pages 273-284. Springer, Springer, 2010. URL: https://doi.org/10.1007/978-3-642-14162-1_23.
  9. Julien Baste, Michael R. Fellows, Lars Jaffke, Tomás Masarík, Mateus de Oliveira Oliveira, Geevarghese Philip, and Frances A. Rosamond. Diversity of solutions: An exploration through the lens of fixed-parameter tractability theory. Artif. Intell., 303:103644, 2022. URL: https://doi.org/10.1016/j.artint.2021.103644.
  10. Julien Baste, Lars Jaffke, Tomás Masarík, Geevarghese Philip, and Günter Rote. FPT algorithms for diverse collections of hitting sets. Algorithms, 12(12):254, 2019. URL: https://doi.org/10.3390/a12120254.
  11. Sven Baumer and Rainer Schuler. Improving a probabilistic 3-SAT algorithm by dynamic search and independent clause pairs. In Enrico Giunchiglia and Armando Tacchella, editors, Theory and Applications of Satisfiability Testing, 6th International Conference, SAT 2003. Santa Margherita Ligure, Italy, May 5-8, 2003 Selected Revised Papers, volume 2919 of Lecture Notes in Computer Science, pages 150-161. Springer, Springer, 2003. URL: https://doi.org/10.1007/978-3-540-24605-3_12.
  12. Allan Borodin, Hyun Chul Lee, and Yuli Ye. Max-sum diversification, monotone submodular functions and dynamic updates. In Michael Benedikt, Markus Krötzsch, and Maurizio Lenzerini, editors, Proceedings of the 31st ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, PODS 2012, Scottsdale, AZ, USA, May 20-24, 2012, pages 155-166. ACM, 2012. URL: https://doi.org/10.1145/2213556.2213580.
  13. Chris Calabro. The exponential complexity of satisfiability problems. PhD thesis, University of California, San Diego, USA, 2009. URL: http://www.escholarship.org/uc/item/0pk5w64k.
  14. 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.
  15. Jean Cardinal, Jerri Nummenpalo, and Emo Welzl. Solving and sampling with many solutions: Satisfiability and other hard problems. In Daniel Lokshtanov and Naomi Nishimura, editors, 12th International Symposium on Parameterized and Exact Computation, IPEC 2017, September 6-8, 2017, Vienna, Austria, volume 89 of LIPIcs, pages 11:1-11:12. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.IPEC.2017.11.
  16. Alfonso Cevallos, Friedrich Eisenbrand, and Rico Zenklusen. An improved analysis of local search for max-sum diversification. Math. Oper. Res., 44(4):1494-1509, 2019. URL: https://doi.org/10.1287/moor.2018.0982.
  17. Zongchen Chen and Nitya Mani. From algorithms to connectivity and back: Finding a giant component in random k-sat. In Nikhil Bansal and Viswanath Nagarajan, editors, Proceedings of the 2023 ACM-SIAM Symposium on Discrete Algorithms, SODA 2023, Florence, Italy, January 22-25, 2023, pages 3437-3470. SIAM, SIAM, 2023. URL: https://doi.org/10.1137/1.9781611977554.ch132.
  18. Pierluigi Crescenzi and Gianluca Rossi. On the Hamming distance of constraint satisfaction problems. Theor. Comput. Sci., 288(1):85-100, 2002. URL: https://doi.org/10.1016/S0304-3975(01)00146-3.
  19. Uriel Feige, Abraham D. Flaxman, and Dan Vilenchik. On the diameter of the set of satisfying assignments in random satisfiable k-cnf formulas. SIAM J. Discret. Math., 25(2):736-749, 2011. URL: https://doi.org/10.1137/090749323.
  20. Fedor V. Fomin, Serge Gaspers, Daniel Lokshtanov, and Saket Saurabh. Exact algorithms via monotone local search. J. ACM, 66(2):8:1-8:23, March 2019. URL: https://doi.org/10.1145/3284176.
  21. Fedor V. Fomin and Petteri Kaski. Exact exponential algorithms. Commun. ACM, 56(3):80-88, 2013. URL: https://doi.org/10.1145/2428556.2428575.
  22. Jie Gao, Mayank Goswami, Karthik C. S., Meng-Tsung Tsai, Shih-Yu Tsai, and Hao-Tsung Yang. Obtaining approximately optimal and diverse solutions via dispersion. In Armando Castañeda and Francisco Rodríguez-Henríquez, editors, LATIN 2022: Theoretical Informatics - 15th Latin American Symposium, Guanajuato, Mexico, November 7-11, 2022, Proceedings, volume 13568 of Lecture Notes in Computer Science, pages 222-239. Springer, Springer, 2022. URL: https://doi.org/10.1007/978-3-031-20624-5_14.
  23. Carla P. Gomes, Ashish Sabharwal, and Bart Selman. Near-uniform sampling of combinatorial spaces using XOR constraints. In Bernhard Schölkopf, John C. Platt, and Thomas Hofmann, editors, Advances in Neural Information Processing Systems 19, Proceedings of the Twentieth Annual Conference on Neural Information Processing Systems, Vancouver, British Columbia, Canada, December 4-7, 2006, volume 19, pages 481-488. MIT Press, 2006. URL: https://proceedings.neurips.cc/paper/2006/hash/4110a1994471c595f7583ef1b74ba4cb-Abstract.html.
  24. Teofilo F. Gonzalez. Clustering to minimize the maximum intercluster distance. Theor. Comput. Sci., 38:293-306, 1985. URL: https://doi.org/10.1016/0304-3975(85)90224-5.
  25. Elena Grigorescu, Tali Kaufman, and Madhu Sudan. Succinct representation of codes with applications to testing. SIAM J. Discret. Math., 26(4):1618-1634, 2012. URL: https://doi.org/10.1137/100818364.
  26. Mohit Gurumukhani, Ramamohan Paturi, Pavel Pudlák, Michael E. Saks, and Navid Talebanfard. Local enumeration and majority lower bounds. CoRR, abs/2403.09134, 2024. URL: https://doi.org/10.48550/arXiv.2403.09134.
  27. Venkatesan Guruswami, Johan Håstad, and Swastik Kopparty. On the list-decodability of random linear codes. In Leonard J. Schulman, editor, Proceedings of the 42nd ACM Symposium on Theory of Computing, STOC 2010, Cambridge, Massachusetts, USA, 5-8 June 2010, pages 409-416. ACM, 2010. URL: https://doi.org/10.1145/1806689.1806747.
  28. Thomas Dueholm Hansen, Haim Kaplan, Or Zamir, and Uri Zwick. Faster k-sat algorithms using biased-ppsz. In Moses Charikar and Edith Cohen, editors, Proceedings of the 51st Annual ACM SIGACT Symposium on Theory of Computing, STOC 2019, Phoenix, AZ, USA, June 23-26, 2019, pages 578-589. ACM, 2019. URL: https://doi.org/10.1145/3313276.3316359.
  29. Emmanuel Hebrard, Brahim Hnich, Barry O'Sullivan, and Toby Walsh. Finding diverse and similar solutions in constraint programming. In Manuela M. Veloso and Subbarao Kambhampati, editors, Proceedings, The Twentieth National Conference on Artificial Intelligence and the Seventeenth Innovative Applications of Artificial Intelligence Conference, July 9-13, 2005, Pittsburgh, Pennsylvania, USA, volume 5, pages 372-377. AAAI Press / The MIT Press, 2005. URL: http://www.aaai.org/Library/AAAI/2005/aaai05-059.php.
  30. Timon Hertli. Breaking the PPSZ barrier for unique 3-sat. In Javier Esparza, Pierre Fraigniaud, Thore Husfeldt, and Elias Koutsoupias, editors, Automata, Languages, and Programming - 41st International Colloquium, ICALP 2014, Copenhagen, Denmark, July 8-11, 2014, Proceedings, Part I, volume 8572 of Lecture Notes in Computer Science, pages 600-611. Springer, Springer, 2014. URL: https://doi.org/10.1007/978-3-662-43948-7_50.
  31. Timon Hertli, Robin A. Moser, and Dominik Scheder. Improving PPSZ for 3-sat using critical variables. In Thomas Schwentick and Christoph Dürr, editors, 28th International Symposium on Theoretical Aspects of Computer Science, STACS 2011, March 10-12, 2011, Dortmund, Germany, volume 9 of LIPIcs, pages 237-248. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011. URL: https://doi.org/10.4230/LIPIcs.STACS.2011.237.
  32. Edward A. Hirsch. A fast deterministic algorithm for formulas that have many satisfying assignments. Log. J. IGPL, 6(1):59-71, 1998. URL: https://doi.org/10.1093/jigpal/6.1.59.
  33. Thomas Hofmeister, Uwe Schöning, Rainer Schuler, and Osamu Watanabe. A probabilistic 3-SAT algorithm further improved. In Helmut Alt and Afonso Ferreira, editors, STACS 2002, 19th Annual Symposium on Theoretical Aspects of Computer Science, Antibes - Juan les Pins, France, March 14-16, 2002, Proceedings, volume 2285 of Lecture Notes in Computer Science, pages 192-202. Springer, Springer, 2002. URL: https://doi.org/10.1007/3-540-45841-7_15.
  34. 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.
  35. Russell Impagliazzo, Ramamohan Paturi, and Francis Zane. Which problems have strongly exponential complexity? J. Comput. Syst. Sci., 63(4):512-530, 2001. URL: https://doi.org/10.1006/jcss.2001.1774.
  36. Piotr Indyk, Sepideh Mahabadi, Mohammad Mahdian, and Vahab S. Mirrokni. Composable core-sets for diversity and coverage maximization. In Richard Hull and Martin Grohe, editors, Proceedings of the 33rd ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems, PODS'14, Snowbird, UT, USA, June 22-27, 2014, pages 100-108. ACM, 2014. URL: https://doi.org/10.1145/2594538.2594560.
  37. Daniel Kane and Osamu Watanabe. A short implicant of a CNF formula with many satisfying assignments. Algorithmica, 76(4):1203-1223, 2016. URL: https://doi.org/10.1007/s00453-016-0125-z.
  38. Nathan Kitchen and Andreas Kuehlmann. Stimulus generation for constrained random simulation. In Georges G. E. Gielen, editor, 2007 International Conference on Computer-Aided Design, ICCAD 2007, San Jose, CA, USA, November 5-8, 2007, pages 258-265. IEEE, IEEE Computer Society, 2007. URL: https://doi.org/10.1109/ICCAD.2007.4397275.
  39. Sixue Liu. Chain, generalization of covering code, and deterministic algorithm for k-sat. In Ioannis Chatzigiannakis, Christos Kaklamanis, Dániel Marx, and Donald Sannella, editors, 45th International Colloquium on Automata, Languages, and Programming, ICALP 2018, July 9-13, 2018, Prague, Czech Republic, volume 107 of LIPIcs, pages 88:1-88:13. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2018. URL: https://doi.org/10.4230/LIPIcs.ICALP.2018.88.
  40. Alexander Nadel. Generating diverse solutions in SAT. In Karem A. Sakallah and Laurent Simon, editors, Theory and Applications of Satisfiability Testing - SAT 2011 - 14th International Conference, SAT 2011, Ann Arbor, MI, USA, June 19-22, 2011. Proceedings, volume 6695 of Lecture Notes in Computer Science, pages 287-301. Springer, Springer, 2011. URL: https://doi.org/10.1007/978-3-642-21581-0_23.
  41. 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.
  42. Ramamohan Paturi, Pavel Pudlák, and Francis Zane. Satisfiability coding lemma. Chic. J. Theor. Comput. Sci., 1999:566, 1999. URL: http://cjtcs.cs.uchicago.edu/articles/1999/11/contents.html.
  43. Thierry Petit and Andrew C. Trapp. Enriching solutions to combinatorial problems via solution engineering. INFORMS J. Comput., 31(3):429-444, 2019. URL: https://doi.org/10.1287/ijoc.2018.0855.
  44. Quentin Plazar, Mathieu Acher, Gilles Perrouin, Xavier Devroey, and Maxime Cordy. Uniform sampling of SAT solutions for configurable systems: Are we there yet? In 12th IEEE Conference on Software Testing, Validation and Verification, ICST 2019, Xi'an, China, April 22-27, 2019, pages 240-251. IEEE, IEEE, 2019. URL: https://doi.org/10.1109/ICST.2019.00032.
  45. Ron M. Roth. Introduction to Coding Theory. Cambridge University Press, 2006. Google Scholar
  46. 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. URL: https://doi.org/10.1145/800133.804350.
  47. Dominik Scheder. PPSZ for k ≥ 5: More is better. ACM Trans. Comput. Theory, 11(4):25:1-25:22, 2019. URL: https://doi.org/10.1145/3349613.
  48. Dominik Scheder. PPSZ is better than you think. In 62nd IEEE Annual Symposium on Foundations of Computer Science, FOCS 2021, Denver, CO, USA, February 7-10, 2022, pages 205-216. IEEE, IEEE, 2021. URL: https://doi.org/10.1109/FOCS52979.2021.00028.
  49. Dominik Scheder and John P. Steinberger. PPSZ for general k-sat - making hertli’s analysis simpler and 3-sat faster. In Ryan O'Donnell, editor, 32nd Computational Complexity Conference, CCC 2017, July 6-9, 2017, Riga, Latvia, volume 79 of LIPIcs, pages 9:1-9:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.CCC.2017.9.
  50. Manuel Schmitt and Rolf Wanka. Exploiting independent subformulas: A faster approximation scheme for #k-sat. Inf. Process. Lett., 113(9):337-344, 2013. URL: https://doi.org/10.1016/j.ipl.2013.02.013.
  51. Uwe Schöning. A probabilistic algorithm for k -sat based on limited local search and restart. Algorithmica, 32(4):615-623, 2002. URL: https://doi.org/10.1007/s00453-001-0094-7.
  52. Virginia Vassilevska Williams. Some open problems in fine-grained complexity. SIGACT News, 49(4):29-35, December 2018. URL: https://doi.org/10.1145/3300150.3300158.
  53. Virginia Vassilevska Williams, Yinzhan Xu, Zixuan Xu, and Renfei Zhou. New bounds for matrix multiplication: from alpha to omega. In David P. Woodruff, editor, Proceedings of the 2024 ACM-SIAM Symposium on Discrete Algorithms, SODA 2024, Alexandria, VA, USA, January 7-10, 2024, pages 3792-3835. SIAM, SIAM, 2024. URL: https://doi.org/10.1137/1.9781611977912.134.
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-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact