Skip to main content
eScholarship
Open Access Publications from the University of California

Combinatorial Theory

Combinatorial Theory banner

Exact enumeration of satisfiable 2-SAT formulae

Published Web Location

https://doi.org/10.5070/C63261985Creative Commons 'BY' version 4.0 license
Abstract

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.

Mathematics Subject Classifications: 05A15, 68Q87, 68R95

Keywords: 2-CNF, exact enumeration, random graphs, phase transitions, strongly connected components, satisfiability, generating functions

Main Content
For improved accessibility of PDF content, download the file to your device.
Current View