fix: close completeness gaps from review-implementation audit (#88)

docs/paper/reductions.typ

@@ -45,6 +45,10 @@
   "Factoring": [Factoring],
   "KingsSubgraph": [King's Subgraph MIS],
   "TriangularSubgraph": [Triangular Subgraph MIS],
+  "MaximalIS": [Maximal Independent Set],
+  "BMF": [Boolean Matrix Factorization],
+  "PaintShop": [Paint Shop],
+  "BicliqueCover": [Biclique Cover],
 )
 
 // Definition label: "def:<ProblemName>" — each definition block must have a matching label
@@ -335,6 +339,10 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V|
   Given $G = (V, E)$, find $K subset.eq V$ maximizing $|K|$ such that all pairs in $K$ are adjacent: $forall u, v in K: (u, v) in E$. Equivalent to MIS on the complement graph $overline(G)$.
 ]
 
+#problem-def("MaximalIS")[
+  Given $G = (V, E)$ with vertex weights $w: V -> RR$, find $S subset.eq V$ maximizing $sum_(v in S) w(v)$ such that $S$ is independent ($forall u, v in S: (u, v) in.not E$) and maximal (no vertex $u in V backslash S$ can be added to $S$ while maintaining independence).
+]
+
 
 == Set Problems
 
@@ -378,6 +386,20 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V|
   Given a composite integer $N$ and bit sizes $m, n$, find integers $p in [2, 2^m - 1]$ and $q in [2, 2^n - 1]$ such that $p times q = N$. Here $p$ has $m$ bits and $q$ has $n$ bits.
 ]
 
+== Specialized Problems
+
+#problem-def("BMF")[
+  Given an $m times n$ boolean matrix $A$ and rank $k$, find boolean matrices $B in {0,1}^(m times k)$ and $C in {0,1}^(k times n)$ minimizing the Hamming distance $d_H (A, B circle.tiny C)$, where the boolean product $(B circle.tiny C)_(i j) = or.big_ell (B_(i ell) and C_(ell j))$.
+]
+
+#problem-def("PaintShop")[
+  Given a sequence of $2n$ positions where each of $n$ cars appears exactly twice, assign a binary color to each car (each car's two occurrences receive opposite colors) to minimize the number of color changes between consecutive positions.
+]
+
+#problem-def("BicliqueCover")[
+  Given a bipartite graph $G = (L, R, E)$ and integer $k$, find $k$ bicliques $(L_1, R_1), dots, (L_k, R_k)$ that cover all edges ($E subset.eq union.big_i L_i times R_i$) while minimizing the total size $sum_i (|L_i| + |R_i|)$.
+]
+
 // Completeness check: warn about problem types in JSON but missing from paper
 #{
   let json-models = {
@@ -756,6 +778,15 @@ where $P$ is a penalty weight large enough that any constraint violation costs m
   _Correctness._ Original clause true $arrow.l.r$ auxiliary chain can propagate truth through new clauses.
 ]
 
+#reduction-rule("Satisfiability", "CircuitSAT",
+  example: true,
+  example-caption: [3-variable SAT formula to boolean circuit],
+)[
+  Each CNF clause $C_i = (ell_(i 1) or dots or ell_(i m_i))$ becomes an OR gate $g_i$, and a final AND gate computes $g_1 and dots and g_k$, constrained to output _true_.
+][
+  The circuit is satisfiable iff the CNF formula is satisfiable, since the AND-of-ORs structure is preserved exactly. Variable mapping: SAT variable $x_j$ maps to circuit input $x_j$; ancilla variables are the clause gate outputs and the final AND output.
+]
+
 #let cs_sg = load-example("circuitsat_to_spinglass")
 #let cs_sg_r = load-results("circuitsat_to_spinglass")
 #reduction-rule("CircuitSAT", "SpinGlass",

examples/reduction_ksatisfiability_to_satisfiability.rs

