from dataclasses import dataclass
from typing import Set, FrozenSet, List, Dict, Optional


@dataclass(frozen=True)
class Rule:
    name: str
    conditions: FrozenSet[str]
    conclusion: str
    certainty: float = 1.0


def forward_chain(facts: Set[str], rules: List[Rule]) -> Dict[str, float]:
    """Fire every applicable rule until no new facts are derived.

    Returns a dict mapping every derived fact to its certainty factor.
    """
    certainty: Dict[str, float] = {f: 1.0 for f in facts}
    changed = True
    while changed:
        changed = False
        for rule in rules:
            if not rule.conditions.issubset(certainty.keys()):
                continue
            min_cf = min(certainty[c] for c in rule.conditions)
            new_cf = min_cf * rule.certainty
            if rule.conclusion not in certainty:
                certainty[rule.conclusion] = new_cf
                changed = True
            else:
                old = certainty[rule.conclusion]
                combined = old + new_cf * (1 - old)
                if combined > old + 1e-9:
                    certainty[rule.conclusion] = combined
                    changed = True
    return certainty


def backward_chain(
    goal: str, facts: Set[str], rules: List[Rule],
    trace: Optional[List[str]] = None,
) -> Optional[float]:
    """Recursively prove `goal`, returning its certainty or None."""
    if trace is None:
        trace = []
    if goal in facts:
        return 1.0

    best_cf = None
    for rule in rules:
        if rule.conclusion != goal:
            continue
        trace.append(f"Trying {rule.name} to prove {goal}")
        sub_cfs = []
        for cond in rule.conditions:
            cf = backward_chain(cond, facts, rules, trace)
            if cf is None:
                sub_cfs = None
                break
            sub_cfs.append(cf)
        if sub_cfs is None:
            continue
        cf = min(sub_cfs) * rule.certainty if sub_cfs else rule.certainty
        if best_cf is None or cf > best_cf:
            best_cf = cf
    return best_cf
