Advertisement

Phase Transition in Matched Formulas and a Heuristic for Biclique Satisfiability

  • Miloš Chromý
  • Petr Kučera
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11376)

Abstract

A matched formula is a CNF formula whose incidence graph admits a matching which matches a distinct variable to every clause. We study phase transition in a context of matched formulas and their generalization of biclique satisfiable formulas. We have performed experiments to find a phase transition of property “being matched” with respect to the ratio \(m/n\) where \(m\) is the number of clauses and \(n\) is the number of variables of the input formula \(\varphi \). We compare the results of experiments to a theoretical lower bound which was shown by Franco and Van Gelder [11]. Any matched formula is satisfiable, and it remains satisfiable even if we change polarities of any literal occurrences. Szeider [17] generalized matched formulas into two classes having the same property—var-satisfiable and biclique satisfiable formulas. A formula is biclique satisfiable if its incidence graph admits covering by pairwise disjoint bounded bicliques. Recognizing if a formula is biclique satisfiable is NP-complete. In this paper we describe a heuristic algorithm for recognizing whether a formula is biclique satisfiable and we evaluate it by experiments on random formulas. We also describe an encoding of the problem of checking whether a formula is biclique satisfiable into SAT and we use it to evaluate the performance of our heuristic.

Keywords

SAT Matched formulas Biclique SAT var-SAT Phase transition Biclique cover 

References

  1. 1.
    Metacentrum grid computing, June 2017. https://metavo.metacentrum.cz/en/
  2. 2.
    Aharoni, R., Linial, N.: Minimal non-two-colorable hypergraphs and minimal unsatisfiable formulas. J. Comb. Theory Ser. A 43(2), 196–204 (1986).  https://doi.org/10.1016/0097-3165(86)90060-9. http://www.sciencedirect.com/science/article/pii/0097316586900609MathSciNetCrossRefzbMATHGoogle Scholar
  3. 3.
    Audemard, G., Simon, L.: The glucose sat solver, June 2017. http://www.labri.fr/perso/lsimon/glucose/
  4. 4.
    Bollobás, B.: Modern Graph Theory. GTM, vol. 184. Springer, New York (1998).  https://doi.org/10.1007/978-1-4612-0619-4CrossRefzbMATHGoogle Scholar
  5. 5.
    Cheeseman, P., Kanefsky, B., Taylor, W.M.: Where the really hard problems are. In: Proceedings of the 12th International Joint Conference on Artificial Intelligence, IJCAI 1991, vol. 1, pp. 331–337. Morgan Kaufmann Publishers Inc., San Francisco (1991). http://dl.acm.org/citation.cfm?id=1631171.1631221
  6. 6.
    Chromý, M., Kučera, P.: Phase transition in matched formulas and a heuristic for biclique satisfiability. ArXiv e-prints, August 2018. https://arxiv.org/abs/1808.01774
  7. 7.
    Connamacher, H.S., Molloy, M.: The satisfiability threshold for a seemingly intractable random constraint satisfaction problem. CoRR abs/1202.0042 (2012). http://arxiv.org/abs/1202.0042MathSciNetCrossRefGoogle Scholar
  8. 8.
    Cook, S.A.: The complexity of theorem-proving procedures. In: Proceedings of the Third Annual ACM Symposium on Theory of Computing, STOC 1971, pp. 151–158. ACM, New York (1971).  https://doi.org/10.1145/800157.805047
  9. 9.
    Dubois, O., Boufkhad, Y., Mandler, J.: Typical random 3-SAT formulae and the satisfiability threshold. In: Proceedings of the Eleventh Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2000, pp. 126–127. Society for Industrial and Applied Mathematics, Philadelphia (2000). http://dl.acm.org/citation.cfm?id=338219.338243
  10. 10.
    Eén, N., Sörensson, N.: The minisat, June 2017. http://minisat.se/
  11. 11.
    Franco, J., Van Gelder, A.: A perspective on certain polynomial-time solvable classes of satisfiability. Discrete Appl. Math. 125(2–3), 177–214 (2003).  https://doi.org/10.1016/S0166-218X(01)00358-4. http://www.sciencedirect.com/science/article/pii/S0166218X01003584MathSciNetCrossRefzbMATHGoogle Scholar
  12. 12.
    Gent, I.P., Walsh, T.: The SAT phase transition. In: Proceedings of the 11th European Conference on Artificial Intelligence, pp. 105–109. Wiley (1994)Google Scholar
  13. 13.
    Heydari, M.H., Morales, L., Shields Jr., C.O., Sudborough, I.H.: Computing cross associations for attack graphs and other applications. In: 2007 40th Annual Hawaii International Conference on System Sciences, HICSS 2007, p. 270b, January 2007.  https://doi.org/10.1109/HICSS.2007.141
  14. 14.
    Hopcroft, J.E., Karp, R.M.: An \(n^{5/2}\) algorithm for maximum matchings in bipartite graphs. SIAM J. Comput. 2(4), 225–231 (1973)MathSciNetCrossRefGoogle Scholar
  15. 15.
    Lovász, L., Plummer, M.D.: Matching Theory. North-Holland, Amsterdam (1986)zbMATHGoogle Scholar
  16. 16.
    Mitchell, D., Selman, B., Levesque, H.: Hard and easy distributions of SAT problems. In: Proceedings of the 10th National Conference on Artificial Intelligence (AAAI 1992), San Jose, CA, USA, pp. 459–465 (1992)Google Scholar
  17. 17.
    Szeider, S.: Generalizations of matched CNF formulas. Ann. Math. Artif. Intell. 43(1), 223–238 (2005).  https://doi.org/10.1007/s10472-005-0432-6MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Tovey, C.A.: A simplified NP-complete satisfiability problem. Discrete Appl. Math. 8(1), 85–89 (1984).  https://doi.org/10.1016/0166-218X(84)90081-7. http://www.sciencedirect.com/science/article/pii/0166218X84900817MathSciNetCrossRefzbMATHGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Faculty of Mathematics and Physics, Department of Theoretical Computer Science and Mathematical LogicCharles UniversityPraha 1Czech Republic

Personalised recommendations