Skip to content

Instantly share code, notes, and snippets.

@laughinghan

laughinghan/SAT_visualization.js

Created September 8, 2021 02:19
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save laughinghan/5a749bbc60df093389597a7b7d17708c to your computer and use it in GitHub Desktop.
Save laughinghan/5a749bbc60df093389597a7b7d17708c to your computer and use it in GitHub Desktop.
Download ZIP
Raw
SAT_visualization.js
// 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')
}
}
Raw
SAT_visualizations.html
<!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