The demo below shows the core isolation trick in miniature. We have a small Boolean formula over 4 variables (x1, x2, x3, x4) with several satisfying assignments. Adding a random XOR constraint (a parity equation) cuts the solution space roughly in half each time.
<p class="hint">A Boolean formula over 4 variables has multiple satisfying assignments (shown below). Each <b>XOR constraint</b> is a random parity equation — it cuts the solution set roughly in half. Keep adding constraints until exactly <b>one solution survives</b>.</p>
<div id="solutions-panel">
<div class="panel-label">Surviving solutions (<span id="count">?</span>)</div>
<div id="solution-list"></div>
</div>
<div id="constraints-panel">
<div class="panel-label">XOR constraints added</div>
<div id="constraint-list"><em class="none-msg">None yet</em></div>
</div>
<div class="status" id="status"></div>
<div class="btns">
<button id="add" type="button">Add XOR constraint</button>
<button id="reset" type="button" class="ghost">Reset</button>
</div>
* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; font-size: 15px; }
.hint { font-size: .88rem; color: #444; margin: 0 0 .8rem; line-height: 1.5; }
#solutions-panel, #constraints-panel {
background: #f0f4f8; border: 1px solid #cdd6e0; border-radius: 8px;
padding: .55rem .75rem; margin-bottom: .6rem;
}
.panel-label { font-size: .78rem; font-weight: 700; color: #5a7088; text-transform: uppercase;
letter-spacing: .04em; margin-bottom: .35rem; }
#solution-list { display: flex; flex-wrap: wrap; gap: .35rem; }
.sol-chip {
font: 600 12px ui-monospace, monospace; padding: .2rem .5rem;
background: #1d3557; color: #fff; border-radius: 5px; transition: all .25s;
}
.sol-chip.eliminated { background: #b0b8c4; color: #666; text-decoration: line-through; }
.sol-chip.isolated { background: #0a7d33; box-shadow: 0 0 0 2px #0a7d3355; }
#constraint-list { font: 13px ui-monospace, monospace; color: #334; }
.xor-line { margin: .15rem 0; }
em.none-msg { font-style: italic; color: #999; font-size: .85rem; }
.status { font-size: .95rem; font-weight: 600; min-height: 1.4em; margin: .4rem 0; }
.status.ok { color: #0a7d33; }
.status.warn { color: #b35900; }
.status.info { color: #1d3557; }
.btns { display: flex; gap: .5rem; flex-wrap: wrap; }
button { font: 600 14px system-ui, sans-serif; padding: .45rem .95rem;
border: 1px solid #1d3557; background: #1d3557; color: #fff;
border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }
button:disabled { opacity: .45; cursor: default; }
const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Valiant-Vazirani isolation demo.
// We have 4 Boolean variables: x1,x2,x3,x4.
// The "formula" is: all assignments where NOT (x1=0 AND x2=0 AND x3=0 AND x4=0)
// i.e., all 15 non-zero assignments, giving a manageable set to visualise.
//
// A XOR constraint is a random non-empty subset S ⊆ {1,2,3,4} and a random bit b.
// It says: XOR of x_i for i in S = b.
// Each such constraint cuts the solution space in half (exactly, for full-rank systems).
// The Valiant-Vazirani lemma: after ~log2(|solutions|) constraints,
// with probability ≥ 1/8 exactly one solution survives.
const VARS = 4;
const varNames = ['x₁','x₂','x₃','x₄'];
// All assignments of 4 bits as arrays [x1,x2,x3,x4] ∈ {0,1}^4
// Exclude all-zero (our "formula" forbids it).
const ALL_ASSIGNMENTS = [];
for (let m = 1; m < (1 << VARS); m++) {
const a = [];
for (let i = 0; i < VARS; i++) a.push((m >> i) & 1);
ALL_ASSIGNMENTS.push(a);
}
let surviving = ALL_ASSIGNMENTS.slice(); // currently surviving assignments
let constraints = []; // list of {subset, b}
function assignLabel(a) {
// e.g. "1010"
return a.join('');
}
function satisfiesConstraint(a, c) {
// XOR of a[i] for i in c.subset equals c.b
let xorVal = 0;
for (const i of c.subset) xorVal ^= a[i];
return xorVal === c.b;
}
function randomConstraint() {
// Random non-empty subset of variable indices
let subset = [];
while (subset.length === 0) {
subset = [];
for (let i = 0; i < VARS; i++) {
if (Math.random() < 0.5) subset.push(i);
}
}
const b = Math.random() < 0.5 ? 0 : 1;
return { subset, b };
}
function constraintLabel(c) {
const terms = c.subset.map(i => varNames[i]).join(' ⊕ '); // ⊕
return terms + ' = ' + c.b;
}
function render() {
// Solution chips
const list = document.getElementById('solution-list');
list.innerHTML = '';
const survivingSet = new Set(surviving.map(assignLabel));
for (const a of ALL_ASSIGNMENTS) {
const chip = document.createElement('span');
chip.className = 'sol-chip';
chip.title = varNames.map((v,i) => v+'='+a[i]).join(', ');
const lbl = assignLabel(a);
if (survivingSet.has(lbl)) {
if (surviving.length === 1) chip.classList.add('isolated');
} else {
chip.classList.add('eliminated');
}
chip.textContent = lbl;
list.appendChild(chip);
}
document.getElementById('count').textContent = surviving.length;
// Constraints
const clist = document.getElementById('constraint-list');
if (constraints.length === 0) {
clist.innerHTML = '<em class="none-msg">None yet</em>';
} else {
clist.innerHTML = constraints.map((c, i) =>
'<div class="xor-line">' + (i+1) + '. ' + constraintLabel(c) + '</div>'
).join('');
}
// Status
const st = document.getElementById('status');
const addBtn = document.getElementById('add');
if (surviving.length === 0) {
st.textContent = `No solutions survive — try Reset and a different random run.`;
st.className = 'status warn';
addBtn.disabled = true;
} else if (surviving.length === 1) {
const a = surviving[0];
st.textContent = fmt(`✓ Isolated! Unique solution: %map%`, { map: varNames.map((v,i) => v+'='+a[i]).join(', ') });
st.className = 'status ok';
addBtn.disabled = true;
console.log(`Valiant-Vazirani: isolated solution`, assignLabel(a), `after`, constraints.length, `XOR constraints`);
} else {
st.textContent = fmt(`%length% solutions remain. Add more XOR constraints.`, { length: surviving.length });
st.className = 'status info';
addBtn.disabled = false;
}
}
function addConstraint() {
const c = randomConstraint();
constraints.push(c);
surviving = surviving.filter(a => satisfiesConstraint(a, c));
render();
}
function reset() {
surviving = ALL_ASSIGNMENTS.slice();
constraints = [];
document.getElementById('add').disabled = false;
render();
}
document.getElementById('add').addEventListener('click', addConstraint);
document.getElementById('reset').addEventListener('click', reset);
reset();
<p class="hint">A Boolean formula over 4 variables has multiple satisfying assignments (shown below). Each <b>XOR constraint</b> is a random parity equation — it cuts the solution set roughly in half. Keep adding constraints until exactly <b>one solution survives</b>.</p>
<div id="solutions-panel">
<div class="panel-label">Surviving solutions (<span id="count">?</span>)</div>
<div id="solution-list"></div>
</div>
<div id="constraints-panel">
<div class="panel-label">XOR constraints added</div>
<div id="constraint-list"><em class="none-msg">None yet</em></div>
</div>
<div class="status" id="status"></div>
<div class="btns">
<button id="add" type="button">Add XOR constraint</button>
<button id="reset" type="button" class="ghost">Reset</button>
</div>
* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; font-size: 15px; }
.hint { font-size: .88rem; color: #444; margin: 0 0 .8rem; line-height: 1.5; }
#solutions-panel, #constraints-panel {
background: #f0f4f8; border: 1px solid #cdd6e0; border-radius: 8px;
padding: .55rem .75rem; margin-bottom: .6rem;
}
.panel-label { font-size: .78rem; font-weight: 700; color: #5a7088; text-transform: uppercase;
letter-spacing: .04em; margin-bottom: .35rem; }
#solution-list { display: flex; flex-wrap: wrap; gap: .35rem; }
.sol-chip {
font: 600 12px ui-monospace, monospace; padding: .2rem .5rem;
background: #1d3557; color: #fff; border-radius: 5px; transition: all .25s;
}
.sol-chip.eliminated { background: #b0b8c4; color: #666; text-decoration: line-through; }
.sol-chip.isolated { background: #0a7d33; box-shadow: 0 0 0 2px #0a7d3355; }
#constraint-list { font: 13px ui-monospace, monospace; color: #334; }
.xor-line { margin: .15rem 0; }
em.none-msg { font-style: italic; color: #999; font-size: .85rem; }
.status { font-size: .95rem; font-weight: 600; min-height: 1.4em; margin: .4rem 0; }
.status.ok { color: #0a7d33; }
.status.warn { color: #b35900; }
.status.info { color: #1d3557; }
.btns { display: flex; gap: .5rem; flex-wrap: wrap; }
button { font: 600 14px system-ui, sans-serif; padding: .45rem .95rem;
border: 1px solid #1d3557; background: #1d3557; color: #fff;
border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }
button:disabled { opacity: .45; cursor: default; }
const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Valiant-Vazirani isolation demo.
// We have 4 Boolean variables: x1,x2,x3,x4.
// The "formula" is: all assignments where NOT (x1=0 AND x2=0 AND x3=0 AND x4=0)
// i.e., all 15 non-zero assignments, giving a manageable set to visualise.
//
// A XOR constraint is a random non-empty subset S ⊆ {1,2,3,4} and a random bit b.
// It says: XOR of x_i for i in S = b.
// Each such constraint cuts the solution space in half (exactly, for full-rank systems).
// The Valiant-Vazirani lemma: after ~log2(|solutions|) constraints,
// with probability ≥ 1/8 exactly one solution survives.
const VARS = 4;
const varNames = ['x₁','x₂','x₃','x₄'];
// All assignments of 4 bits as arrays [x1,x2,x3,x4] ∈ {0,1}^4
// Exclude all-zero (our "formula" forbids it).
const ALL_ASSIGNMENTS = [];
for (let m = 1; m < (1 << VARS); m++) {
const a = [];
for (let i = 0; i < VARS; i++) a.push((m >> i) & 1);
ALL_ASSIGNMENTS.push(a);
}
let surviving = ALL_ASSIGNMENTS.slice(); // currently surviving assignments
let constraints = []; // list of {subset, b}
function assignLabel(a) {
// e.g. "1010"
return a.join('');
}
function satisfiesConstraint(a, c) {
// XOR of a[i] for i in c.subset equals c.b
let xorVal = 0;
for (const i of c.subset) xorVal ^= a[i];
return xorVal === c.b;
}
function randomConstraint() {
// Random non-empty subset of variable indices
let subset = [];
while (subset.length === 0) {
subset = [];
for (let i = 0; i < VARS; i++) {
if (Math.random() < 0.5) subset.push(i);
}
}
const b = Math.random() < 0.5 ? 0 : 1;
return { subset, b };
}
function constraintLabel(c) {
const terms = c.subset.map(i => varNames[i]).join(' ⊕ '); // ⊕
return terms + ' = ' + c.b;
}
function render() {
// Solution chips
const list = document.getElementById('solution-list');
list.innerHTML = '';
const survivingSet = new Set(surviving.map(assignLabel));
for (const a of ALL_ASSIGNMENTS) {
const chip = document.createElement('span');
chip.className = 'sol-chip';
chip.title = varNames.map((v,i) => v+'='+a[i]).join(', ');
const lbl = assignLabel(a);
if (survivingSet.has(lbl)) {
if (surviving.length === 1) chip.classList.add('isolated');
} else {
chip.classList.add('eliminated');
}
chip.textContent = lbl;
list.appendChild(chip);
}
document.getElementById('count').textContent = surviving.length;
// Constraints
const clist = document.getElementById('constraint-list');
if (constraints.length === 0) {
clist.innerHTML = '<em class="none-msg">None yet</em>';
} else {
clist.innerHTML = constraints.map((c, i) =>
'<div class="xor-line">' + (i+1) + '. ' + constraintLabel(c) + '</div>'
).join('');
}
// Status
const st = document.getElementById('status');
const addBtn = document.getElementById('add');
if (surviving.length === 0) {
st.textContent = `No solutions survive — try Reset and a different random run.`;
st.className = 'status warn';
addBtn.disabled = true;
} else if (surviving.length === 1) {
const a = surviving[0];
st.textContent = fmt(`✓ Isolated! Unique solution: %map%`, { map: varNames.map((v,i) => v+'='+a[i]).join(', ') });
st.className = 'status ok';
addBtn.disabled = true;
console.log(`Valiant-Vazirani: isolated solution`, assignLabel(a), `after`, constraints.length, `XOR constraints`);
} else {
st.textContent = fmt(`%length% solutions remain. Add more XOR constraints.`, { length: surviving.length });
st.className = 'status info';
addBtn.disabled = false;
}
}
function addConstraint() {
const c = randomConstraint();
constraints.push(c);
surviving = surviving.filter(a => satisfiesConstraint(a, c));
render();
}
function reset() {
surviving = ALL_ASSIGNMENTS.slice();
constraints = [];
document.getElementById('add').disabled = false;
render();
}
document.getElementById('add').addEventListener('click', addConstraint);
document.getElementById('reset').addEventListener('click', reset);
reset();
Press Add XOR constraint to add another random parity equation over a random subset of variables. Watch how the number of surviving solutions drops — with good probability you'll be left with exactly one. Press Reset to start over with all solutions. Notice that after about 4 constraints you either have 0 or 1 solution: that is the isolation lemma working in real time.
Comments
Loading comments...