DCI: A Compact Representation of 2 SAT Solution Spaces

This preprint presents the Decomposition and Conditional Implication (DCI) framework, a compact representation of the complete set of satisfying assignments of a 2-CNF formula. The formula is split into a Static Core, the variables forced to the same value in every solution, and a Dynamic Dependency Core, the condensation of the implication graph of the remaining formula. The representation has size O(n+m). The paper proves that it describes the solution space exactly, that any sequence of free choices can be propagated without conflict or backtracking, that every solution is reachable, and that all solutions can be enumerated with O(n+m) delay. It also gives a corrected complexity analysis. Deciding satisfiability and producing one solution takes linear time. Extracting the forced variables takes O(n(n+m)), and a linear-time algorithm would imply Boolean matrix multiplication in quadratic time. Counting solutions from the representation is #P-hard. The method builds on the Aspvall–Plass–Tarjan implication-graph approach to 2-SAT. Practical uses include: (1) artificial intelligence, where binary constraints appear in planning, scheduling and constraint-satisfaction problems and a compact map of forced and free choices lets a solver explore alternatives without re-solving; (2) AI-assisted configuration and explainability, where "which options are locked and which are still open" can be read directly from the representation; and (3) cybersecurity, where access-control and firewall rules, security-policy consistency and feature-dependency checks are often binary implications ("if A is allowed, B must be denied"), so forced and conflicting settings can be found and all consistent policy configurations enumerated. This is a working draft: the proofs are complete and were checked against brute-force enumeration by computer, but they have not yet been independently refereed, and some questions (listed in Section 10) remain open.