sat_search_tree_analysis.py

#!/usr/bin/env python3
"""
SAT Search Tree Analysis
========================

Looking for phi/Lucas structure in HOW solutions are found,
not just WHERE they are.

The hypothesis: The branching structure of SAT search exhibits
Fibonacci/phi patterns due to E8/H4 geometry.

Author: Anthony
Date: January 27, 2026
"""

import numpy as np
import random
import math
from collections import defaultdict

PHI = (1 + math.sqrt(5)) / 2
FIBONACCI = [1, 1, 2, 3, 5, 8, 13, 21, 34, 55, 89, 144, 233, 377, 610, 987]

def generate_random_3sat(n_vars, n_clauses):
    """Generate a random 3-SAT formula."""
    clauses = []
    for _ in range(n_clauses):
        vars_in_clause = random.sample(range(n_vars), 3)
        clause = [(v, random.choice([True, False])) for v in vars_in_clause]
        clauses.append(clause)
    return clauses

def count_satisfied(clauses, assignment):
    """Count how many clauses are satisfied."""
    count = 0
    for clause in clauses:
        for var, is_positive in clause:
            if var < len(assignment):
                val = assignment[var]
                if (is_positive and val) or (not is_positive and not val):
                    count += 1
                    break
    return count

class DPLLSolver:
    """DPLL solver that tracks search tree statistics."""
    
    def __init__(self, clauses, n_vars):
        self.clauses = clauses
        self.n_vars = n_vars
        self.nodes_visited = 0
        self.branch_counts = []  # Track branching at each depth
        self.backtrack_counts = []
        self.depth_visits = defaultdict(int)
        
    def solve(self):
        assignment = [None] * self.n_vars
        result = self._dpll(assignment, 0)
        return result
    
    def _dpll(self, assignment, depth):
        self.nodes_visited += 1
        self.depth_visits[depth] += 1
        
        # Check if all clauses satisfied
        satisfied = self._check_satisfied(assignment)
        if satisfied == True:
            return assignment.copy()
        if satisfied == False:
            return None
        
        # Find unassigned variable
        var = self._choose_variable(assignment)
        if var is None:
            return None
        
        # Track branching
        while len(self.branch_counts) <= depth:
            self.branch_counts.append(0)
            self.backtrack_counts.append(0)
        
        # Try True
        self.branch_counts[depth] += 1
        assignment[var] = True
        result = self._dpll(assignment, depth + 1)
        if result is not None:
            return result
        
        # Backtrack, try False
        self.backtrack_counts[depth] += 1
        self.branch_counts[depth] += 1
        assignment[var] = False
        result = self._dpll(assignment, depth + 1)
        if result is not None:
            return result
        
        # Backtrack completely
        assignment[var] = None
        return None
    
    def _check_satisfied(self, assignment):
        """Check if formula is satisfied/unsatisfied/undetermined."""
        all_satisfied = True
        for clause in self.clauses:
            clause_satisfied = False
            clause_determined = True
            for var, is_positive in clause:
                if assignment[var] is None:
                    clause_determined = False
                elif (is_positive and assignment[var]) or (not is_positive and not assignment[var]):
                    clause_satisfied = True
                    break
            
            if not clause_satisfied:
                if clause_determined:
                    return False  # Clause definitely unsatisfied
                all_satisfied = False
        
        return True if all_satisfied else None
    
    def _choose_variable(self, assignment):
        """Choose next variable to branch on."""
        for i, val in enumerate(assignment):
            if val is None:
                return i
        return None

def analyze_search_pattern(solver):
    """Analyze search tree for phi/Fibonacci patterns."""
    
    # Ratio of nodes at consecutive depths
    depth_ratios = []
    depths = sorted(solver.depth_visits.keys())
    for i in range(len(depths) - 1):
        d1, d2 = depths[i], depths[i+1]
        if solver.depth_visits[d2] > 0:
            ratio = solver.depth_visits[d1] / solver.depth_visits[d2]
            depth_ratios.append(ratio)
    
    # Backtrack ratios
    backtrack_ratios = []
    for i in range(len(solver.branch_counts)):
        if solver.branch_counts[i] > 0:
            ratio = solver.backtrack_counts[i] / solver.branch_counts[i]
            backtrack_ratios.append(ratio)
    
    # Check if any ratios are close to phi or 1/phi
    phi_matches = 0
    inv_phi_matches = 0
    fib_ratio_matches = 0
    
    for r in depth_ratios + backtrack_ratios:
        if r > 0:
            # Check proximity to phi
            if abs(r - PHI) / PHI < 0.1:
                phi_matches += 1
            if abs(r - 1/PHI) / (1/PHI) < 0.1:
                inv_phi_matches += 1
            # Check Fibonacci ratios
            for i in range(len(FIBONACCI) - 1):
                fib_ratio = FIBONACCI[i+1] / FIBONACCI[i]
                if abs(r - fib_ratio) / fib_ratio < 0.1:
                    fib_ratio_matches += 1
                    break
    
    total_ratios = len(depth_ratios) + len(backtrack_ratios)
    
    return {
        'nodes': solver.nodes_visited,
        'max_depth': max(solver.depth_visits.keys()) if solver.depth_visits else 0,
        'depth_ratios': depth_ratios,
        'backtrack_ratios': backtrack_ratios,
        'phi_matches': phi_matches,
        'inv_phi_matches': inv_phi_matches,
        'fib_ratio_matches': fib_ratio_matches,
        'total_ratios': total_ratios,
        'phi_fraction': phi_matches / total_ratios if total_ratios > 0 else 0
    }

