DPLL Algorithm in JavaScript.

An implementation of the Davis-Putnam-Logemann-Loveland (DPLL) algorithm for solving the CNF-SAT problem that runs on Node.js.

This algorithm decides the satisfiability of propositional logic formulae in conjunctive normal form (CNF) - i.e. an AND of ORs.

The dpll source code is available on GitHub, and is released under the MIT license.

Most of this documentation actually comes from wikipedia and is generated by docco.

Disclaimer

This implementation is most definitively not as efficient / complete / advanced / ... (fill in the blanks!) as those entering the SAT competition.

Why JavaScript?

Any application that can be written in JavaScript, will eventually be written in JavaScript (Jeff Atwood).

Tests

This library comes with its unit tests written with mocha. To run them, simply head to the test directory and execute mocha *Test.js.

Quick Start

Let's say we want to solve the following formula:

(a ∨ b) ∧ (¬b ∨ c ∨ ¬d) ∧ (d ∨ ¬e)

Or in plain english:

(a or b) and (not b or c or not d) and (d or not e)

In other words we want to know the values of a, b, c, d and e that make this formula TRUE.

First, create the CNF formula:

var dpll = require('*PATH_TO_DPLL.js*/dpll');

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

formula.openClause(a).or(b).close()
       .openClauseNot(b).or(c).orNot(d).close()
       .openClause(d).orNot(e).close();

Then, create a solver for this formula:

var solver = new dpll.Solver(formula);

Finally, solve the formula and query the returned valuation to get the thruth value of each variable:

var solution = solver.solve();
console.log(solution.get(a));

Solver#solve() returns undefined if the formula can not be solved.

If the formula is satisfiable, the returned valuation will NOT contain the variables that have been optimized away. For instance if the formula contains the clause (x ∨ ¬x ∨ y) and x appears nowhere in any other clause of the formula, then x is optimized away and therefore its value is irrelevant - i.e. it could be TRUE or FALSE.

More about...

Public API

make CnfFormula available

exports.CnfFormula = require('./CnfFormula');

make Solver available

exports.Solver = require('./Solver');