simple backtracking sat solver in javascript
JavaScript
Switch branches/tags
Nothing to show
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
.gitignore
.travis.yml
LICENSE
README.md
backtrack.js
example.js
expression.js
package.json
test.js

README.md

backtrack

build status

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.

License

MIT