gsat.js

(function() {
  print("Enter the number of restarts");
  retries = readline();

  print("Enter the number of flips");
  flips = readline();

  retries = 10;
  flips = 10;

  formula_4literais = {
    ls : [0, 0, 0, 0, 0, 0],

    clauses : [
      function(env) { return env[0] || env[1] || env[2]; },
      function(env) { return env[0] || !env[1] || env[2]; },
      function(env) { return env[4] || env[2] || !env[3];},
      function(env) { return env[1] || env[2] || env[3]; },
      function(env) { return env[3] || env[2] || env[5]; },
      function(env) { return env[4] || env[1] || !env[0]; },
      function(env) { return env[0] || !env[5] || env[3]; },
      function(env) { return env[2] || env[4] || env[5]; },
    ],

    apply : function() {
      for (var i = 0; i < this.clauses.length; i++) {
        f = this.clauses[i];
        if (!f(this.ls)) return false;
      }

      return true;
    },

    satisfied : function(env) {
      var s = 0;

      for (var i = 0; i < env.length; i++) {
        f = this.clauses[i];
        if (f(env)) s++;
      }

      return s;
    }
  }
  
  function random_bool() {
    var f = Math.random();
    return f >= 0.5;
  }

  function random_int(max) {
    return Math.floor(Math.random()*(max+1));
  }

  function generate_random_attribution(formula) {
    literals = new Array();
    literals.length = formula.ls.length;

    for (var i = 0; i < literals.length; i++) {
      literals[i] = random_bool();
    }

    formula.ls = literals;
  }

  function hillclimb(formula) {
    var currently_sat = formula.satisfied(formula.ls);
    var more_sat = [];
    var max_sat = currently_sat;
    
    for (var i = 0; i < formula.ls.length; i++) {
      var new_ls = formula.ls.slice(0); // cloning the array
      new_ls[i] = !formula.ls[i]; 

      var sat = formula.satisfied(new_ls);
      if (sat >= currently_sat) {
        more_sat.push({ satisfied: sat, env : new_ls });
        max_set = sat > max_sat ? sat : max_sat;
      }
    }

    more_sat.filter(function(tuple) {
      return tuple.satisfied >= max_sat;
    });
    
    return more_sat;
  }

  function gsat(formula) {
    for (var i = 0; i < retries; i++) {
      generate_random_attribution(formula);
      print("Generating random attr: ", formula.ls);

      for (var j = 0; j < flips; j++) {
        print("Tentando verificar verdade");
        if (formula.apply()) {
          print("Encontrei!");
          return formula.ls;
        } else {
          more_sat = hillclimb(formula);
          var rand_int = random_int(more_sat.length);
          
          var tuple = more_sat[rand_int];
          formula.ls = tuple.env;
        }
      }

      print("Com a atribuicao inicial e o numero flips nao foi possivel encontrar uma solucao, tentar novamente");
    }
  }

  gsat(formula_4literais);

  print("Verdade: ", formula_4literais.ls);

})();