Phase Transition in Matched Formulas and a Heuristic for Biclique Satisfiability

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


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.


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


  1. 1.
    Metacentrum grid computing, June 2017.
  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). Scholar
  3. 3.
    Audemard, G., Simon, L.: The glucose sat solver, June 2017.
  4. 4.
    Bollobás, B.: Modern Graph Theory. GTM, vol. 184. Springer, New York (1998). 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).
  6. 6.
    Chromý, M., Kučera, P.: Phase transition in matched formulas and a heuristic for biclique satisfiability. ArXiv e-prints, August 2018.
  7. 7.
    Connamacher, H.S., Molloy, M.: The satisfiability threshold for a seemingly intractable random constraint satisfaction problem. CoRR abs/1202.0042 (2012). 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).
  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).
  10. 10.
    Eén, N., Sörensson, N.: The minisat, June 2017.
  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). 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.
  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). Scholar
  18. 18.
    Tovey, C.A.: A simplified NP-complete satisfiability problem. Discrete Appl. Math. 8(1), 85–89 (1984). 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