Document Open Access Logo

On the Parameterized Complexity of Diverse SAT

Authors Neeldhara Misra , Harshil Mittal, Ashutosh Rai

PDF
Thumbnail PDF

File

LIPIcs.ISAAC.2024.50.pdf
  • Filesize: 0.8 MB
  • 18 pages

Document Identifiers

Author Details

Neeldhara Misra
  • Department of Computer Science and Engineering, Indian Institute of Technology Gandhinagar, India
Harshil Mittal
  • Department of Computer Science and Engineering, Indian Institute of Technology Gandhinagar, India
Ashutosh Rai
  • Department of Mathematics, Indian Institute of Technology Delhi, New Delhi, India

Funding

  • Misra, Neeldhara: Supported by IIT Gandhinagar and the SERB ECR grant ECR/2018/ 002967.
  • Mittal, Harshil: Supported by IIT Gandhinagar and Google as an ISAAC sponsor.
  • Rai, Ashutosh: Supported by IIT Delhi.

Acknowledgements

We thank Saraswati Girish Nanoti for helpful discussions.

Cite As Get BibTex

Neeldhara Misra, Harshil Mittal, and Ashutosh Rai. On the Parameterized Complexity of Diverse SAT. In 35th International Symposium on Algorithms and Computation (ISAAC 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 322, pp. 50:1-50:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.ISAAC.2024.50

Abstract

We study the Boolean Satisfiability problem (SAT) in the framework of diversity, where one asks for multiple solutions that are mutually far apart (i.e., sufficiently dissimilar from each other) for a suitable notion of distance/dissimilarity between solutions. Interpreting assignments as bit vectors, we take their Hamming distance to quantify dissimilarity, and we focus on the problem of finding two solutions. Specifically, we define the problem Max Differ SAT (resp. Exact Differ SAT) as follows: Given a Boolean formula ϕ on n variables, decide whether ϕ has two satisfying assignments that differ on at least (resp. exactly) d variables. We study the classical and parameterized (in parameters d and n-d) complexities of Max Differ SAT and Exact Differ SAT, when restricted to some classes of formulas on which SAT is known to be polynomial-time solvable. In particular, we consider affine formulas, Krom formulas (i.e., 2-CNF formulas) and hitting formulas.
For affine formulas, we show the following: Both problems are polynomial-time solvable when each equation has at most two variables. Exact Differ SAT is NP-hard, even when each equation has at most three variables and each variable appears in at most four equations. Also, Max Differ SAT is NP-hard, even when each equation has at most four variables. Both problems are 𝖶[1]-hard in the parameter n-d. In contrast, when parameterized by d, Exact Differ SAT is 𝖶[1]-hard, but Max Differ SAT admits a single-exponential FPT algorithm and a polynomial-kernel. For Krom formulas, we show the following: Both problems are polynomial-time solvable when each variable appears in at most two clauses. Also, both problems are 𝖶[1]-hard in the parameter d (and therefore, it turns out, also NP-hard), even on monotone inputs (i.e., formulas with no negative literals). Finally, for hitting formulas, we show that both problems can be solved in polynomial-time.

Subject Classification

ACM Subject Classification
  • Theory of computation → Design and analysis of algorithms
Keywords
  • Diverse solutions
  • Affine formulas
  • 2-CNF formulas
  • Hitting formulas

Metrics

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

References

  1. Ola Angelsmark and Johan Thapper. Algorithms for the maximum Hamming distance problem. In International Workshop on Constraint Solving and Constraint Logic Programming, pages 128-141. Springer, 2004. URL: https://doi.org/10.1007/11402763_10.
  2. Bengt Aspvall, Michael F Plass, and Robert Endre Tarjan. A linear-time algorithm for testing the truth of certain quantified boolean formulas. Information processing letters, 8(3):121-123, 1979. URL: https://doi.org/10.1016/0020-0190(79)90002-4.
  3. Julien Baste, Michael R Fellows, Lars Jaffke, Tomáš Masařík, Mateus de Oliveira Oliveira, Geevarghese Philip, and Frances A Rosamond. Diversity of solutions: An exploration through the lens of fixed-parameter tractability theory. Artificial Intelligence, 303:103644, 2022. URL: https://doi.org/10.1016/j.artint.2021.103644.
  4. Julien Baste, Lars Jaffke, Tomáš Masaří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.
  5. Endre Boros, Yves Crama, and Peter L Hammer. Polynomial-time inference of all valid implications for horn and related formulae. Annals of Mathematics and Artificial Intelligence, 1:21-32, 1990. URL: https://doi.org/10.1007/BF01531068.
  6. Endre Boros, Peter L Hammer, and Xiaorong Sun. Recognition of q-Horn formulae in linear time. Discrete Applied Mathematics, 55(1):1-13, 1994. URL: https://doi.org/10.1016/0166-218X(94)90033-7.
  7. Michele Conforti, Gérard Cornuéjols, Ajai Kapoor, Kristina Vuškovic, and MR Rao. Balanced matrices. Mathematical Programming: State of the Art, pages 1-33, 1994. Google Scholar
  8. Stephen A Cook. The complexity of theorem-proving procedures. In Logic, Automata, and Computational Complexity: The Works of Stephen A. Cook, pages 143-152. Association for Computing Machinery, 2023. URL: https://doi.org/10.1145/3588287.3588297.
  9. Marek Cygan, Fedor V Fomin, Łukasz Kowalik, Daniel Lokshtanov, Dániel Marx, Marcin Pilipczuk, Michał Pilipczuk, and Saket Saurabh. Parameterized algorithms, volume 5. Springer, 2015. URL: https://doi.org/10.1007/978-3-319-21275-3.
  10. Vilhelm Dahllöf. Algorithms for max Hamming exact satisfiability. In Proceedings of the 16th International Symposium on Algorithms and Computation (ISAAC), pages 829-838. Springer, 2005. URL: https://doi.org/10.1007/11602613_83.
  11. Mark de Berg, Andrés López Martínez, and Frits C. R. Spieksma. Finding diverse minimum s-t cuts. In Proceedings of the 34th International Symposium on Algorithms and Computation ISAAC, volume 283 of LIPIcs, pages 24:1-24:17, 2023. URL: https://doi.org/10.4230/LIPIcs.ISAAC.2023.24.
  12. William F Dowling and Jean H Gallier. Linear-time algorithms for testing the satisfiability of propositional Horn formulae. The Journal of Logic Programming, 1(3):267-284, 1984. URL: https://doi.org/10.1016/0743-1066(84)90014-1.
  13. Rod G Downey, Michael R Fellows, Alexander Vardy, and Geoff Whittle. The parametrized complexity of some fundamental problems in coding theory. SIAM Journal on Computing, 29(2):545-570, 1999. URL: https://doi.org/10.1137/S0097539797323571.
  14. Rodney G Downey and Michael R Fellows. Fixed-parameter intractability. In 1992 Seventh Annual Structure in Complexity Theory Conference, pages 36-37. IEEE Computer Society, 1992. Google Scholar
  15. Rodney G Downey, Michael R Fellows, et al. Fundamentals of Parameterized Complexity, volume 4. Springer, 2013. Google Scholar
  16. S. Even, A. Shamir, and A. Itai. On the complexity of time table and multi-commodity flow problems. In Proceedings of the 16th Annual Symposium on Foundations of Computer Science (SFCS), pages 184-193. IEEE Computer Society, 1975. URL: https://doi.org/10.1109/SFCS.1975.21.
  17. Fedor V Fomin, Petr A Golovach, Lars Jaffke, Geevarghese Philip, and Danil Sagunov. Diverse pairs of matchings. In 31st International Symposium on Algorithms and Computation (ISAAC 2020). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2020. Google Scholar
  18. Fedor V Fomin, Petr A Golovach, Fahad Panolan, Geevarghese Philip, and Saket Saurabh. Diverse collections in matroids and graphs. Mathematical Programming, pages 1-33, 2023. Google Scholar
  19. John Franco and Allen Van Gelder. A perspective on certain polynomial-time solvable classes of satisfiability. Discrete Applied Mathematics, 125(2-3):177-214, 2003. URL: https://doi.org/10.1016/S0166-218X(01)00358-4.
  20. Aadityan Ganesh, HV Vishwa Prakash, Prajakta Nimbhorkar, and Geevarghese Philip. Disjoint stable matchings in linear time. In Proceedings of the 47th International Workshop on Graph-Theoretic Concepts in Computer Science (WG), pages 94-105. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-86838-3_7.
  21. Joseph F Grcar. How ordinary elimination became Gaussian elimination. Historia Mathematica, 38(2):163-218, 2011. Google Scholar
  22. Tesshu Hanaka, Yasuaki Kobayashi, Kazuhiro Kurita, and Yota Otachi. Finding diverse trees, paths, and more. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 35, pages 3778-3786, 2021. URL: https://doi.org/10.1609/aaai.v35i5.16495.
  23. Gordon Hoi, Sanjay Jain, and Frank Stephan. A fast exponential time algorithm for max hamming distance x3sat. arXiv preprint, 2019. URL: https://arxiv.org/abs/1910.01293.
  24. Gordon Hoi and Frank Stephan. Measure and conquer for max Hamming distance XSAT. In 30th International Symposium on Algorithms and Computation (ISAAC 2019). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. Google Scholar
  25. Russell Impagliazzo and Ramamohan Paturi. On the complexity of k-sat. Journal of Computer and System Sciences (JCSS), 62(2):367-375, 2001. URL: https://doi.org/10.1006/jcss.2000.1727.
  26. Kazuo Iwama. CNF-satisfiability test by counting and polynomial average time. SIAM Journal on Computing, 18(2):385-391, 1989. URL: https://doi.org/10.1137/0218026.
  27. Richard M Karp. Reducibility among combinatorial problems. Springer, 2010. URL: https://doi.org/10.1007/978-3-540-68279-0_8.
  28. Konstantinos Koiliaris and Chao Xu. Faster pseudopolynomial time algorithms for subset sum. ACM Transactions on Algorithms (TALG), 15(3):1-20, 2019. URL: https://doi.org/10.1145/3329863.
  29. Melven R Krom. The decision problem for a class of first-order formulas in which all disjunctions are binary. Mathematical Logic Quarterly, 13(1-2):15-20, 1967. Google Scholar
  30. Leonid Anatolevich Levin. Universal sequential search problems. Problemy peredachi informatsii, 9(3):115-116, 1973. Google Scholar
  31. Harry R Lewis. Renaming a set of clauses as a Horn set. Journal of the ACM (JACM), 25(1):134-135, 1978. URL: https://doi.org/10.1145/322047.322059.
  32. Ilya Mironov and Lintao Zhang. Applications of sat solvers to cryptanalysis of hash functions. In Proceedings of the 9th International Conference on Theory and Applications of Satisfiability Testing (SAT), pages 102-115. Springer, 2006. URL: https://doi.org/10.1007/11814948_13.
  33. Neeldhara Misra, Harshil Mittal, and Saraswati Nanoti. Diverse non crossing matchings. In CCCG, pages 249-256, 2022. Google Scholar
  34. Bojan Mohar. Face covers and the genus problem for apex graphs. Journal of Combinatorial Theory (JCT), Series B, 82(1):102-117, 2001. URL: https://doi.org/10.1006/jctb.2000.2026.
  35. Thomas J Schaefer. The complexity of satisfiability problems. In Proceedings of the tenth annual ACM Symposium on Theory of Computing, pages 216-226, 1978. URL: https://doi.org/10.1145/800133.804350.
  36. Maria Grazia Scutella. A note on Dowling and Gallier’s top-down algorithm for propositional horn satisfiability. The Journal of Logic Programming, 8(3):265-273, 1990. URL: https://doi.org/10.1016/0743-1066(90)90026-2.
  37. Yakir Vizel, Georg Weissenbacher, and Sharad Malik. Boolean satisfiability solvers and their applications in model checking. Proceedings of the IEEE, 103(11):2021-2035, 2015. URL: https://doi.org/10.1109/JPROC.2015.2455034.
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 About DROPS Imprint Privacy Contact