We obtain exact expressions counting the satisfiable 2-SAT formulae and describe the structure of associated implication digraphs. Our approach is based on generating function manipulations. To reflect the combinatorial specificities of the implication digraphs, we introduce a new kind of generating function, the Implication generating function, inspired by the Graphic generating function used in digraph enumeration. Using the underlying recurrences, we make accurate numerical predictions of the phase transition curve of the 2-SAT problem inside the critical window. We expect these exact formulae to be amenable to rigorous asymptotic analysis using complex analytic tools, leading to a more detailed picture of the 2-SAT phase transition in the future.

翻译：我们获得了精确的表达方式, 计算了可参数 2 - SAT 公式, 并描述了相关隐含语法的结构。 我们的方法是以生成功能操控为基础。 为了反映这些隐含语法的组合特性, 我们引入了一种新的生成功能, 即由绘图查点中使用的图形生成函数所启发的生成功能。 我们使用潜在的重现, 对关键窗口中2 - SAT 问题的阶段过渡曲线做出准确的数字预测。 我们期望这些精确的公式能够使用复杂的分析工具进行严格的无药可治分析, 从而在未来更详细地描述二 - SAT 阶段的过渡。