code: 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 **exactly** false, return `false`; this model will not
    // work.
    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];
        break;
      }
    }
  
    // 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));
  }
docs: ### solve  * `variables` is the list of all variables * `clauses` is an array of clauses. * `model` is a set of variable assignments.