fix overhead formulas per Codex review

- sat_circuitsat: account for extra assignments/variables from unused SAT vars
- sat_coloring: OR-gadget adds 11 edges (not 10), plus base triangle constant
- circuit_spinglass: 4× spin and 6× interaction multipliers for gate arity

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: isPANN

src/rules/circuit_spinglass.rs

@@ -414,8 +414,8 @@ where
 
 #[reduction(
     overhead = {
-        num_spins = "num_assignments * num_variables",
-        num_interactions = "num_assignments * num_variables",
+        num_spins = "4 * num_assignments * num_variables",
+        num_interactions = "6 * num_assignments * num_variables",
     }
 )]
 impl ReduceTo<SpinGlass<SimpleGraph, i32>> for CircuitSAT {

src/rules/sat_circuitsat.rs

@@ -36,8 +36,8 @@ impl ReductionResult for ReductionSATToCircuit {
 
 #[reduction(
     overhead = {
-        num_variables = "num_vars + num_clauses + 1",
-        num_assignments = "num_clauses + 2",
+        num_variables = "2 * num_vars + num_clauses + 1",
+        num_assignments = "num_vars + num_clauses + 2",
     }
 )]
 impl ReduceTo<CircuitSAT> for Satisfiability {

src/rules/sat_coloring.rs

@@ -296,8 +296,8 @@ impl ReductionSATToColoring {
 
 #[reduction(
     overhead = {
-        num_vertices = "2 * num_vars + 5 * num_literals",
-        num_edges = "3 * num_vars + 10 * num_literals",
+        num_vertices = "2 * num_vars + 5 * num_literals + 3",
+        num_edges = "3 * num_vars + 11 * num_literals + 3",
     }
 )]
 impl ReduceTo<KColoring<K3, SimpleGraph>> for Satisfiability {