Skip to content

Commit 7207490

Browse files
GiggleLiuclaude
GiggleLiu
and
claude
authored
fix: close completeness gaps from review-implementation audit (#88) (#89)
* fix: add MaximalIS to CLI dispatch table Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * fix: add missing re-exports for MaximumClique, ILP, KSatisfiability Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * refactor: rename rule tests to closed_loop convention Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * docs: add paper entries for MaximalIS, BMF, PaintShop, BicliqueCover and SAT to CircuitSAT rule Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * feat: add example programs for SAT→CircuitSAT, SP→MIS, KSAT→SAT Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> * fix: use varying set sizes in SP→MIS example The previous example used only size-2 sets, which is degenerate (equivalent to a matching problem). Replace with 5 sets of sizes 2 and 3 over an 8-element universe for a more general demonstration. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
1 parent 7070fa6 commit 7207490

28 files changed

+518
-25
lines changed

‎docs/paper/reductions.typ‎

Lines changed: 31 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,10 @@
4545
"Factoring": [Factoring],
4646
"KingsSubgraph": [King's Subgraph MIS],
4747
"TriangularSubgraph": [Triangular Subgraph MIS],
48+
"MaximalIS": [Maximal Independent Set],
49+
"BMF": [Boolean Matrix Factorization],
50+
"PaintShop": [Paint Shop],
51+
"BicliqueCover": [Biclique Cover],
4852
)
4953

5054
// 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|
335339
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)$.
336340
]
337341

342+
#problem-def("MaximalIS")[
343+
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).
344+
]
345+
338346

339347
== Set Problems
340348

@@ -378,6 +386,20 @@ In all graph problems below, $G = (V, E)$ denotes an undirected graph with $|V|
378386
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.
379387
]
380388

389+
== Specialized Problems
390+
391+
#problem-def("BMF")[
392+
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))$.
393+
]
394+
395+
#problem-def("PaintShop")[
396+
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.
397+
]
398+
399+
#problem-def("BicliqueCover")[
400+
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|)$.
401+
]
402+
381403
// Completeness check: warn about problem types in JSON but missing from paper
382404
#{
383405
let json-models = {
@@ -756,6 +778,15 @@ where $P$ is a penalty weight large enough that any constraint violation costs m
756778
_Correctness._ Original clause true $arrow.l.r$ auxiliary chain can propagate truth through new clauses.
757779
]
758780

781+
#reduction-rule("Satisfiability", "CircuitSAT",
782+
example: true,
783+
example-caption: [3-variable SAT formula to boolean circuit],
784+
)[
785+
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_.
786+
][
787+
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.
788+
]
789+
759790
#let cs_sg = load-example("circuitsat_to_spinglass")
760791
#let cs_sg_r = load-results("circuitsat_to_spinglass")
761792
#reduction-rule("CircuitSAT", "SpinGlass",

‎examples/reduction_ksatisfiability_to_satisfiability.rs‎