@@ -0,0 +1,140 @@
+// # K-Satisfiability (3-SAT) to Satisfiability Reduction (Trivial Embedding)
+//
+// ## Mathematical Equivalence
+// K-SAT is a special case of SAT where every clause has exactly k literals.
+// The reduction is a trivial embedding: the K-SAT clauses are directly used
+// as SAT clauses with no transformation needed.
+//
+// ## This Example
+// - Instance: 3-SAT with 4 variables and 3 clauses (each with exactly 3 literals)
+//   - C1: x1 OR NOT x2 OR x3
+//   - C2: NOT x1 OR x3 OR x4
+//   - C3: x2 OR NOT x3 OR NOT x4
+// - Source K-SAT: satisfiable
+// - Target: SAT with identical clauses (same variables, same clauses)
+//
+// ## Output
+// Exports `docs/paper/examples/ksatisfiability_to_satisfiability.json` and
+// `ksatisfiability_to_satisfiability.result.json`.
+
+use problemreductions::export::*;
+use problemreductions::prelude::*;
+use problemreductions::variant::K3;
+
+pub fn run() {
+    println!("=== K-Satisfiability (3-SAT) -> Satisfiability Reduction ===\n");
+
+    // 1. Create a small 3-SAT instance: 4 variables, 3 clauses (each with exactly 3 literals)
+    let clauses = vec![
+        CNFClause::new(vec![1, -2, 3]),  // x1 OR NOT x2 OR x3
+        CNFClause::new(vec![-1, 3, 4]),  // NOT x1 OR x3 OR x4
+        CNFClause::new(vec![2, -3, -4]), // x2 OR NOT x3 OR NOT x4
+    ];
+    let clause_strings = [
+        "x1 OR NOT x2 OR x3",
+        "NOT x1 OR x3 OR x4",
+        "x2 OR NOT x3 OR NOT x4",
+    ];
+
+    let ksat = KSatisfiability::<K3>::new(4, clauses);
+
+    println!("Source: KSatisfiability<K3> with {} variables, {} clauses", ksat.num_vars(), ksat.num_clauses());
+    for (i, c) in clause_strings.iter().enumerate() {
+        println!("  C{}: {}", i + 1, c);
+    }
+
+    // 2. Reduce to Satisfiability (trivial embedding)
+    let reduction = ReduceTo::<Satisfiability>::reduce_to(&ksat);
+    let sat = reduction.target_problem();
+
+    println!("\n=== Problem Transformation ===");
+    println!(
+        "Target: Satisfiability with {} variables, {} clauses",
+        sat.num_vars(),
+        sat.num_clauses()
+    );
+    println!("  (Trivial embedding: K-SAT is a special case of SAT, no transformation needed)");
+
+    // Print target clauses
+    println!("\n  Target SAT clauses:");
+    for (i, clause) in sat.clauses().iter().enumerate() {
+        println!("    Clause {}: {:?}", i, clause.literals);
+    }
+
+    // 3. Solve the target SAT problem (satisfaction problem)
+    let solver = BruteForce::new();
+    let sat_solutions = solver.find_all_satisfying(sat);
+    println!("\n=== Solution ===");
+    println!("Target SAT solutions found: {}", sat_solutions.len());
+
+    // 4. Extract and verify all solutions
+    let mut solutions = Vec::new();
+    for sat_sol in &sat_solutions {
+        let ksat_sol = reduction.extract_solution(sat_sol);
+        let valid = ksat.evaluate(&ksat_sol);
+        let assignment: Vec<String> = ksat_sol
+            .iter()
+            .enumerate()
+            .map(|(i, &v)| {
+                format!(
+                    "x{}={}",
+                    i + 1,
+                    if v == 1 { "T" } else { "F" }
+                )
+            })
+            .collect();
+        println!("  [{}] -> valid: {}", assignment.join(", "), valid);
+        assert!(valid, "Extracted K-SAT solution must be valid");
+
+        solutions.push(SolutionPair {
+            source_config: ksat_sol,
+            target_config: sat_sol.to_vec(),
+        });
+    }
+
+    println!(
+        "\nAll {} SAT solutions map to valid K-SAT assignments",
+        sat_solutions.len()
+    );
+    println!("Reduction verified successfully");
+
+    // 5. Export JSON
+    let source_variant = variant_to_map(KSatisfiability::<K3>::variant());
+    let target_variant = variant_to_map(Satisfiability::variant());
+    let overhead = lookup_overhead(
+        "KSatisfiability",
+        &source_variant,
+        "Satisfiability",
+        &target_variant,
+    )
+    .expect("KSatisfiability -> Satisfiability overhead not found");
+
+    let data = ReductionData {
+        source: ProblemSide {
+            problem: KSatisfiability::<K3>::NAME.to_string(),
+            variant: source_variant,
+            instance: serde_json::json!({
+                "num_vars": ksat.num_vars(),
+                "num_clauses": ksat.num_clauses(),
+                "k": 3,
+            }),
+        },
+        target: ProblemSide {
+            problem: Satisfiability::NAME.to_string(),
+            variant: target_variant,
+            instance: serde_json::json!({
+                "num_vars": sat.num_vars(),
+                "num_clauses": sat.num_clauses(),
+            }),
+        },
+        overhead: overhead_to_json(&overhead),
+    };
+
+    let results = ResultData { solutions };
+    let name = "ksatisfiability_to_satisfiability";
+    write_example(name, &data, &results);
+}
+
+fn main() {
+    run()
+}

examples/reduction_maximumsetpacking_to_maximumindependentset.rs

