Circuit-SAT Solution-Space Geometry

Code and data for: "A Complete Computational Survey of Solution-Space Geometry in Circuit-SAT for 4-Input Boolean Functions"

Overview

This repository contains the complete computational pipeline for surveying the solution-space geometry of circuit-SAT instances across all 222 NPN-equivalence classes of 4-input Boolean functions over basis B₂. The pipeline enumerates structurally distinct circuits, computes persistent homology on Hamming-distance point clouds, and explores reconfiguration graphs via BFS.

Repository Structure

├── README.md
├── LICENSE
├── requirements.txt
├── .gitignore
├── configs/                # Pipeline configuration
├── src/                    # Computational pipeline (Phases 1-10) + figure generation
├── data/                   # Pre-computed results (JSON)
└── figures/                # Generated figures (after running scripts)

Quick Start

pip install -r requirements.txt

Generate figures from pre-computed data

python src/generate_fig_scatter.py        # H0 max-persistence vs C(f)
python src/generate_fig_connectivity.py   # Connectivity transition + confound analysis

Run the full pipeline from scratch

The pipeline consists of 10 phases, each reading the output of previous phases:

python src/phase1_circuit_sizes.py      # Determine C(f) for all 222 NPN4 classes
python src/phase2_sample_solutions.py   # Enumerate circuits via blocking clauses
python src/phase3_persistent_homology.py # Compute H0/H1/H2 persistence
python src/phase4_analysis.py           # Correlations and predictive modeling
python src/phase5_figures.py            # Publication figures
python src/phase6_robustness.py         # 7 encoding variants + 2 null models
python src/phase7_reachability.py       # BFS on reconfiguration graph (25 functions)
python src/phase7b_complete_bfs.py      # BFS for all 222 classes
python src/phase8_formal_metrics.py     # Formal metric definitions (F, H, kappa)
python src/phase9_scaling_laws.py       # Scaling law fits

Phase 10 (phase10_n5_verify.py) requires external NPN5 classification data; see comments in the script.

Total computation time: ~3.3 hours on a single Intel i7-12700K.

Pre-computed Data

All JSON files in data/ are the actual outputs used in the paper. Key files:

File	Description
`npn4_circuit_sizes.json`	Minimum circuit sizes for all 222 NPN4 classes
`tda_features.json`	TDA features for 657 instances with ≥3 solutions
`solutions_meta.json`	Metadata for all 665 instance-size pairs
`reachability/summary.json`	BFS results for 25 functions at C ∈ {2, 5, 7}
`reachability/summary_complete.json`	BFS results for all 222 classes
`robustness/summary.json`	Robustness analysis across encoding variants

Solution matrices (.npy) and persistence diagrams are not included due to size but are regenerated by Phases 2-3.

Dependencies

SAT solving: PySAT (Glucose 4)
Persistent homology: Ripser
Numerical: NumPy, SciPy, scikit-learn, Matplotlib

Configuration

configs/default.json contains pipeline parameters:

n: Number of input variables (4)
max_circuit_size: Maximum gates to search (12)
max_solutions_per_instance: Solution enumeration cap (1000)
tda_subsample: Max solutions for TDA computation (300)
max_homology_dim: Maximum homology dimension (2)
circuit_size_range_above_min: Slack levels tested (2, i.e., δ ∈ {0, 1, 2})
random_seed: Reproducibility seed (42)

Citation

@misc{li2026circuitsat,
  author       = {Li, Alex Chengyu},
  title        = {A Complete Computational Survey of Solution-Space Geometry
                  in Circuit-SAT for 4-Input Boolean Functions},
  year         = {2026},
  doi          = {10.5281/zenodo.19132019},
  publisher    = {Zenodo},
}

License

MIT License. See LICENSE.

crabsatellite/circuit-sat-geometry