The demo below shows a small DNF (OR of ANDs). Set the restriction probability p and press Apply random restriction to randomly freeze some variables. Watch how many clauses survive, how many collapse to constants, and what the residual formula looks like.
<p class="hint">A <b>DNF</b> (OR of ANDs) is shown below. Each clause is an AND of literals.
Set the restriction probability <b>p</b> (chance a variable stays free) and press
<b>Apply random restriction</b> to randomly fix some variables to 0 or 1.
Watch how the formula shrinks — this collapse is the engine of Håstad's proof.</p>
<div class="controls">
<label>p = <span id="pval">0.30</span>
<input type="range" id="pslider" min="0.05" max="1.0" step="0.05" value="0.30">
</label>
<button id="restrict" type="button">Apply random restriction</button>
<button id="reset" type="button" class="ghost">Reset</button>
</div>
<div id="formula-area">
<div class="section-label">Original DNF</div>
<div id="original-dnf" class="dnf-display"></div>
<div id="result-area" class="hidden">
<div class="section-label">After restriction</div>
<div id="restricted-dnf" class="dnf-display"></div>
<div id="stats" class="stats"></div>
</div>
</div>
* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; }
.hint { font-size: .88rem; color: #444; margin: 0 0 .7rem; line-height: 1.5; }
.controls { display: flex; flex-wrap: wrap; gap: .6rem; align-items: center; margin-bottom: .9rem; }
label { font-size: .9rem; display: flex; align-items: center; gap: .4rem; }
input[type=range] { width: 130px; }
button { font: 600 13px system-ui; padding: .42rem .85rem; border: 1px solid #1d3557;
background: #1d3557; color: #fff; border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }
#formula-area { margin-top: .4rem; }
.section-label { font-size: .78rem; font-weight: 700; text-transform: uppercase;
letter-spacing: .06em; color: #6b7a8d; margin: .6rem 0 .3rem; }
.dnf-display { display: flex; flex-wrap: wrap; gap: 6px; align-items: center; min-height: 2rem; }
.clause { display: flex; gap: 3px; align-items: center; background: #e8eef3;
border: 1px solid #cdd9e3; border-radius: 8px; padding: 4px 8px;
font: 600 13px ui-monospace, monospace; }
.lit { padding: 1px 4px; border-radius: 4px; background: #d0dae5; color: #1d3557; }
.lit.neg { background: #f0d5d8; color: #9b1c28; }
.lit.fixed-1 { background: #bbf0d0; color: #1a6636; }
.lit.fixed-0 { background: #e0e0e0; color: #999; text-decoration: line-through; }
.clause.true-clause { border-color: #1a6636; background: #e8f7ee; }
.clause.false-clause { border-color: #aaa; background: #f0f0f0; opacity: .5; }
.or-sep { color: #6b7a8d; font-weight: 700; font-size: 1rem; }
.stats { margin-top: .7rem; font-size: .88rem; line-height: 1.6; }
.stats b { color: #1d3557; }
.good { color: #1a6636; font-weight: 700; }
.bad { color: #9b1c28; font-weight: 700; }
.hidden { display: none; }
const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Håstad Switching Lemma demo
// Shows a DNF (OR of ANDs); applies a p-random restriction;
// evaluates clauses and shows what remains.
//
// Key claim: after a p-random restriction, any width-w DNF becomes computable by a small decision tree with high probability.
const VARS = ['x1','x2','x3','x4','x5','x6'];
// Fixed DNF: 5 clauses, each of width 3
const DNF = [
[{v:'x1',neg:false},{v:'x2',neg:false},{v:'x3',neg:false}], // x1 AND x2 AND x3
[{v:'x2',neg:true}, {v:'x4',neg:false},{v:'x5',neg:false}], // ¬x2 AND x4 AND x5
[{v:'x1',neg:true}, {v:'x3',neg:true}, {v:'x6',neg:false}], // ¬x1 AND ¬x3 AND x6
[{v:'x4',neg:true}, {v:'x5',neg:true}, {v:'x6',neg:true}], // ¬x4 AND ¬x5 AND ¬x6
[{v:'x3',neg:false},{v:'x4',neg:false},{v:'x6',neg:true}], // x3 AND x4 AND ¬x6
];
function litLabel(l) { return (l.neg ? '¬' : '') + l.v; }
function renderClause(clause, assignment) {
// Returns {el, status: ’free’|’true’|’false’}
const el = document.createElement('div');
el.className = 'clause';
let clauseTrue = false;
let clauseFalse = false;
let freeLits = [];
clause.forEach((lit, i) => {
if (i > 0) { const sep = document.createElement('span'); sep.textContent = '·'; sep.style.color='#6b7a8d'; el.appendChild(sep); }
const span = document.createElement('span');
span.className = 'lit';
const val = assignment[lit.v];
if (val === undefined) {
// free
span.textContent = litLabel(lit);
if (lit.neg) span.classList.add('neg');
freeLits.push(lit);
} else {
// fixed
const litVal = lit.neg ? (1 - val) : val;
span.textContent = litLabel(lit) + '=' + litVal;
if (litVal === 1) { span.classList.add('fixed-1'); clauseTrue = true; }
else { span.classList.add('fixed-0'); clauseFalse = true; }
}
el.appendChild(span);
});
// A clause is TRUE (collapsed to 1) if any literal is fixed-true
// A clause is FALSE (collapsed to 0) if all literals are fixed-false
const allFixed = clause.every(l => assignment[l.v] !== undefined);
const allFalse = clause.every(l => { const v = assignment[l.v]; if(v===undefined) return false; return (l.neg ? (1-v) : v) === 0; });
if (clauseTrue) { el.className='clause true-clause'; return {el, status:'true'}; }
if (allFalse) { el.className='clause false-clause'; return {el, status:'false'}; }
return {el, status:'free'};
}
function renderDNF(dnf, assignment, container) {
container.innerHTML = '';
dnf.forEach((clause, i) => {
if (i > 0) {
const sep = document.createElement('span');
sep.className = 'or-sep'; sep.textContent = '∨'; container.appendChild(sep);
}
const {el} = renderClause(clause, assignment);
container.appendChild(el);
});
}
// Original (no assignment)
const origContainer = document.getElementById('original-dnf');
renderDNF(DNF, {}, origContainer);
document.getElementById('pslider').addEventListener('input', function() {
document.getElementById('pval').textContent = parseFloat(this.value).toFixed(2);
});
document.getElementById('restrict').addEventListener('click', function() {
const p = parseFloat(document.getElementById('pslider').value);
const assignment = {};
VARS.forEach(v => {
if (Math.random() >= p) {
// fix to 0 or 1
assignment[v] = Math.random() < 0.5 ? 0 : 1;
}
});
const resultArea = document.getElementById('result-area');
const restricted = document.getElementById('restricted-dnf');
resultArea.classList.remove('hidden');
// Render each clause with assignment
restricted.innerHTML = '';
let trueCount = 0, falseCount = 0, freeCount = 0;
const freeVarsInResult = new Set();
DNF.forEach((clause, i) => {
if (i > 0) {
const sep = document.createElement('span');
sep.className = 'or-sep'; sep.textContent = '∨'; restricted.appendChild(sep);
}
const {el, status} = renderClause(clause, assignment);
restricted.appendChild(el);
if (status === 'true') trueCount++;
else if (status === 'false') falseCount++;
else {
freeCount++;
clause.forEach(l => { if (assignment[l.v] === undefined) freeVarsInResult.add(l.v); });
}
});
const fixed = VARS.filter(v => assignment[v] !== undefined).length;
const free = VARS.length - fixed;
const stats = document.getElementById('stats');
const resultWord = trueCount > 0 ? '<span class="good">TRUE (formula is 1)</span>'
: freeCount === 0 ? '<span class="bad">FALSE (all clauses killed)</span>'
: fmt(`<span class="bad">formula has %freeCount% remaining clause(s)</span>`, { freeCount: freeCount });
// Hastad bound: meaningful only when 5p < 1 (p < 0.2)
const fivep = 5 * p;
const boundNote = fivep < 1
? fmt(`Håstad’s lemma (meaningful here since p < 0.2): width-3 DNF becomes a depth-s decision tree with prob ≥ 1 − (%fivep%)^s ≈ 1 − %pow% for s=3.`, { fivep: fivep.toFixed(2), pow: Math.pow(fivep, 3).toFixed(4) })
: `Try p ≤ 0.15 to see Håstad’s bound become informative (needs 5p < 1).`;
stats.innerHTML =
fmt(`<b>Variables fixed:</b> %fixed% / %length% (p = %p% kept free).<br><b>Clauses collapsed to TRUE:</b> %trueCount% | <b>to FALSE:</b> %falseCount% | <b>still active:</b> %freeCount%.<br><b>Free variables left in active clauses:</b> %v%.<br>Overall result: %resultWord%.<br><small>%boundNote%</small>`, { fixed: fixed, length: VARS.length, p: p.toFixed(2), trueCount: trueCount, falseCount: falseCount, freeCount: freeCount, v: freeVarsInResult.size > 0 ? [...freeVarsInResult].join(', ') : `none`, resultWord: resultWord, boundNote: boundNote });
// Log the assignment for verification
console.log(`Assignment:`, assignment, '| Active clauses:', freeCount,
'| True clauses:', trueCount, '| False clauses:', falseCount);
});
document.getElementById('reset').addEventListener('click', function() {
document.getElementById('result-area').classList.add('hidden');
});
<p class="hint">A <b>DNF</b> (OR of ANDs) is shown below. Each clause is an AND of literals.
Set the restriction probability <b>p</b> (chance a variable stays free) and press
<b>Apply random restriction</b> to randomly fix some variables to 0 or 1.
Watch how the formula shrinks — this collapse is the engine of Håstad's proof.</p>
<div class="controls">
<label>p = <span id="pval">0.30</span>
<input type="range" id="pslider" min="0.05" max="1.0" step="0.05" value="0.30">
</label>
<button id="restrict" type="button">Apply random restriction</button>
<button id="reset" type="button" class="ghost">Reset</button>
</div>
<div id="formula-area">
<div class="section-label">Original DNF</div>
<div id="original-dnf" class="dnf-display"></div>
<div id="result-area" class="hidden">
<div class="section-label">After restriction</div>
<div id="restricted-dnf" class="dnf-display"></div>
<div id="stats" class="stats"></div>
</div>
</div>
* { box-sizing: border-box; }
body { font-family: system-ui, sans-serif; color: #222; margin: 0; }
.hint { font-size: .88rem; color: #444; margin: 0 0 .7rem; line-height: 1.5; }
.controls { display: flex; flex-wrap: wrap; gap: .6rem; align-items: center; margin-bottom: .9rem; }
label { font-size: .9rem; display: flex; align-items: center; gap: .4rem; }
input[type=range] { width: 130px; }
button { font: 600 13px system-ui; padding: .42rem .85rem; border: 1px solid #1d3557;
background: #1d3557; color: #fff; border-radius: 8px; cursor: pointer; }
button.ghost { background: #fff; color: #1d3557; }
#formula-area { margin-top: .4rem; }
.section-label { font-size: .78rem; font-weight: 700; text-transform: uppercase;
letter-spacing: .06em; color: #6b7a8d; margin: .6rem 0 .3rem; }
.dnf-display { display: flex; flex-wrap: wrap; gap: 6px; align-items: center; min-height: 2rem; }
.clause { display: flex; gap: 3px; align-items: center; background: #e8eef3;
border: 1px solid #cdd9e3; border-radius: 8px; padding: 4px 8px;
font: 600 13px ui-monospace, monospace; }
.lit { padding: 1px 4px; border-radius: 4px; background: #d0dae5; color: #1d3557; }
.lit.neg { background: #f0d5d8; color: #9b1c28; }
.lit.fixed-1 { background: #bbf0d0; color: #1a6636; }
.lit.fixed-0 { background: #e0e0e0; color: #999; text-decoration: line-through; }
.clause.true-clause { border-color: #1a6636; background: #e8f7ee; }
.clause.false-clause { border-color: #aaa; background: #f0f0f0; opacity: .5; }
.or-sep { color: #6b7a8d; font-weight: 700; font-size: 1rem; }
.stats { margin-top: .7rem; font-size: .88rem; line-height: 1.6; }
.stats b { color: #1d3557; }
.good { color: #1a6636; font-weight: 700; }
.bad { color: #9b1c28; font-weight: 700; }
.hidden { display: none; }
const fmt = (s, v) => s.replace(/%(\w+)%/g, (_, k) => String(v[k] ?? ''));
// Håstad Switching Lemma demo
// Shows a DNF (OR of ANDs); applies a p-random restriction;
// evaluates clauses and shows what remains.
//
// Key claim: after a p-random restriction, any width-w DNF becomes computable by a small decision tree with high probability.
const VARS = ['x1','x2','x3','x4','x5','x6'];
// Fixed DNF: 5 clauses, each of width 3
const DNF = [
[{v:'x1',neg:false},{v:'x2',neg:false},{v:'x3',neg:false}], // x1 AND x2 AND x3
[{v:'x2',neg:true}, {v:'x4',neg:false},{v:'x5',neg:false}], // ¬x2 AND x4 AND x5
[{v:'x1',neg:true}, {v:'x3',neg:true}, {v:'x6',neg:false}], // ¬x1 AND ¬x3 AND x6
[{v:'x4',neg:true}, {v:'x5',neg:true}, {v:'x6',neg:true}], // ¬x4 AND ¬x5 AND ¬x6
[{v:'x3',neg:false},{v:'x4',neg:false},{v:'x6',neg:true}], // x3 AND x4 AND ¬x6
];
function litLabel(l) { return (l.neg ? '¬' : '') + l.v; }
function renderClause(clause, assignment) {
// Returns {el, status: ’free’|’true’|’false’}
const el = document.createElement('div');
el.className = 'clause';
let clauseTrue = false;
let clauseFalse = false;
let freeLits = [];
clause.forEach((lit, i) => {
if (i > 0) { const sep = document.createElement('span'); sep.textContent = '·'; sep.style.color='#6b7a8d'; el.appendChild(sep); }
const span = document.createElement('span');
span.className = 'lit';
const val = assignment[lit.v];
if (val === undefined) {
// free
span.textContent = litLabel(lit);
if (lit.neg) span.classList.add('neg');
freeLits.push(lit);
} else {
// fixed
const litVal = lit.neg ? (1 - val) : val;
span.textContent = litLabel(lit) + '=' + litVal;
if (litVal === 1) { span.classList.add('fixed-1'); clauseTrue = true; }
else { span.classList.add('fixed-0'); clauseFalse = true; }
}
el.appendChild(span);
});
// A clause is TRUE (collapsed to 1) if any literal is fixed-true
// A clause is FALSE (collapsed to 0) if all literals are fixed-false
const allFixed = clause.every(l => assignment[l.v] !== undefined);
const allFalse = clause.every(l => { const v = assignment[l.v]; if(v===undefined) return false; return (l.neg ? (1-v) : v) === 0; });
if (clauseTrue) { el.className='clause true-clause'; return {el, status:'true'}; }
if (allFalse) { el.className='clause false-clause'; return {el, status:'false'}; }
return {el, status:'free'};
}
function renderDNF(dnf, assignment, container) {
container.innerHTML = '';
dnf.forEach((clause, i) => {
if (i > 0) {
const sep = document.createElement('span');
sep.className = 'or-sep'; sep.textContent = '∨'; container.appendChild(sep);
}
const {el} = renderClause(clause, assignment);
container.appendChild(el);
});
}
// Original (no assignment)
const origContainer = document.getElementById('original-dnf');
renderDNF(DNF, {}, origContainer);
document.getElementById('pslider').addEventListener('input', function() {
document.getElementById('pval').textContent = parseFloat(this.value).toFixed(2);
});
document.getElementById('restrict').addEventListener('click', function() {
const p = parseFloat(document.getElementById('pslider').value);
const assignment = {};
VARS.forEach(v => {
if (Math.random() >= p) {
// fix to 0 or 1
assignment[v] = Math.random() < 0.5 ? 0 : 1;
}
});
const resultArea = document.getElementById('result-area');
const restricted = document.getElementById('restricted-dnf');
resultArea.classList.remove('hidden');
// Render each clause with assignment
restricted.innerHTML = '';
let trueCount = 0, falseCount = 0, freeCount = 0;
const freeVarsInResult = new Set();
DNF.forEach((clause, i) => {
if (i > 0) {
const sep = document.createElement('span');
sep.className = 'or-sep'; sep.textContent = '∨'; restricted.appendChild(sep);
}
const {el, status} = renderClause(clause, assignment);
restricted.appendChild(el);
if (status === 'true') trueCount++;
else if (status === 'false') falseCount++;
else {
freeCount++;
clause.forEach(l => { if (assignment[l.v] === undefined) freeVarsInResult.add(l.v); });
}
});
const fixed = VARS.filter(v => assignment[v] !== undefined).length;
const free = VARS.length - fixed;
const stats = document.getElementById('stats');
const resultWord = trueCount > 0 ? '<span class="good">TRUE (formula is 1)</span>'
: freeCount === 0 ? '<span class="bad">FALSE (all clauses killed)</span>'
: fmt(`<span class="bad">formula has %freeCount% remaining clause(s)</span>`, { freeCount: freeCount });
// Hastad bound: meaningful only when 5p < 1 (p < 0.2)
const fivep = 5 * p;
const boundNote = fivep < 1
? fmt(`Håstad’s lemma (meaningful here since p < 0.2): width-3 DNF becomes a depth-s decision tree with prob ≥ 1 − (%fivep%)^s ≈ 1 − %pow% for s=3.`, { fivep: fivep.toFixed(2), pow: Math.pow(fivep, 3).toFixed(4) })
: `Try p ≤ 0.15 to see Håstad’s bound become informative (needs 5p < 1).`;
stats.innerHTML =
fmt(`<b>Variables fixed:</b> %fixed% / %length% (p = %p% kept free).<br><b>Clauses collapsed to TRUE:</b> %trueCount% | <b>to FALSE:</b> %falseCount% | <b>still active:</b> %freeCount%.<br><b>Free variables left in active clauses:</b> %v%.<br>Overall result: %resultWord%.<br><small>%boundNote%</small>`, { fixed: fixed, length: VARS.length, p: p.toFixed(2), trueCount: trueCount, falseCount: falseCount, freeCount: freeCount, v: freeVarsInResult.size > 0 ? [...freeVarsInResult].join(', ') : `none`, resultWord: resultWord, boundNote: boundNote });
// Log the assignment for verification
console.log(`Assignment:`, assignment, '| Active clauses:', freeCount,
'| True clauses:', trueCount, '| False clauses:', falseCount);
});
document.getElementById('reset').addEventListener('click', function() {
document.getElementById('result-area').classList.add('hidden');
});
Comments
Loading comments...