Lines changed: 140 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,140 @@
1+
// # K-Satisfiability (3-SAT) to Satisfiability Reduction (Trivial Embedding)
2+
//
3+
// ## Mathematical Equivalence
4+
// K-SAT is a special case of SAT where every clause has exactly k literals.
5+
// The reduction is a trivial embedding: the K-SAT clauses are directly used
6+
// as SAT clauses with no transformation needed.
7+
//
8+
// ## This Example
9+
// - Instance: 3-SAT with 4 variables and 3 clauses (each with exactly 3 literals)
10+
// - C1: x1 OR NOT x2 OR x3
11+
// - C2: NOT x1 OR x3 OR x4
12+
// - C3: x2 OR NOT x3 OR NOT x4
13+
// - Source K-SAT: satisfiable
14+
// - Target: SAT with identical clauses (same variables, same clauses)
15+
//
16+
// ## Output
17+
// Exports `docs/paper/examples/ksatisfiability_to_satisfiability.json` and
18+
// `ksatisfiability_to_satisfiability.result.json`.
19+
20+
use problemreductions::export::*;
21+
use problemreductions::prelude::*;
22+
use problemreductions::variant::K3;
23+
24+
pub fn run() {
25+
println!("=== K-Satisfiability (3-SAT) -> Satisfiability Reduction ===\n");
26+
27+
// 1. Create a small 3-SAT instance: 4 variables, 3 clauses (each with exactly 3 literals)
28+
let clauses = vec![
29+
CNFClause::new(vec![1, -2, 3]), // x1 OR NOT x2 OR x3
30+
CNFClause::new(vec![-1, 3, 4]), // NOT x1 OR x3 OR x4
31+
CNFClause::new(vec![2, -3, -4]), // x2 OR NOT x3 OR NOT x4
32+
];
33+
let clause_strings = [
34+
"x1 OR NOT x2 OR x3",
35+
"NOT x1 OR x3 OR x4",
36+
"x2 OR NOT x3 OR NOT x4",
37+
];
38+
39+
let ksat = KSatisfiability::<K3>::new(4, clauses);
40+
41+
println!("Source: KSatisfiability<K3> with {} variables, {} clauses", ksat.num_vars(), ksat.num_clauses());
42+
for (i, c) in clause_strings.iter().enumerate() {
43+
println!(" C{}: {}", i + 1, c);
44+
}
45+
46+
// 2. Reduce to Satisfiability (trivial embedding)
47+
let reduction = ReduceTo::<Satisfiability>::reduce_to(&ksat);
48+
let sat = reduction.target_problem();
49+
50+
println!("\n=== Problem Transformation ===");
51+
println!(
52+
"Target: Satisfiability with {} variables, {} clauses",
53+
sat.num_vars(),
54+
sat.num_clauses()
55+
);
56+
println!(" (Trivial embedding: K-SAT is a special case of SAT, no transformation needed)");
57+
58+
// Print target clauses
59+
println!("\n Target SAT clauses:");
60+
for (i, clause) in sat.clauses().iter().enumerate() {
61+
println!(" Clause {}: {:?}", i, clause.literals);
62+
}
63+
64+
// 3. Solve the target SAT problem (satisfaction problem)
65+
let solver = BruteForce::new();
66+
let sat_solutions = solver.find_all_satisfying(sat);
67+
println!("\n=== Solution ===");
68+
println!("Target SAT solutions found: {}", sat_solutions.len());
69+
70+
// 4. Extract and verify all solutions
71+
let mut solutions = Vec::new();
72+
for sat_sol in &sat_solutions {
73+
let ksat_sol = reduction.extract_solution(sat_sol);
74+
let valid = ksat.evaluate(&ksat_sol);
75+
let assignment: Vec<String> = ksat_sol
76+
.iter()
77+
.enumerate()
78+
.map(|(i, &v)| {
79+
format!(
80+
"x{}={}",
81+
i + 1,
82+
if v == 1 { "T" } else { "F" }
83+
)
84+
})
85+
.collect();
86+
println!(" [{}] -> valid: {}", assignment.join(", "), valid);
87+
assert!(valid, "Extracted K-SAT solution must be valid");
88+
89+
solutions.push(SolutionPair {
90+
source_config: ksat_sol,
91+
target_config: sat_sol.to_vec(),
92+
});
93+
}
94+
95+
println!(
96+
"\nAll {} SAT solutions map to valid K-SAT assignments",
97+
sat_solutions.len()
98+
);
99+
println!("Reduction verified successfully");
100+
101+
// 5. Export JSON
102+
let source_variant = variant_to_map(KSatisfiability::<K3>::variant());
103+
let target_variant = variant_to_map(Satisfiability::variant());
104+
let overhead = lookup_overhead(
105+
"KSatisfiability",
106+
&source_variant,
107+
"Satisfiability",
108+
&target_variant,
109+
)
110+
.expect("KSatisfiability -> Satisfiability overhead not found");
111+
112+
let data = ReductionData {
113+
source: ProblemSide {
114+
problem: KSatisfiability::<K3>::NAME.to_string(),
115+
variant: source_variant,
116+
instance: serde_json::json!({
117+
"num_vars": ksat.num_vars(),
118+
"num_clauses": ksat.num_clauses(),
119+
"k": 3,
120+
}),
121+
},
122+
target: ProblemSide {
123+
problem: Satisfiability::NAME.to_string(),
124+
variant: target_variant,
125+
instance: serde_json::json!({
126+
"num_vars": sat.num_vars(),
127+
"num_clauses": sat.num_clauses(),
128+
}),
129+
},
130+
overhead: overhead_to_json(&overhead),
131+
};
132+
133+
let results = ResultData { solutions };
134+
let name = "ksatisfiability_to_satisfiability";
135+
write_example(name, &data, &results);
136+
}
137+
138+
fn main() {
139+
run()
140+
}

‎examples/reduction_maximumsetpacking_to_maximumindependentset.rs‎

