2018/08/06 by Miloš Chromý, Chromý, Miloš, Petr Kučera +1
Computer Science · #Constraint Satisfaction and Optimization #Data Structures and Algorithms (cs.DS) #F.2.2 #FOS: Computer and information sciences #Formal Methods in Verification #Logic, Reasoning, and Knowledge #Natural Language Processing Techniques #semigroups and automata theory
paper · pdf · doi:10.48550/arxiv.1808.01774
openalex publication_date 2018/08/06 · openalex created_date 2022/08/04 · openalex updated_date 2026/07/28
A matched formula is a CNF formula whose incidence graph admits a matching\nwhich matches a distinct variable to every clause. We study phase transition in\na context of matched formulas and their generalization of biclique satisfiable\nformulas. We have performed experiments to find a phase transition of property\n"being matched" with respect to the ratio m/n where m is the number of\nclauses and n is the number of variables of the input formula \φ. We\ncompare the results of experiments to a theoretical lower bound which was shown\nby Franco and Gelder (2003). Any matched formula is satisfiable, moreover, it\nremains satisfiable even if we change polarities of any literal occurrences.\nSzeider (2005) generalized matched formulas into two classes having the same\nproperty -- var-satisfiable and biclique satisfiable formulas. A formula is\nbiclique satisfiable if its incidence graph admits covering by pairwise\ndisjoint bounded bicliques. Recognizing if a formula is biclique satisfiable is\nNP-complete. In this paper we describe a heuristic algorithm for recognizing\nwhether a formula is biclique satisfiable and we evaluate it by experiments on\nrandom formulas. We also describe an encoding of the problem of checking\nwhether a formula is biclique satisfiable into SAT and we use it to evaluate\nthe performance of our heuristic\n