An Improved Generator for 3-CNF Formulas

摘要

We consider the satisfiability problem (SAT) for Boolean formulas given in conjunctive normal form with the restriction that each clause contains three literals (3-CNF). Generation of random formulas with a fixed clause length is widely used in empirical studies. An interesting phenomenon of this method is the repeatedly confirmed linear dependence of the number of clauses in the formula on the number of Boolean variables at the point of the "phase transition" from satisfiable to unsatisfiable formulas (when the fraction of unsatisfiable formulas becomes prevailing). We propose and study a method for generating random formulas that has a smaller coefficient (3.49) of proportionality between the number of clauses and the number of variables at the point of the "phase transition" (for the previously known generation method this coefficient is 4.23).