@@ -0,0 +1,145 @@
+// # Set Packing to Independent Set Reduction
+//
+// ## Mathematical Equivalence
+// Each set becomes a vertex; two vertices are adjacent if their sets overlap.
+// Selecting a collection of non-overlapping sets is equivalent to selecting
+// an independent set in the conflict graph. The optimal packing size equals
+// the maximum independent set size.
+//
+// ## This Example
+// - Instance: 5 sets over universe {0,...,7}, with varying sizes (2 and 3)
+//   - S0 = {0, 1, 2}, S1 = {2, 3}, S2 = {4, 5, 6}, S3 = {1, 5, 7}, S4 = {3, 6}
+// - Conflict edges: (0,1) share 2, (0,3) share 1, (1,4) share 3, (2,3) share 5, (2,4) share 6
+// - Source MaximumSetPacking: max packing size 2 (e.g., S0+S2, S1+S3, S3+S4, ...)
+// - Target MaximumIndependentSet: 5 vertices, 5 edges, max IS size 2
+//
+// ## Output
+// Exports `docs/paper/examples/maximumsetpacking_to_maximumindependentset.json` and
+// `maximumsetpacking_to_maximumindependentset.result.json`.
+//
+// See docs/paper/reductions.typ for the full reduction specification.
+
+use problemreductions::export::*;
+use problemreductions::prelude::*;
+use problemreductions::topology::{Graph, SimpleGraph};
+
+pub fn run() {
+    println!("\n=== Set Packing -> Independent Set Reduction ===\n");
+
+    // 1. Create MaximumSetPacking instance: 5 sets over universe {0,...,7}
+    let sets = vec![
+        vec![0, 1, 2], // S0 (size 3)
+        vec![2, 3],    // S1 (size 2, overlaps S0 at 2)
+        vec![4, 5, 6], // S2 (size 3, disjoint from S0, S1)
+        vec![1, 5, 7], // S3 (size 3, overlaps S0 at 1, S2 at 5)
+        vec![3, 6],    // S4 (size 2, overlaps S1 at 3, S2 at 6)
+    ];
+    let num_sets = sets.len();
+    let sp = MaximumSetPacking::with_weights(sets.clone(), vec![1i32; num_sets]);
+
+    println!("Source: MaximumSetPacking with {} sets", num_sets);
+    for (i, s) in sets.iter().enumerate() {
+        println!("  S{} = {:?}", i, s);
+    }
+
+    // 2. Reduce to MaximumIndependentSet
+    let reduction = ReduceTo::<MaximumIndependentSet<SimpleGraph, i32>>::reduce_to(&sp);
+    let target = reduction.target_problem();
+
+    println!("\nTarget: MaximumIndependentSet");
+    println!("  Vertices: {}", target.graph().num_vertices());
+    println!("  Edges: {} {:?}", target.graph().num_edges(), target.graph().edges());
+
+    // 3. Solve the target problem
+    let solver = BruteForce::new();
+    let target_solutions = solver.find_all_best(target);
+
+    println!("\nBest target solutions: {}", target_solutions.len());
+
+    // 4. Extract and verify each solution
+    let mut solutions = Vec::new();
+    for (i, target_sol) in target_solutions.iter().enumerate() {
+        let source_sol = reduction.extract_solution(target_sol);
+        let source_size = sp.evaluate(&source_sol);
+        let target_size = target.evaluate(target_sol);
+
+        println!(
+            "  Solution {}: target={:?} (size={:?}), source={:?} (size={:?}, valid={})",
+            i,
+            target_sol,
+            target_size,
+            source_sol,
+            source_size,
+            source_size.is_valid()
+        );
+
+        assert!(
+            source_size.is_valid(),
+            "Extracted source solution must be valid"
+        );
+
+        solutions.push(SolutionPair {
+            source_config: source_sol,
+            target_config: target_sol.clone(),
+        });
+    }
+
+    // 5. Verify the optimal value
+    let target_sol = &target_solutions[0];
+    let source_sol = reduction.extract_solution(target_sol);
+    let source_size = sp.evaluate(&source_sol);
+    let target_size = target.evaluate(target_sol);
+
+    assert_eq!(
+        source_size,
+        problemreductions::types::SolutionSize::Valid(2),
+        "MaximumSetPacking optimal packing size is 2"
+    );
+    assert_eq!(
+        target_size,
+        problemreductions::types::SolutionSize::Valid(2),
+        "MaximumIndependentSet should also have size 2"
+    );
+
+    // 6. Export JSON
+    let source_variant = variant_to_map(MaximumSetPacking::<i32>::variant());
+    let target_variant = variant_to_map(MaximumIndependentSet::<SimpleGraph, i32>::variant());
+    let overhead = lookup_overhead(
+        "MaximumSetPacking",
+        &source_variant,
+        "MaximumIndependentSet",
+        &target_variant,
+    )
+    .expect("MaximumSetPacking -> MaximumIndependentSet overhead not found");
+
+    let data = ReductionData {
+        source: ProblemSide {
+            problem: MaximumSetPacking::<i32>::NAME.to_string(),
+            variant: source_variant,
+            instance: serde_json::json!({
+                "num_sets": sp.num_sets(),
+                "sets": sp.sets(),
+            }),
+        },
+        target: ProblemSide {
+            problem: MaximumIndependentSet::<SimpleGraph, i32>::NAME.to_string(),
+            variant: target_variant,
+            instance: serde_json::json!({
+                "num_vertices": target.graph().num_vertices(),
+                "num_edges": target.graph().num_edges(),
+                "edges": target.graph().edges(),
+            }),
+        },
+        overhead: overhead_to_json(&overhead),
+    };
+
+    let results = ResultData { solutions };
+    let name = "maximumsetpacking_to_maximumindependentset";
+    write_example(name, &data, &results);
+
+    println!("\nDone: SetPacking(5 sets) optimal=2 maps to IS(5 vertices, 5 edges) optimal=2");
+}
+
+fn main() {
+    run()
+}