def run_experiment(n_vars, clause_ratio, n_trials=100):
    """Run experiment at given parameters."""
    n_clauses = int(n_vars * clause_ratio)
    
    all_stats = []
    sat_count = 0
    
    for _ in range(n_trials):
        clauses = generate_random_3sat(n_vars, n_clauses)
        solver = DPLLSolver(clauses, n_vars)
        result = solver.solve()
        
        if result is not None:
            sat_count += 1
        
        stats = analyze_search_pattern(solver)
        stats['sat'] = result is not None
        all_stats.append(stats)
    
    return all_stats, sat_count

def main():
    print("=" * 70)
    print("SAT SEARCH TREE PHI-STRUCTURE ANALYSIS")
    print("Looking for golden ratio patterns in DPLL search")
    print("=" * 70)
    print()
    
    n_vars = 20
    n_trials = 100
    ratios = [3.5, 4.0, 4.267, 4.5, 5.0]
    
    print(f"Variables: {n_vars}")
    print(f"Trials per ratio: {n_trials}")
    print(f"phi = {PHI:.6f}")
    print(f"1/phi = {1/PHI:.6f}")
    print()
    
    results = {}
    
    for ratio in ratios:
        print(f"\nRunning ratio {ratio}...", end=" ", flush=True)
        stats, sat_count = run_experiment(n_vars, ratio, n_trials)
        results[ratio] = stats
        
        # Aggregate statistics
        avg_nodes = np.mean([s['nodes'] for s in stats])
        avg_depth = np.mean([s['max_depth'] for s in stats])
        avg_phi_frac = np.mean([s['phi_fraction'] for s in stats])
        
        # Collect all depth ratios
        all_depth_ratios = []
        for s in stats:
            all_depth_ratios.extend(s['depth_ratios'])
        
        # Check how many are close to phi
        near_phi = sum(1 for r in all_depth_ratios if abs(r - PHI) < 0.2) if all_depth_ratios else 0
        near_inv_phi = sum(1 for r in all_depth_ratios if abs(r - 1/PHI) < 0.2) if all_depth_ratios else 0
        
        print(f"SAT: {sat_count}%, Nodes: {avg_nodes:.0f}, Depth: {avg_depth:.1f}")
        print(f"         Depth ratios near phi: {near_phi}/{len(all_depth_ratios)}")
        print(f"         Depth ratios near 1/phi: {near_inv_phi}/{len(all_depth_ratios)}")
    
    # Detailed analysis at phase transition
    print()
    print("=" * 70)
    print("DETAILED ANALYSIS AT PHASE TRANSITION (ratio = 4.267)")
    print("=" * 70)
    
    if 4.267 in results:
        stats = results[4.267]
        all_ratios = []
        for s in stats:
            all_ratios.extend(s['depth_ratios'])
        
        if all_ratios:
            print(f"\nDepth ratio statistics:")
            print(f"  Mean: {np.mean(all_ratios):.4f}")
            print(f"  Std:  {np.std(all_ratios):.4f}")
            print(f"  phi = {PHI:.4f}")
            print(f"  1/phi = {1/PHI:.4f}")
            
            # Distance from phi
            dist_from_phi = [abs(r - PHI) for r in all_ratios]
            dist_from_inv_phi = [abs(r - 1/PHI) for r in all_ratios]
            dist_from_2 = [abs(r - 2) for r in all_ratios]
            
            print(f"\n  Mean distance from phi: {np.mean(dist_from_phi):.4f}")
            print(f"  Mean distance from 1/phi: {np.mean(dist_from_inv_phi):.4f}")
            print(f"  Mean distance from 2: {np.mean(dist_from_2):.4f}")
            
            # Which is closest?
            if np.mean(dist_from_phi) < np.mean(dist_from_2):
                print("\n  >>> Ratios closer to phi than to 2!")
            if np.mean(dist_from_inv_phi) < min(np.mean(dist_from_phi), np.mean(dist_from_2)):
                print("  >>> Ratios closest to 1/phi!")
    
    # Nodes vs depth scaling
    print()
    print("=" * 70)
    print("SEARCH COMPLEXITY SCALING")
    print("=" * 70)
    
    for ratio in ratios:
        stats = results[ratio]
        nodes = [s['nodes'] for s in stats]
        depths = [s['max_depth'] for s in stats]
        
        # Fit: nodes ~ base^depth
        # log(nodes) ~ depth * log(base)
        valid_pairs = [(d, n) for d, n in zip(depths, nodes) if d > 0 and n > 0]
        if len(valid_pairs) > 10:
            ds, ns = zip(*valid_pairs)
            log_ns = np.log(ns)
            # Linear regression
            slope, intercept = np.polyfit(ds, log_ns, 1)
            base = np.exp(slope)
            
            print(f"\nRatio {ratio}:")
            print(f"  Nodes ~ {base:.4f}^depth")
            print(f"  phi = {PHI:.4f}, 2 = 2.0000")
            
            if abs(base - PHI) < abs(base - 2):
                print(f"  >>> Base closer to phi than to 2!")
            
            # Check specific values
            if abs(base - PHI) < 0.15:
                print(f"  *** POTENTIAL PHI SCALING DETECTED ***")

if __name__ == "__main__":
    main()