Fix condition CNF explosion by using flat symbols for condition names

When conditions reference other conditions via !Condition, the CNF
expression was recursively expanded into the full boolean tree. For
templates with many conditions (e.g., 5 groups of 10 Fn::Equals each
plus a DeployLambdas = Not(Or(G1..G5))), this created massive
expressions where sympy's CNF conversion (_or()) exploded
exponentially.

Fix: Give each condition name its own Symbol and express relationships
as implication constraints added once to the EncodedCNF. Nested
!Condition references now resolve to the simple Symbol instead of
expanding the full expression. The SAT solver handles implications
through the constraints.

Both the template-level (conditions/conditions.py) and context-level
(context/conditions/_conditions.py) classes are updated.

Performance on reproduction template: 20+ seconds -> 0.33 seconds.

Fixes #4406

Author: kddejong

src/cfnlint/conditions/_condition.py

@@ -233,7 +233,14 @@ def build_true_cnf(self, params: dict[str, Symbol]) -> Any:
         Returns:
             Any: A SymPy CNF clause
         """
-        return self.build_cnf(params)
+        if self._name in params:
+            return params[self._name]
+        return super().build_cnf(params)
+
+    def build_cnf(self, params: dict[str, Symbol]) -> Any:
+        if self._name in params:
+            return params[self._name]
+        return super().build_cnf(params)
 
     def build_false_cnf(self, params: dict[str, Symbol]) -> Any:
         """Build a SymPy CNF for a False based scenario

src/cfnlint/conditions/conditions.py

@@ -187,6 +187,31 @@ def _build_equal_vars(c_equals: list[Equal]):
                     if prop is not None:
                         cnf.add_prop(Not(prop))
 
+        # Create a Symbol per condition name and add implication constraints
+        # so that build_true_cnf/build_false_cnf can use the simple Symbol
+        # instead of the full boolean expression (avoids CNF explosion).
+        # We add condition symbols to equal_vars FIRST so that when
+        # build_cnf is called, nested !Condition references resolve to
+        # the simple Symbol instead of expanding the full expression.
+        cond_symbols: dict[str, Symbol] = {}
+        for condition_name in condition_names:
+            cond_symbols[condition_name] = Symbol(f"__cond_{condition_name}")
+
+        # Build equivalences using cond_symbols for nested condition refs
+        # but NOT for the condition being defined (to avoid circularity)
+        for condition_name in condition_names:
+            cond_sym = cond_symbols[condition_name]
+            # Merge equal_vars with other condition symbols (excluding self)
+            build_params = dict(equal_vars)
+            for other_name, other_sym in cond_symbols.items():
+                if other_name != condition_name:
+                    build_params[other_name] = other_sym
+            cond_expr = self._conditions[condition_name].build_cnf(build_params)
+            cnf.add_prop(Implies(cond_sym, cond_expr))
+            cnf.add_prop(Implies(cond_expr, cond_sym))
+
+        equal_vars.update(cond_symbols)
+
         for rule in self._rules:
             cnf.add_prop(rule.build_cnf(equal_vars))
 

src/cfnlint/context/conditions/_condition.py

@@ -8,7 +8,7 @@
 from dataclasses import dataclass, field
 from typing import Any
 
-from sympy import And, Not, Or
+from sympy import And, Not, Or, Symbol
 from sympy.logic.boolalg import BooleanFunction
 
 from cfnlint.conditions._utils import get_hash
@@ -20,19 +20,16 @@
 class Condition:
     instance: Any = field(init=True)
     status: bool | None = field(init=True, default=None)
-    hash: str = field(init=True, default="")  # Changed to init=True with default
+    hash: str = field(init=True, default="")
 
     fn_equals: Equal | None = field(init=True, default=None)
     condition: list["Condition"] | "Condition" | None = field(init=True, default=None)
     cnf: BooleanFunction = field(init=True, default_factory=BooleanFunction)
 
-    # Removed __post_init__ since hash is now passed in
-
     @classmethod
     def create_from_instance(
         cls, instance: Any, all_conditions: dict[str, Any]
     ) -> "Condition":
-        # Calculate hash here once
         instance_hash = get_hash(instance)
 
         fn_k, fn_v = is_function(instance)
