Created
September 8, 2021 02:19
-
-
Save laughinghan/5a749bbc60df093389597a7b7d17708c to your computer and use it in GitHub Desktop.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
// https://jsbin.com/xirefor/edit?js,output | |
var paper = Raphael("paper", 600, 600) | |
var n = 7 // number of boolean variables | |
var C1 = function(x1, x2, x3, x4, x5, x6, x7) { | |
return !x2 || !x3 || !x4 || x5 | |
} | |
var C2 = function(x1, x2, x3, x4, x5, x6, x7) { | |
return !x1 || !x5 || x6 | |
} | |
var C3 = function(x1, x2, x3, x4, x5, x6, x7) { | |
return !x5 || x7 | |
} | |
var C4 = function(x1, x2, x3, x4, x5, x6, x7) { | |
return !x1 || !x6 || !x7 | |
} | |
var C5 = function(x1, x2, x3, x4, x5, x6, x7) { | |
return !x1 || !x2 || x5 | |
} | |
var C6 = function(x1, x2, x3, x4, x5, x6, x7) { | |
return !x1 || !x3 || x5 | |
} | |
var C7 = function(x1, x2, x3, x4, x5, x6, x7) { | |
return !x1 || !x4 || x5 | |
} | |
var C8 = function(x1, x2, x3, x4, x5, x6, x7) { | |
return !x1 || x2 || x3 || x4 || x5 || !x6 | |
} | |
var L1 = function(x1, x2, x3, x4, x5, x6, x7) { | |
return !x1 || !x5 | |
} | |
function evalClause(clause, id) { | |
return clause( | |
!((id >> 6) & 1), | |
!((id >> 5) & 1), | |
!((id >> 4) & 1), | |
!((id >> 3) & 1), | |
!((id >> 2) & 1), | |
!((id >> 1) & 1), | |
!(id & 1)) | |
} | |
function evalClauses(id) { | |
if (C1checked.checked && !evalClause(C1, id)) return false | |
if (C2checked.checked && !evalClause(C2, id)) return false | |
if (C3checked.checked && !evalClause(C3, id)) return false | |
if (C4checked.checked && !evalClause(C4, id)) return false | |
if (C5checked.checked && !evalClause(C5, id)) return false | |
if (C6checked.checked && !evalClause(C6, id)) return false | |
if (C7checked.checked && !evalClause(C7, id)) return false | |
if (C8checked.checked && !evalClause(C8, id)) return false | |
if (L1checked.checked && !evalClause(L1, id)) return false | |
return true | |
} | |
all_none.onclick = function() { | |
var count = 0 | |
var checkboxes = clauses.getElementsByTagName('input') | |
for (var checkbox of checkboxes) { | |
if (checkbox.checked) count += 1 | |
} | |
if (count === 0) { | |
for (var checkbox of checkboxes) { | |
checkbox.checked = true | |
} | |
} else { | |
for (var checkbox of checkboxes) { | |
checkbox.checked = false | |
} | |
} | |
} | |
clauses.onclick = redrawDots | |
var varSpans = [] | |
for (let x_i = 1; x_i <= n; x_i += 1) { | |
var span = document.createElement('span') | |
span.innerHTML = `<i>x</i><sub>${x_i}</sub>` | |
vars.appendChild(span) | |
if (x_i < n) { | |
vars.appendChild(document.createTextNode(', ')) | |
} | |
span.onmouseenter = function() { | |
drawVarStripes(x_i) | |
} | |
span.onmouseleave = function() { | |
redrawDots() | |
} | |
varSpans.push(span) | |
} | |
var dots = [] | |
for (var i = 0; i < Math.pow(2, Math.floor(n/2)); i += 1) { | |
for (var j = 0; j < Math.pow(2, Math.ceil(n/2)); j += 1) { | |
let id = i*Math.pow(2, Math.ceil(n/2)) + j | |
var dot = paper.circle(18 + j*24, 12 + i*24, 8).attr({ | |
fill: evalClauses(id) ? 'darkgray' : 'white', | |
stroke: '#000', | |
'stroke-width': 1, | |
}) | |
.mouseover(function() { | |
for (var i = 0; i < varSpans.length; i += 1) { | |
varSpans[i].style.background = (id >> (n-1-i)) & 1 ? '': 'lime' | |
} | |
}) | |
.mouseout(function() { | |
for (var span of varSpans) span.style.background = '' | |
}) | |
dots.push(dot) | |
} | |
} | |
function redrawDots() { | |
for (var id = 0; id < dots.length; id += 1) { | |
dots[id].attr('fill', evalClauses(id) ? 'darkgray' : 'white') | |
} | |
} | |
function drawVarStripes(x_i) { | |
for (var id = 0; id < dots.length; id += 1) { | |
dots[id].attr('fill', | |
!((id >> (n-x_i)) & 1) ? 'lime' : | |
evalClauses(id) ? 'darkgray' : 'white') | |
} | |
} |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
<!DOCTYPE html> | |
<html> | |
<head> | |
<meta charset="utf-8"> | |
<meta name="viewport" content="width=device-width"> | |
<title>JS Bin</title> | |
<script src="https://cdnjs.cloudflare.com/ajax/libs/raphael/2.1.0/raphael-min.js"></script> | |
</head> | |
<body> | |
<p>The space of solutions to the example in <a href="https://cse442-17f.github.io/Conflict-Driven-Clause-Learning/">this CDCL tutorial</a>:</p> | |
<p id="vars"></p> | |
<div id="clauses"> | |
<p><label><input type="checkbox" checked id="C1checked"> <i>C</i><sub>1</sub> = ¬ <i>x</i><sub>2</sub> ∨ ¬ <i>x</i><sub>3</sub> ∨ ¬ <i>x</i><sub>4</sub> ∨ <i>x</i><sub>5</sub></p> | |
<p><label><input type="checkbox" checked id="C2checked"> <i>C</i><sub>2</sub> = ¬ <i>x</i><sub>1</sub> ∨ ¬ <i>x</i><sub>5</sub> ∨ <i>x</i><sub>6</sub></p> | |
<p><label><input type="checkbox" checked id="C3checked"> <i>C</i><sub>3</sub> = ¬ <i>x</i><sub>5</sub> ∨ <i>x</i><sub>7</sub></p> | |
<p><label><input type="checkbox" checked id="C4checked"> <i>C</i><sub>4</sub> = ¬ <i>x</i><sub>1</sub> ∨ ¬ <i>x</i><sub>6</sub> ∨ ¬ <i>x</i><sub>7</sub></p> | |
<p><label><input type="checkbox" checked id="C5checked"> <i>C</i><sub>5</sub> = ¬ <i>x</i><sub>1</sub> ∨ ¬ <i>x</i><sub>2</sub> ∨ <i>x</i><sub>5</sub></p> | |
<p><label><input type="checkbox" checked id="C6checked"> <i>C</i><sub>6</sub> = ¬ <i>x</i><sub>1</sub> ∨ ¬ <i>x</i><sub>3</sub> ∨ <i>x</i><sub>5</sub></p> | |
<p><label><input type="checkbox" checked id="C7checked"> <i>C</i><sub>7</sub> = ¬ <i>x</i><sub>1</sub> ∨ ¬ <i>x</i><sub>4</sub> ∨ <i>x</i><sub>5</sub></p> | |
<p><label><input type="checkbox" checked id="C8checked"> <i>C</i><sub>8</sub> = ¬ <i>x</i><sub>1</sub> ∨ <i>x</i><sub>2</sub> ∨ <i>x</i><sub>3</sub> ∨ <i>x</i><sub>4</sub> ∨ <i>x</i><sub>5</sub> ∨ ¬ <i>x</i><sub>6</sub></p> | |
<p><label><input type="checkbox" checked id="L1checked"> <i>L</i><sub>1</sub> = ¬ <i>x</i><sub>1</sub> ∨ ¬ <i>x</i><sub>5</sub></p> | |
<p><button id="all_none">All/None</button> | |
</div> | |
<div id="paper"></div> | |
</body> | |
</html> |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment