## backtrack.js | |
---|---|

This is an extremely simple implementation of the 'backtracking' algorithm for solving boolean satisfiability problems. It contains no optimizations. | |

The input consists of a boolean expression in Conjunctive Normal Form. This means it looks something like this:
We encode this as an array of strings with a
| |

## solve`variables` is the list of all variables`clauses` is an array of clauses.`model` is a set of variable assignments.
| ```
function solve (variables, clauses, model) {
model = model || {};
``` |

If every clause is satisfiable, return the model which worked. | ```
if (clauses.every(function (c) { return satisfiable(c, model); }))
return model;
``` |

If any clause is | ```
if (clauses.some(function (c) { return satisfiable(c, model) === false; }))
return false;
``` |

Choose a new value to test by simply looping over the possible variables and checking to see if the variable has been given a value yet. | ```
var choice;
for (var i = 0; i < variables.length; i++) {
if (model[variables[i]] === undefined) {
choice = variables[i];
}
}
``` |

If there are no more variables to try, return false. | ` if (!choice) return false;` |

Recurse into two cases. The variable we chose will need to be either true or false for the expression to be satisfied. | ```
return solve(variables, clauses, update(model, choice, true)) ||
solve(variables, clauses, update(model, choice, false));
}
``` |

## updateCopies the model, then sets | ```
function update (model, choice, value) {
var copy = {};
for (var v in model) copy[v] = model[v];
copy[choice] = value;
return copy;
}
``` |

## satisfiableDetermines whether a clause is satisfiable given a certain model. | `function satisfiable (clause, model) {` |

If every variable is false, then the clause is false. | ```
if (clause.every(function (v) { return resolve(v, model) === false; }))
return false;
``` |

If any variable is true, then the clause is true. | ```
if (clause.some(function (v) { return resolve(v, model) === true; }))
return true;
``` |

Otherwise, we don't know what the clause is. | ```
return undefined;
}
``` |

## resolveResolve some variable to its actual value, or undefined. | ```
function resolve (variable, model) {
if (variable[0] == '-') {
var value = model[variable.slice(1)];
return value === undefined? undefined : !value;
} else return model[variable];
}
exports.solve = solve;
exports.update = update;
exports.satisfiable = satisfiable;
exports.resolve = resolve;
``` |