This is a simple backtracking SAT solver written in javascript. I wrote it partially because I needed a SAT solver and partially because I was unable to find a simple example of such an algorithm online.
It has no dependencies and it is written in clean ECMAScript 5. It expects input in Conjunctive Normal Form and will output a model which satisfies the given set of clauses.
You can install it like this:
$ npm i backtrack
and use it like this
var solve = require('backtrack').solve;
var clauses = [
['blue', 'green', '-yellow'],
['-blue', '-green', 'yellow'],
['pink', 'purple', 'green', 'blue', '-yellow']
];
var variables = ['blue', 'green', 'yellow', 'pink', 'purple'];
var model = solve(variables, clauses);
// model => { purple: true, pink: true, yellow: true, green: true }
Read the annotated source!
Tests are written in mocha
$ npm test
You can also pass in a model and the solver will inform you if the expression is satisfiable under the assumptions you have given it:
var solvable = solve(variables, clauses, {blue: true, yellow: false, green: true});
// solvable => false
Since the second clause is now unsolvable, the entire expression is unsolvable.
MIT