Lines changed: 145 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,145 @@
1+
// # Set Packing to Independent Set Reduction
2+
//
3+
// ## Mathematical Equivalence
4+
// Each set becomes a vertex; two vertices are adjacent if their sets overlap.
5+
// Selecting a collection of non-overlapping sets is equivalent to selecting
6+
// an independent set in the conflict graph. The optimal packing size equals
7+
// the maximum independent set size.
8+
//
9+
// ## This Example
10+
// - Instance: 5 sets over universe {0,...,7}, with varying sizes (2 and 3)
11+
// - S0 = {0, 1, 2}, S1 = {2, 3}, S2 = {4, 5, 6}, S3 = {1, 5, 7}, S4 = {3, 6}
12+
// - Conflict edges: (0,1) share 2, (0,3) share 1, (1,4) share 3, (2,3) share 5, (2,4) share 6
13+
// - Source MaximumSetPacking: max packing size 2 (e.g., S0+S2, S1+S3, S3+S4, ...)
14+
// - Target MaximumIndependentSet: 5 vertices, 5 edges, max IS size 2
15+
//
16+
// ## Output
17+
// Exports `docs/paper/examples/maximumsetpacking_to_maximumindependentset.json` and
18+
// `maximumsetpacking_to_maximumindependentset.result.json`.
19+
//
20+
// See docs/paper/reductions.typ for the full reduction specification.
21+
22+
use problemreductions::export::*;
23+
use problemreductions::prelude::*;
24+
use problemreductions::topology::{Graph, SimpleGraph};
25+
26+
pub fn run() {
27+
println!("\n=== Set Packing -> Independent Set Reduction ===\n");
28+
29+
// 1. Create MaximumSetPacking instance: 5 sets over universe {0,...,7}
30+
let sets = vec![
31+
vec![0, 1, 2], // S0 (size 3)
32+
vec![2, 3], // S1 (size 2, overlaps S0 at 2)
33+
vec![4, 5, 6], // S2 (size 3, disjoint from S0, S1)
34+
vec![1, 5, 7], // S3 (size 3, overlaps S0 at 1, S2 at 5)
35+
vec![3, 6], // S4 (size 2, overlaps S1 at 3, S2 at 6)
36+
];
37+
let num_sets = sets.len();
38+
let sp = MaximumSetPacking::with_weights(sets.clone(), vec![1i32; num_sets]);
39+
40+
println!("Source: MaximumSetPacking with {} sets", num_sets);
41+
for (i, s) in sets.iter().enumerate() {
42+
println!(" S{} = {:?}", i, s);
43+
}
44+
45+
// 2. Reduce to MaximumIndependentSet
46+
let reduction = ReduceTo::<MaximumIndependentSet<SimpleGraph, i32>>::reduce_to(&sp);
47+
let target = reduction.target_problem();
48+
49+
println!("\nTarget: MaximumIndependentSet");
50+
println!(" Vertices: {}", target.graph().num_vertices());
51+
println!(" Edges: {} {:?}", target.graph().num_edges(), target.graph().edges());
52+
53+
// 3. Solve the target problem
54+
let solver = BruteForce::new();
55+
let target_solutions = solver.find_all_best(target);
56+
57+
println!("\nBest target solutions: {}", target_solutions.len());
58+
59+
// 4. Extract and verify each solution
60+
let mut solutions = Vec::new();
61+
for (i, target_sol) in target_solutions.iter().enumerate() {
62+
let source_sol = reduction.extract_solution(target_sol);
63+
let source_size = sp.evaluate(&source_sol);
64+
let target_size = target.evaluate(target_sol);
65+
66+
println!(
67+
" Solution {}: target={:?} (size={:?}), source={:?} (size={:?}, valid={})",
68+
i,
69+
target_sol,
70+
target_size,
71+
source_sol,
72+
source_size,
73+
source_size.is_valid()
74+
);
75+
76+
assert!(
77+
source_size.is_valid(),
78+
"Extracted source solution must be valid"
79+
);
80+
81+
solutions.push(SolutionPair {
82+
source_config: source_sol,
83+
target_config: target_sol.clone(),
84+
});
85+
}
86+
87+
// 5. Verify the optimal value
88+
let target_sol = &target_solutions[0];
89+
let source_sol = reduction.extract_solution(target_sol);
90+
let source_size = sp.evaluate(&source_sol);
91+
let target_size = target.evaluate(target_sol);
92+
93+
assert_eq!(
94+
source_size,
95+
problemreductions::types::SolutionSize::Valid(2),
96+
"MaximumSetPacking optimal packing size is 2"
97+
);
98+
assert_eq!(
99+
target_size,
100+
problemreductions::types::SolutionSize::Valid(2),
101+
"MaximumIndependentSet should also have size 2"
102+
);
103+
104+
// 6. Export JSON
105+
let source_variant = variant_to_map(MaximumSetPacking::<i32>::variant());
106+
let target_variant = variant_to_map(MaximumIndependentSet::<SimpleGraph, i32>::variant());
107+
let overhead = lookup_overhead(
108+
"MaximumSetPacking",
109+
&source_variant,
110+
"MaximumIndependentSet",
111+
&target_variant,
112+
)
113+
.expect("MaximumSetPacking -> MaximumIndependentSet overhead not found");
114+
115+
let data = ReductionData {
116+
source: ProblemSide {
117+
problem: MaximumSetPacking::<i32>::NAME.to_string(),
118+
variant: source_variant,
119+
instance: serde_json::json!({
120+
"num_sets": sp.num_sets(),
121+
"sets": sp.sets(),
122+
}),
123+
},
124+
target: ProblemSide {
125+
problem: MaximumIndependentSet::<SimpleGraph, i32>::NAME.to_string(),
126+
variant: target_variant,
127+
instance: serde_json::json!({
128+
"num_vertices": target.graph().num_vertices(),
129+
"num_edges": target.graph().num_edges(),
130+
"edges": target.graph().edges(),
131+
}),
132+
},
133+
overhead: overhead_to_json(&overhead),
134+
};
135+
136+
let results = ResultData { solutions };
137+
let name = "maximumsetpacking_to_maximumindependentset";
138+
write_example(name, &data, &results);
139+
140+
println!("\nDone: SetPacking(5 sets) optimal=2 maps to IS(5 vertices, 5 edges) optimal=2");
141+
}
142+
143+
fn main() {
144+
run()
145+
}

0 commit comments

Comments
 (0)