Phase Transition in Matched Formulas and a Heuristic for Biclique Satisfiability

TL;DR

This paper investigates phase transitions in matched formulas, introduces a heuristic for recognizing biclique satisfiable formulas, and evaluates its effectiveness through experiments and SAT encoding.

Contribution

It presents a heuristic algorithm for identifying biclique satisfiable formulas and compares its performance with SAT-based methods, advancing understanding of formula satisfiability.

Findings

Phase transition observed in the property of being matched.

Heuristic algorithm shows promising results on random formulas.

SAT encoding used for performance evaluation.

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 Gelder (2003). Any matched formula is satisfiable, moreover, it remains satisfiable even if we change polarities of any literal occurrences. Szeider (2005) 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