Skip to content

Commit

Permalink
Updated index.html
Browse files Browse the repository at this point in the history
  • Loading branch information
Cedric Liegeois committed Oct 17, 2013
1 parent e441a8b commit 670e90a
Show file tree
Hide file tree
Showing 3 changed files with 63 additions and 79 deletions.
80 changes: 33 additions & 47 deletions doc/index.html
Original file line number Diff line number Diff line change
@@ -1,5 +1,4 @@
<!DOCTYPE html>

<html>
<head>
<title>DPLL Algorithm in JavaScript.</title>
Expand All @@ -9,25 +8,20 @@
</head>
<body>

<div class="header">
<a class="logo" href="index.html">dpll</a>


<h1>DPLL Algorithm in JavaScript.</h1>




</div>
<div class="header">
<a class="logo" href="index.html">dpll</a>


<h1>DPLL Algorithm in JavaScript.</h1>

<!--div class="container">
<div class="page"-->


</div>

<div class="content">


<div class="content">


<p>An implementation of the Davis-Putnam-Logemann-Loveland (<a href="http://en.wikipedia.org/wiki/DPLL_algorithm">DPLL</a>)
<p>An implementation of the Davis-Putnam-Logemann-Loveland (<a href="http://en.wikipedia.org/wiki/DPLL_algorithm">DPLL</a>)
algorithm
for solving the <a href="http://en.wikipedia.org/wiki/Boolean_satisfiability_problem">CNF-SAT</a> problem that runs on
<a href="http://nodejs.org">Node.js</a>.</p>
Expand All @@ -53,59 +47,51 @@ <h2>Quick Start</h2>
<p>Or in plain english:</p>
<p><em>(a or b) and (not b or c or not d) and (d or not e)</em></p>
<p>In other words we want to know the values of <em>a</em>, <em>b</em>, <em>c</em>, <em>d</em> and <em>e</em> that make this formula <strong>TRUE</strong>.</p>
<p>First, create the <a href="./CnfFormula.html">CNF formula</a>: </p>
<p>First, create the <a href="./CnfFormula.html">CNF formula</a>:</p>
<pre><code>var dpll = require(&#39;*PATH_TO_DPLL.js*/dpll&#39;);

var formula = new dpll.CnfFormula();
var a = {}, b = {}, c = {}, d = {} e = {};
var a = {}, b = {}, c = {}, d = {}, e = {};

formula.openClause(a).or(b).close()
.openClauseNot(b).or(c).orNot(d).close()
.openClause(d).orNot(e).close();</code></pre>
<p>Then, create a <a href="./Solver.html">solver</a> for this formula:</p>
<pre><code>var solver = new dpll.Solver(formula);</code></pre>
<p>Finally, solve the formula and query the returned <a href="./Valuation.html">valuation</a> to get the thruth value of each variable:</p>
<p>Finally, solve the formula and query the returned <a href="./Valuation.html">valuation</a> to get the thruth value of each
variable:</p>
<pre><code>var solution = solver.solve();
console.log(solution.get(a));</code></pre>
<p>If the formula could not be solved <code>Solver#solve()</code> will return <code>undefined</code>.</p>
<p>If the formula has been solved the result will <strong>NOT</strong> contain the variables that have
been optimized away. For instance if the formula contains the <a href="./Clause.html">clause</a> <em>(x &or; &not;x &or; y)</em>
<p><code>Solver#solve()</code> returns <code>undefined</code> if the formula can not be solved.</p>
<p>If the formula is satisfiable, the returned valuation will <strong>NOT</strong> contain the variables that have
been optimized away. For instance if the formula contains the <a href="./Clause.html">clause</a> <em>(x &or; &not;x &or; y)</em>
and <em>x</em> appears nowhere in any other clause of the formula, then <em>x</em> is optimized away and therefore its value is
irrelevant - i.e. it could be <strong>TRUE</strong> or <strong>FALSE</strong>.</p>
<h2>More about...</h2>
<ul>
<li><p>the DPLL algorithm itself: <a href="./Solver.html">Solver.js</a></p>
</li>
<li><p>CNF Formulas: <a href="./CnfFormula.html">CnfFormula.js</a></p>
<li><p>CNF Formula: <a href="./CnfFormula.html">CnfFormula.js</a></p>
</li>
<li><p>Valuations: <a href="./Valuation.html">Valuation.js</a></p>
<li><p>Valuation: <a href="./Valuation.html">Valuation.js</a></p>
</li>
<li><p>Clauses: <a href="./Clause.html">Clause.js</a></p>
<li><p>Clause: <a href="./Clause.html">Clause.js</a></p>
</li>
</ul>
<h2>Public API</h2>
<p>make <code>CnfFormula</code> available</p>


<div class='highlight'><pre>(<span class="keyword">function</span>() {</pre></div>



<p>make <code>CnfFormula</code> available</p>


<div class='highlight'><pre> exports.CnfFormula = require(<span class="string">'./CnfFormula'</span>);</pre></div>



<p>make <code>Solver</code> available</p>

<div class='highlight'><pre>exports.CnfFormula = require(<span class="string">'./CnfFormula'</span>);</pre></div>



<p>make <code>Solver</code> available</p>


<div class='highlight'><pre> exports.Solver = require(<span class="string">'./Solver'</span>);
})();</pre></div>


</div>
<!--/div>
</div-->

<div class='highlight'><pre>exports.Solver = require(<span class="string">'./Solver'</span>);</pre></div>


</div>
</body>
</html>
31 changes: 15 additions & 16 deletions doc/style.css
Original file line number Diff line number Diff line change
Expand Up @@ -116,21 +116,20 @@ pre, tt, code {
padding-bottom: 20px;
border-bottom: 1px solid #cccccc;
-moz-box-shadow: 0 4px 2px -2px rgba(0,0,0,0.1);
-webkit-box-shadow: 0 4px 2px -2px rgba(0,0,0,0.1);
box-shadow: 0 4px 2px -2px rgba(0,0,0,0.1);
-webkit-box-shadow: 0 4px 2px -2px rgba(0,0,0,0.1);
box-shadow: 0 4px 2px -2px rgba(0,0,0,0.1);
background: white;
width: 100%;
padding: 20px 0;
opacity: 0.95;
padding: 20px 0;
}

.header h1 {
float: left;
float: left;
display: inline;
margin: 0;
padding: 0;
font-size: 44px;
line-height: 100px;
margin: 0;
padding: 0;
font-size: 44px;
line-height: 100px;
}

.logo {
Expand All @@ -147,8 +146,8 @@ pre, tt, code {
transition-property: background;
transition-duration: 0.5s;
transition-timing-function: ease-in-out;
margin: 0px 2% 0px 5%;
padding: 0;
margin: 0px 2% 0px 5%;
padding: 0;
}

.logo:hover {
Expand Down Expand Up @@ -196,21 +195,21 @@ span.lineno {
/* Original theme - http://noahfrederick.com/vim-color-scheme-hemisu/ */
/* http://jmblog.github.com/color-themes-for-google-code-highlightjs */
.hemisu-comment, pre .comment, pre .xml .doctype, pre .html .doctype {
color: #999999;
color: #999999;
}

.hemisu-accent1, pre .number, pre .ruby .keyword {
color: #538192;
color: #538192;
}

.hemisu-accent2, pre .string, pre .regexp, pre .xml .value, pre .html .value {
color: #739200;
color: #739200;
}

.hemisu-accent3, pre .keyword, pre .title, pre .constant, pre .xml .tag, pre .html .tag, pre .css .rules .attribute {
color: #ff0055;
color: #ff0055;
}

.hemisu-accent4 {
color: #503d15;
color: #503d15;
}
31 changes: 15 additions & 16 deletions resources/style.css
Original file line number Diff line number Diff line change
Expand Up @@ -116,21 +116,20 @@ pre, tt, code {
padding-bottom: 20px;
border-bottom: 1px solid #cccccc;
-moz-box-shadow: 0 4px 2px -2px rgba(0,0,0,0.1);
-webkit-box-shadow: 0 4px 2px -2px rgba(0,0,0,0.1);
box-shadow: 0 4px 2px -2px rgba(0,0,0,0.1);
-webkit-box-shadow: 0 4px 2px -2px rgba(0,0,0,0.1);
box-shadow: 0 4px 2px -2px rgba(0,0,0,0.1);
background: white;
width: 100%;
padding: 20px 0;
opacity: 0.95;
padding: 20px 0;
}

.header h1 {
float: left;
float: left;
display: inline;
margin: 0;
padding: 0;
font-size: 44px;
line-height: 100px;
margin: 0;
padding: 0;
font-size: 44px;
line-height: 100px;
}

.logo {
Expand All @@ -147,8 +146,8 @@ pre, tt, code {
transition-property: background;
transition-duration: 0.5s;
transition-timing-function: ease-in-out;
margin: 0px 2% 0px 5%;
padding: 0;
margin: 0px 2% 0px 5%;
padding: 0;
}

.logo:hover {
Expand Down Expand Up @@ -196,21 +195,21 @@ span.lineno {
/* Original theme - http://noahfrederick.com/vim-color-scheme-hemisu/ */
/* http://jmblog.github.com/color-themes-for-google-code-highlightjs */
.hemisu-comment, pre .comment, pre .xml .doctype, pre .html .doctype {
color: #999999;
color: #999999;
}

.hemisu-accent1, pre .number, pre .ruby .keyword {
color: #538192;
color: #538192;
}

.hemisu-accent2, pre .string, pre .regexp, pre .xml .value, pre .html .value {
color: #739200;
color: #739200;
}

.hemisu-accent3, pre .keyword, pre .title, pre .constant, pre .xml .tag, pre .html .tag, pre .css .rules .attribute {
color: #ff0055;
color: #ff0055;
}

.hemisu-accent4 {
color: #503d15;
color: #503d15;
}

0 comments on commit 670e90a

Please sign in to comment.