@@ -73,6 +70,7 @@ def create_from_instance(
         if fn_k == "Condition":
             if not isinstance(fn_v, str):
                 raise ValueError(f"Condition value {fn_v!r} must be a string")
+            # Build the sub-condition for is_region/equals traversal
             sub_condition = all_conditions.get(fn_v)
             try:
                 sub_all_conditions = all_conditions.copy()
@@ -82,7 +80,14 @@ def create_from_instance(
                 c = Condition.create_from_instance(
                     {"Fn::Equals": [None, None]}, all_conditions
                 )
-            return cls(instance=instance, condition=c, cnf=c.cnf, hash=instance_hash)
+            # Use a Symbol for the condition name instead of the expanded CNF
+            # The equivalence constraint is added in Conditions.create_from_instance
+            return cls(
+                instance=instance,
+                condition=c,
+                cnf=Symbol(fn_v),
+                hash=instance_hash,
+            )
 
         raise ValueError(f"Unknown key {fn_k!r} in condition")
 

src/cfnlint/context/conditions/_conditions.py

@@ -6,12 +6,11 @@
 from __future__ import annotations
 
 import itertools
-from collections import OrderedDict
 from dataclasses import dataclass, field
 from typing import TYPE_CHECKING, Any, Iterator
 
-from sympy import Not, Or
-from sympy.logic.boolalg import BooleanFunction
+from sympy import Equivalent, Not, Or, Symbol
+from sympy.assumptions.cnf import EncodedCNF
 from sympy.logic.inference import satisfiable
 
 from cfnlint.conditions._utils import get_hash
@@ -26,39 +25,21 @@
     from cfnlint.context.context import Context, Parameter
 
 
-# Use OrderedDict for LRU-like behavior
-_satisfiable_cache: OrderedDict[str, bool] = OrderedDict()
-_MAX_CACHE_SIZE = 10000  # Limit cache size to prevent memory issues
-
-
-def _get_from_satisfiable_cache(cnf_hash: str) -> bool | None:
-    """Get result from cache with LRU behavior"""
-    if cnf_hash in _satisfiable_cache:
-        # Move to end (most recently used)
-        value = _satisfiable_cache.pop(cnf_hash)
-        _satisfiable_cache[cnf_hash] = value
-        return value
-    return None
-
-
-def _add_to_satisfiable_cache(cnf_hash: str, result: bool) -> None:
-    """Add result to cache with size management"""
-    if len(_satisfiable_cache) >= _MAX_CACHE_SIZE:
-        # Remove oldest item (first in OrderedDict)
-        _satisfiable_cache.popitem(last=False)
-    _satisfiable_cache[cnf_hash] = result
-
-
 @dataclass(frozen=True)
 class Conditions:
-    # Template level condition management
     conditions: dict[str, Condition] = field(init=True, default_factory=dict)
-    cnf: BooleanFunction | None = field(init=True, default=None)
+    cnf: EncodedCNF = field(init=True, default_factory=EncodedCNF, compare=False)
+    _condition_symbols: dict[str, Symbol] = field(
+        init=True, default_factory=dict, compare=False
+    )
     _max_scenarios: int = field(init=False, default=128)
 
     @classmethod
     def create_from_instance(
-        cls, conditions: Any, rules: dict[str, dict], parameters: dict[str, "Parameter"]
+        cls,
+        conditions: Any,
+        rules: dict[str, dict],
+        parameters: dict[str, "Parameter"],
     ) -> "Conditions":
         obj: dict[str, Condition] = {}
         if not isinstance(conditions, dict):
@@ -69,13 +50,20 @@ def create_from_instance(
                 del other_conditions[k]
                 obj[k] = Condition.create_from_instance(v, other_conditions)
             except ValueError:
-                # this is a default condition so we can keep the name but it will
-                # not associate with another condition and will always be true/false
                 obj[k] = Condition.create_from_instance(
                     {"Fn::Equals": [None, None]}, conditions
                 )
 
-        cnf = None
+        # Build EncodedCNF with a Symbol per condition name
+        cnf = EncodedCNF()
+        condition_symbols: dict[str, Symbol] = {}
+        for name, cond in obj.items():
+            sym = Symbol(name)
+            condition_symbols[name] = sym
+            # Add equivalence: Symbol(name) <-> condition's boolean expression
+            cnf.add_prop(Equivalent(sym, cond.cnf))
+
+        # Add parameter AllowedValues constraints
         for p_k, p_v in parameters.items():
             if not p_v.allowed_values:
                 continue
@@ -90,21 +78,17 @@ def create_from_instance(
                         if i.left.instance in allowed_values:
                             allowed_values.remove(i.left.instance)
 
-            if not allowed_values:
-                if cnf is None:
-                    cnf = Or(*equals_cnfs)
-                else:
-                    cnf = cnf & Or(*equals_cnfs)
+            if not allowed_values and equals_cnfs:
+                cnf.add_prop(Or(*equals_cnfs))
 
-        return cls(conditions=obj, cnf=cnf)
+        return cls(conditions=obj, cnf=cnf, _condition_symbols=condition_symbols)
 
     def evolve(self, status: dict[str, bool]) -> "Conditions":
         cls = self.__class__
 
         if not status:
             return self
 
-        # Check if we're trying to set the same status
         all_same = True
         for condition, condition_status in status.items():
             if (
@@ -117,50 +101,30 @@ def evolve(self, status: dict[str, bool]) -> "Conditions":
             return self
 
         conditions: dict[str, Condition] = {}
-        cnf = self.cnf
+        cnf = self.cnf.copy()
         for condition, value in self.conditions.items():
             s = status.get(condition, value.status)
             try:
                 conditions[condition] = value.evolve(status=s)
-                if s is not None:
-                    if cnf:
-                        cnf = (
-                            cnf & conditions[condition].cnf
-                            if s
-                            else cnf & Not(conditions[condition].cnf)
-                        )
-                    else:
-                        cnf = (
-                            conditions[condition].cnf
-                            if s
-                            else Not(conditions[condition].cnf)
-                        )
+                if s is not None and condition in self._condition_symbols:
+                    sym = self._condition_symbols[condition]
+                    cnf.add_prop(sym if s else Not(sym))
             except ValueError as e:
                 raise Unsatisfiable(
                     new_status=status,
                     current_status=self.status,
                 ) from e
 
-        cnf_hash = get_hash(str(cnf))
-        cached_result = _get_from_satisfiable_cache(cnf_hash)
-        if cached_result is not None:
-            if not cached_result:
-                raise Unsatisfiable(
-                    new_status=status,
-                    current_status=self.status,
-                )
-        else:
-            is_sat = satisfiable(cnf)
-            _add_to_satisfiable_cache(cnf_hash, bool(is_sat))
-            if not is_sat:
-                raise Unsatisfiable(
-                    new_status=status,
-                    current_status=self.status,
-                )
+        if not satisfiable(cnf):
+            raise Unsatisfiable(
+                new_status=status,
+                current_status=self.status,
+            )
 
         return cls(
             conditions=conditions,
             cnf=cnf,
+            _condition_symbols=self._condition_symbols,
         )
 
     def _build_conditions(self, conditions: set[str]) -> Iterator["Conditions"]:

test/unit/module/context/conditions/test_conditions.py

@@ -6,12 +6,7 @@
 import pytest
 
 from cfnlint.context import create_context_for_template
-from cfnlint.context.conditions._conditions import (
-    _MAX_CACHE_SIZE,
-    Conditions,
-    _add_to_satisfiable_cache,
-    _satisfiable_cache,
-)
+from cfnlint.context.conditions._conditions import Conditions
 from cfnlint.context.conditions.exceptions import Unsatisfiable
 from cfnlint.template import Template
 
@@ -302,29 +297,3 @@ def test_evolve_from_instance(current_status, instance, expected):
 def test_condition_failures():
     with pytest.raises(ValueError):
         Conditions.create_from_instance([], {}, {})
-
-
-def test_add_to_satisfiable_cache():
-    """Test _add_to_satisfiable_cache function with cache size management"""
-    # Clear the cache before testing
-    _satisfiable_cache.clear()
-
-    # Add items to fill the cache
-    for i in range(_MAX_CACHE_SIZE):
-        _add_to_satisfiable_cache(f"test_key_{i}", True)
-
-    # Verify cache size
-    assert len(_satisfiable_cache) == _MAX_CACHE_SIZE
-
-    # Add one more item to trigger cache management (line 48)
-    _add_to_satisfiable_cache("overflow_key", False)
-
-    # Verify cache size remains at max
-    assert len(_satisfiable_cache) == _MAX_CACHE_SIZE
-
-    # Verify the first item was removed (oldest item)
-    assert "test_key_0" not in _satisfiable_cache
-
-    # Verify the new item was added
-    assert "overflow_key" in _satisfiable_cache
-    assert _satisfiable_cache["overflow_key"] is False