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 ϕ. 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.
CITATION STYLE
Chromý, M., & Kučera, P. (2019). Phase transition in matched formulas and a heuristic for biclique satisfiability. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11376 LNCS, pp. 108–121). Springer Verlag. https://doi.org/10.1007/978-3-030-10801-4_10
Mendeley helps you to discover research relevant for your work.