1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
//! The **action groupoid** — what symmetry breaking *means*, categorically, as checked code.
//!
//! Symmetry breaking is not a heuristic; it is the computation of `π₀` of a groupoid. A symmetry
//! group `G` acts on the space `X` of assignments (the "possible worlds"). The **action groupoid**
//! `X ⫽ G` has the assignments as objects and the group elements as the (iso)morphisms `α → g·α`:
//! two assignments are *isomorphic* iff related by a symmetry — bisimilar worlds. Symmetry breaking
//! keeps ONE assignment per isomorphism class — it computes the **skeleton**, equivalently
//! `π₀(X ⫽ G)` (the set of orbits = connected components). The exponential→polynomial collapse is
//! exactly `|X| → |π₀(X ⫽ G)|`.
//!
//! This `X ⫽ G` is a **1-groupoid** (h-level 3 in the homotopy-level table). The ∞-tower above it —
//! symmetries *between* symmetry-breakings, then between those, … — is the honest open direction. We
//! build the first rung (this 1-groupoid) solidly and *check* that symmetry breaking is its `π₀`; the
//! next rung (a groupoid of measures-and-their-morphisms) is sketched in the campaign notes. We do
//! not claim to have built an ∞-groupoid — only the 1-truncation that the present theory occupies,
//! and the precise statement of what climbing would mean.
use crate::cdcl::Lit;
use crate::proof::Perm;
/// The action groupoid `X ⫽ G`: assignments over `nv` variables acted on by the group generated by
/// `gens` (literal permutations). Small `nv` only — it enumerates all `2^nv` objects, which is the
/// point: it makes the orbit collapse *visible and checkable*.
pub struct ActionGroupoid {
nv: usize,
gens: Vec<Perm>,
}
impl ActionGroupoid {
pub fn new(nv: usize, gens: Vec<Perm>) -> Self {
ActionGroupoid { nv, gens }
}
/// Act by a (sign-respecting) symmetry on an assignment encoded as a bitmask: variable `v`'s value
/// is carried to variable `σ(+v).var`, flipped iff `σ(+v)` is negative.
fn act(&self, g: &Perm, a: u32) -> u32 {
let mut b = 0u32;
for v in 0..self.nv {
let val = (a >> v) & 1;
let img = g.apply(Lit::pos(v as u32));
let w = img.var() as usize;
let new_val = if img.is_positive() { val } else { 1 - val };
if new_val == 1 {
b |= 1 << w;
}
}
b
}
/// The orbit id of every assignment — `π₀(X ⫽ G)`, computed as the connected components of the
/// action via union-find. `orbits()[a]` is the canonical representative (smallest member) of `a`'s
/// orbit.
pub fn orbits(&self) -> Vec<u32> {
let total = 1u32 << self.nv;
let mut parent: Vec<u32> = (0..total).collect();
fn find(parent: &mut [u32], x: u32) -> u32 {
let mut r = x;
while parent[r as usize] != r {
r = parent[r as usize];
}
// path compression
let mut c = x;
while parent[c as usize] != r {
let next = parent[c as usize];
parent[c as usize] = r;
c = next;
}
r
}
for a in 0..total {
for g in &self.gens {
let b = self.act(g, a);
let (ra, rb) = (find(&mut parent, a), find(&mut parent, b));
if ra != rb {
// union by smaller-root so representatives are canonical (smallest)
if ra < rb {
parent[rb as usize] = ra;
} else {
parent[ra as usize] = rb;
}
}
}
}
(0..total).map(|a| find(&mut parent, a)).collect()
}
/// `|π₀(X ⫽ G)|` — the number of essentially-different worlds, i.e. exactly what symmetry breaking
/// reduces the search space to.
pub fn num_orbits(&self) -> usize {
let reps = self.orbits();
let mut distinct: Vec<u32> = reps.clone();
distinct.sort_unstable();
distinct.dedup();
distinct.len()
}
/// The full group `G` generated by `gens` (closed under composition, including the identity).
/// Bounded to `cap` elements so a pathological generating set can't blow up; the caller's small
/// examples are well within it.
pub fn group_elements(&self, cap: usize) -> Vec<Perm> {
let mut seen: std::collections::HashSet<Perm> = std::collections::HashSet::new();
let id = Perm::identity(self.nv);
seen.insert(id.clone());
let mut elems = vec![id];
let mut frontier = elems.clone();
while !frontier.is_empty() && elems.len() < cap {
let mut next = Vec::new();
for e in &frontier {
for g in &self.gens {
let prod = g.compose(e); // g ∘ e
if seen.insert(prod.clone()) {
next.push(prod.clone());
elems.push(prod);
if elems.len() >= cap {
return elems;
}
}
}
}
frontier = next;
}
elems
}
/// `π₁(X ⫽ G)` at the assignment `a` — its **stabilizer**: the group elements that fix `a`
/// (`g · a = a`). These are the loops at `a` in the action groupoid; the fundamental-group data of
/// the homotopy type at that component.
pub fn stabilizer_size(&self, a: u32, group: &[Perm]) -> usize {
group.iter().filter(|g| self.act(g, a) == a).count()
}
/// The size of `a`'s orbit (the connected component of `a`).
pub fn orbit_size(&self, a: u32) -> usize {
let reps = self.orbits();
reps.iter().filter(|&&r| r == reps[a as usize]).count()
}
}
#[cfg(test)]
mod tests {
use super::*;
/// The adjacent variable-transpositions that generate the full symmetric group `S_nv` on the bits.
fn full_symmetric_gens(nv: usize) -> Vec<Perm> {
(0..nv.saturating_sub(1))
.map(|i| {
let images: Vec<Lit> = (0..nv)
.map(|v| {
let w = if v == i {
i + 1
} else if v == i + 1 {
i
} else {
v
};
Lit::pos(w as u32)
})
.collect();
Perm::from_images(images)
})
.collect()
}
#[test]
fn symmetry_breaking_is_pi_zero_of_the_action_groupoid() {
// WHAT SYMMETRY BREAKING MEANS, made checkable. Under the full symmetric group acting on the
// bits, two assignments are isomorphic iff they have the same Hamming weight — so the `2^n`
// worlds collapse to exactly `n+1` orbits (weights `0..=n`). That orbit count IS the search
// space symmetry breaking leaves; the exponential→linear collapse is `2^n → n+1`, computed
// here as `π₀` of the action groupoid.
for nv in 3..=8 {
let g = ActionGroupoid::new(nv, full_symmetric_gens(nv));
assert_eq!(g.num_orbits(), nv + 1, "S_n on bits ⇒ orbits = Hamming weights = n+1");
assert!(
g.num_orbits() < (1usize << nv),
"exponential collapse: {} orbits vs {} worlds",
g.num_orbits(),
1usize << nv
);
}
}
#[test]
fn pi_one_of_the_action_groupoid_is_the_stabilizer_and_orbit_stabilizer_holds() {
// ONE MORE FINITE STEP up the tower: pin the homotopy type of X ⫽ G. π₀ = orbits (already);
// π₁ at a component = the STABILIZER. The two are bound by the fiber sequence Stab → G → Orbit
// — the orbit-stabilizer theorem: |G| = |orbit(a)| · |stab(a)| for every assignment a. We check
// it exhaustively under the full symmetric group on the bits (a small, fully-enumerable group).
for nv in 3..=5 {
let g = ActionGroupoid::new(nv, full_symmetric_gens(nv));
let group = g.group_elements(100_000);
// |S_n| = n!
let factorial: usize = (1..=nv).product();
assert_eq!(group.len(), factorial, "the generated group is S_{nv} of order {nv}!");
for a in 0..(1u32 << nv) {
let orbit = g.orbit_size(a);
let stab = g.stabilizer_size(a, &group);
assert_eq!(orbit * stab, group.len(), "orbit-stabilizer: |orbit|·|stab| = |G| at a={a}");
}
}
}
#[test]
fn the_trivial_group_quotients_nothing_and_a_swap_halves() {
// Sanity poles of the quotient. No symmetry ⇒ every world is its own orbit (`2^n`). A single
// variable-swap (a `Z/2` action) pairs `α` with its swap, so the orbit count is the number of
// swap-symmetric-or-paired worlds — strictly fewer than `2^n` whenever the swap moves anything.
let nv = 5;
let none = ActionGroupoid::new(nv, vec![Perm::identity(nv)]);
assert_eq!(none.num_orbits(), 1 << nv, "trivial action ⇒ no collapse");
let swap01: Perm = {
let images: Vec<Lit> =
(0..nv).map(|v| Lit::pos(if v == 0 { 1 } else if v == 1 { 0 } else { v } as u32)).collect();
Perm::from_images(images)
};
let g = ActionGroupoid::new(nv, vec![swap01]);
assert!(g.num_orbits() < (1 << nv), "a swap genuinely identifies worlds");
// Z/2 acting: orbits = fixed points (a₀=a₁) + paired points/2. #fixed = 2^(n-1), #moved = 2^(n-1),
// so orbits = 2^(n-1) + 2^(n-2) = 3·2^(n-2).
assert_eq!(g.num_orbits(), 3 * (1 << (nv - 2)), "Z/2 swap ⇒ 3·2^(n-2) orbits");
}
}