einstein-solver/einwork.js

 function EV() {
     this.__e = {};
 }
 EV.prototype.__e = {};
 EV.prototype.emit = function(n) {
     var that = this;
     var args = [].slice.apply(arguments, [1]);
     (this.__e[n] || []).map(function(lis) {
         lis.map(function(fn) {
             fn.apply(that, args)
         })
     })
     return this;
 }
 EV.prototype.on = function(n) {
     var args = [].slice.apply(arguments, [1]);
     this.__e[n] = this.__e[n] || [];
     this.__e[n].push(args);
     return this;
 }

 function inherits(ctor, superCtor) {
     var Obj = function() {};
     Obj.prototype = superCtor.prototype;
     ctor.prototype = new Obj
 }


 function permutates(xs) {
     var ret = [];

     for (var i = 0; i < xs.length; i = i + 1) {
         var rest = permutates(xs.slice(0, i).concat(xs.slice(i + 1)));

         if (!rest.length) {
             ret.push([xs[i]])
         } else {
             for (var j = 0; j < rest.length; j = j + 1) {
                 ret.push([xs[i]].concat(rest[j]))
             }
         }
     }
     return ret;
 }


 function mo() {
     this.variabler = {};
     this.tabel = {};
     this.tableHead = [];
     this.tableName = "";
     this.regler = [];
     this._internal_step_counter = 0;
     this.rmat = [];
     this.funcs = {};
     this.rulas = [];
 }
 inherits(mo, EV)

 mo.prototype.addVariabelSet = function(navn, arr) {
     this.variabler[navn] = arr;
     return this;
 }
 mo.prototype.addVariableTable = function(navn, arr) {
     this.tableHead = arr;
     this.tableName = navn;
     return this;
 }
 mo.prototype.addFunction = function(name, func) {
     this.funcs[name] = func;
     return this;
 }
 mo.prototype.addClause = function() {
     var args = Array.prototype.slice.apply(arguments, []);
     while (args.length) {
         var arg = args.shift();

         var props = Object.keys(arg);
         var propid1, propid2;

         if (this.variabler[props[0]]) {
             propid1 = Object.keys(this.variabler).indexOf(props[0]);
         }
         if (this.variabler[props[1]]) {
             propid2 = Object.keys(this.variabler).indexOf(props[1]);
         } else {}
         var arr = []
         if (propid1 > -1 && propid2 > -1) {
             val1 = this.variabler[props[0]].indexOf(arg[props[0]])
             val2 = this.variabler[props[1]].indexOf(arg[props[1]])
             arr = ["check", propid1, propid2, val1, val2, [props[0], arg[props[0]], props[1], arg[props[1]]].join(" ")];
         } else {
             var lookfor = props[props.length - 1];
             if (this.funcs[lookfor]) {
                 arr = this.funcs[lookfor].apply(this, [arg])
             }
         }
     }
     this.rulas.push(arr);
     return this;
 }

 mo.prototype.build = function(tabl) {
     var r = [];
     var arr = [];
     var pertable = []

     for (var navn in this.variabler) {
         pertable.push(permutates((this.variabler[navn]).map(function(a, i) {
             return i
         })));
     }

     return pertable;
 }

 mo.prototype.checkn = function(prop1, prop2, val1, val2) {

     return this.current[this.sos[prop1]][val1] == val2

 }

 mo.prototype.check = function(prop1, prop2, val1, val2) {
     var i;
     //   console.log(prop1,this.sos[prop1], prop2, this.current[this.sos[prop1]],this.current[this.sos[prop2]],val1,val2)
     for (i = 0; i < 5; i++) {
         if (this.current[this.sos[prop1]][i] == val1) {
             //         console.log("II,",i,this.current[this.sos[prop1]][i],"=",val1,"&", this.current[this.sos[prop2]][i],"=",val2 );
             var p;
             p = (this.current[this.sos[prop2]][i] == val2)
             return p;
         }
     }
     return false;
 }
 mo.prototype.checkLeft = function(prop1, prop2, val1, val2) {
     var i;
     for (i = 0; i < 4; i++) {
         if (this.current[this.sos[prop1]][i] == val1) {
             var p;
             p = (this.current[this.sos[prop2]][i + 1] == val2)
             return p;
         }
     }
     return false;
 }
 mo.prototype.checkRight = function(prop1, prop2, val1, val2) {
     var i;
     for (i = 1; i < 5; i++) {
         if (this.current[this.sos[prop1]][i] == val1) {
             var p;
             p = (this.current[this.sos[prop2]][i - 1] == val2)
             return p;
         }
     }
     return false;
 }

 mo.prototype.checkBoth = function(prop1, prop2, val1, val2) {

     return this.checkLeft(prop1, prop2, val1, val2) || this.checkRight(prop1, prop2, val1, val2)
 }

 function intersection() {
     var result = [];
     var lists;

     if (arguments.length === 1) {
         lists = arguments[0];
     } else {
         lists = arguments;
     }

     for (var i = 0; i < lists.length; i++) {
         var currentList = lists[i];
         for (var y = 0; y < currentList.length; y++) {
             var currentValue = currentList[y];
             if (result.indexOf(currentValue) === -1) {
                 var existsInAll = true;
                 for (var x = 0; x < lists.length; x++) {
                     if (lists[x].indexOf(currentValue) === -1) {
                         existsInAll = false;
                         break;
                     }
                 }
                 if (existsInAll) {
                     result.push(currentValue);
                 }
             }
         }
     }
     return result;
 }
 mo.prototype.solve = function() {
     var self = this;
     self.current = this.build("House").shift();
     var sa = Object.keys(this.variabler);
     self.sos = sa.map(function(a) {
         return 0; //self.current.length - 1; //Math.floor(Math.random()*self.current.length-1);
     })
     self.subspace = self.current.length;
     self.varspace = sa.length;
     self.space = Math.pow(self.subspace, self.varspace - 1);


     var iteration = 0;
     var maxi = 0;
     var ioa = -1;

     var soso = [];

     var sat = false;


     self.rulas = self.rulas; //slice(0, 9);


     /*     self.rulas.sort(function(a, b) {
         return a[1] > b[1] ? -1 : a[1] < b[1] ? 1 : a[2] > b[2] ? 1 : a[2] < b[2] ? -1 : 0
     })
*/
     //    console.log(self.rulas);


     //  return false;


     // først find variabler som bruges i samme opslag.
     var tas = {}
     var firsta = [];
     self.rulas.map(function(ru) {
        console.log(ru);
         if (ru[1] == ru[2]) {
             firsta.push(ru);
         }
     })

     self.sos = self.sos.map(function(a) {
         return 0
     })

     var osa = -1
     console.log(firsta);

     var cands = [];

 
     for (var x = 0; x < firsta.length; x++) {
         self.sos = self.sos.map(function(a) {
             return 0
         })

         var t = firsta[x];
         var ca = [];
         for (var i = 0; i < self.subspace; i++) {
             var ff = false;
             self.sos[t[1]] = i
             console.log(self.sos);
             ff = self[t.slice(0, 1)[0]].apply(self, t.slice(1))
             if (ff) {
                 ca.push(i);
             }
         }
         cands.push([t[1], ca]);
     }

     console.log(cands);

     //   var inta=intersection.apply(this,cands.map(function(a){ return a[1]}));
     self.sos = self.sos.map(function(a) {
         return 0
     })


     var cc = cands.length;
     var ticks = [0, 0, 0, 0, 0];
     var ic = 0;
     var iomax = self.rulas.length;
     var ioa = 0;

     for (var i0 = 0; i0 < cands[0][1].length; i0++) {
         if (cands[1]) {

             for (var i1 = 0; i1 < cands[1][1].length; i1++) {
                 if (cands[2]) {

                     for (var i2 = 0; i2 < cands[2][1].length; i2++) {
                         if (cands[3]) {

                         } else {
                             var st = [0, 1, 2, 3, 4]
                             self.sos[cands[0][0]] = cands[0][1][i0]
                             self.sos[cands[1][0]] = cands[1][1][i1]
                             self.sos[cands[2][0]] = cands[2][1][i2]

                             st.splice(st.indexOf(cands[0][0]), 1);
                             st.splice(st.indexOf(cands[1][0]), 1);
                             st.splice(st.indexOf(cands[2][0]), 1);

                             for (var i3 = 0; i3 < 120; i3++) {

                                 for (var i4 = 0; i4 < 120; i4++) {
                                     ic++

                                     self.sos[st[0]] = i3
                                     self.sos[st[1]] = i4


                                     var io = 0;
                                     var ff = true;
                                     while (io < iomax && ff) {
                                         ff = false;
                                         var t = self.rulas[io];
                                         ff = self[t.slice(0, 1)[0]].apply(self, t.slice(1))
                                         if (ff) {
                                             io++;
                                         }
                                     }

                                     if (io > ioa) {
                                         // soso.push([].concat(self.sos));
                                         ioa = io;
                                         var tt = self.rulas.map(function(t) {
                                             return [self[t.slice(0, 1)[0]].apply(self, t.slice(1))].concat(t);
                                         })
                                         console.log(ic, io, ioa, iomax, self.sos.join(" "), tt.map(function(a) {
                                             return a.join(" ")
                                         }));
                                     }

                                     if(ioa >= iomax){
                                        return self.sos;

                                     }

                                     if(ic % 1000000 === 0){

                                    console.log("X", ic, io,ioa,iomax, self.sos[cands[0][0]], self.sos[cands[1][0]], self.sos[cands[2][0]], i3, i4);
                                     }

                                 }


                             }




                         }
                     }
                 } else {
                     console.log(cands[0][1][i1], cands[1][1][i2])

                 }

             }


         }

     }



     return false;

     //     console.log("II",inta);




     /* for (var i = 0; i < self.subspace; i++) {
         self.sos[0] = i;
         var mio = 0;
         var ff = true;
         var iomax = 1; // firsta.length;
         while (mio < iomax && ff) {
             var t = firsta[mio];
             ff = self[t.slice(0, 1)[0]].apply(self, t.slice(1))
             if (ff) {
                 mio++;
             }
         }
         if (mio > 0) {
             cands.push(i);
         } else {}
     }
     self.sos[0] = 0;
*/


     //cands = [105,81]


     var iomax = self.rulas.length;

     while (!sat && cands.length > 0) {
         var cand1 = cands.shift();
         self.sos[0] = cand1;
         iteration = 0;

         while (!sat && iteration < self.space) {
             var io = 0;
             var ff = true;
             while (io < iomax && ff) {
                 var t = self.rulas[io];
                 ff = self[t.slice(0, 1)[0]].apply(self, t.slice(1))
                 if (ff) {
                     io++;
                 }
             }
             if (io > ioa) {
                 soso.push([].concat(self.sos));
                 ioa = io;
                 var tt = self.rulas.map(function(t) {
                     return [self[t.slice(0, 1)[0]].apply(self, t.slice(1))].concat(t);
                 })
                 console.log(iteration, io, ioa, iomax, self.sos.join(" "), tt.map(function(a) {
                     return a.join(" ")
                 }));
             }
             if (io >= iomax) {
                 sat = true;
                 //            console.log((iteration).toFixed(0) + " ", ioa, "::", self.sos.join(" "), soso.join(" | "));
             } else {
                 self.sos[1] = iteration % self.subspace;
                 self.sos[2] = Math.floor(iteration / self.subspace) % self.subspace;
                 self.sos[3] = Math.floor(iteration / (self.subspace * self.subspace)) % self.subspace;
                 self.sos[4] = Math.floor(iteration / (self.subspace * self.subspace * self.subspace)) % self.subspace;
                 //             self.sos[0] = Math.floor(iteration / (self.subspace * self.subspace * self.subspace * self.subspace)) % self.subspace;
             }
             if (iteration % 10000000 === 0) {
                 self.emit("status", (iteration / (self.space / 100)).toFixed(2), ioa + ":: " + cands.length + ":: " + self.sos.join(" "))
             }

             // console.log(iteration, self.sos.join(" "));
             iteration++;
         }



     }






     /*     while (!sat && iteration < self.space) {

         var io = 0;
         var ff = true;
         while (io < iomax && ff) {
             var t = self.rulas[io];
             ff = self[t.slice(0, 1)[0]].apply(self, t.slice(1))
             if (ff) {
                 io++;
             }
         }
         if (io > ioa) {
             soso.push([].concat(self.sos));
             ioa = io;
             var tt = self.rulas.map(function(t) {
                 return [self[t.slice(0, 1)[0]].apply(self, t.slice(1))].concat(t);
             })
             console.log(iteration, io, ioa, iomax, self.sos.join(" "), tt.map(function(a) {
                 return a.join(" ")
             }));
         }
         if (io >= iomax) {
             sat = true;
             //            console.log((iteration).toFixed(0) + " ", ioa, "::", self.sos.join(" "), soso.join(" | "));
         } else {
             self.sos[4] = iteration % self.subspace;
             self.sos[1] = Math.floor(iteration / self.subspace) % self.subspace;
             self.sos[2] = Math.floor(iteration / (self.subspace * self.subspace)) % self.subspace;
             self.sos[3] = Math.floor(iteration / (self.subspace * self.subspace * self.subspace)) % self.subspace;
             self.sos[0] = Math.floor(iteration / (self.subspace * self.subspace * self.subspace * self.subspace)) % self.subspace;
         }
         if (iteration % 10000000 === 0) {
             self.emit("status", (iteration / (self.space / 100)).toFixed(2), self.sos.join(" "))
         }
         iteration++;
     }*/

     if (sat) {
         console.log("SOLUTION FOUND");
     }

     var tt = self.rulas.map(function(t) {
         return [self[t.slice(0, 1)[0]].apply(self, t.slice(1))].concat(t);
     })
     console.log(iteration, self.sos.join(" "), tt.map(function(a) {
         return a.join(" ")
     }));
     self.printit()


 }


 mo.prototype.printit = function(vals) {
     var self = this;
     var vals = vals || self.sos;
     var lpad = function(s, l) {
         while (s.length < l) {
             s = " " + s
         };
         return s;
     }
     var rpad = function(s, l) {
         while (s.length < l) {
             s = s + " "
         };
         return s;
     }

     var s = [];
     s.push([" ", 1, 2, 3, 4, 5].map(function(a) {
         return lpad("" + a, 12)
     }).join(" "));


     Object.keys(self.variabler).map(function(k, ia) {

         s.push([k, 0, 1, 2, 3, 4].map(function(a, io) {
             return a == k ? rpad(k + ":" + vals[ia], 20) : lpad("" + self.variabler[k][self.current[vals[ia]][a]], 12)
         }).join(" "))

         //            s.push( )
     })
     console.log(s.join("\n") + "\n")
 }

 mo.prototype.stats = function() {
     console.log("steps ", this._internal_step_counter)
     console.log(this);
 }
 

 var t = new mo()
     .addVariabelSet("Nationality", [ "Dane","Norwegian", "Swede", "Englishman", "German"])
     .addVariabelSet("Color", ["Red",  "White", "Yellow", "Blue","Green"])
     .addVariabelSet("Smokes", ["Prince", "Blend", "Dunhill", "BlueMasters", "PallMall"])
     .addVariabelSet("Drinks", ["Water", "Bier", "Milk", "Tea", "Coffee"])
     .addVariabelSet("Animals", ["Dogs", "Birds", "Cats", "Horses", "Fish"])
     .addVariableTable("House", [0, 1, 2, 3, 4])
     .addFunction("Neighbor", function(arg) {
         var prop1 = Object.keys(arg)[0];
         var prop2 = Object.keys(arg[Object.keys(arg)[1]])[0]
         var val1 = arg[prop1];
         var val2 = arg["Neighbor"][prop2];
         var propid1 = Object.keys(this.variabler).indexOf(prop1)
         var propid2 = Object.keys(this.variabler).indexOf(prop2)
         var valid1 = (this.variabler[prop1]).indexOf(val1)
         var valid2 = (this.variabler[prop2]).indexOf(val2)
         return ["checkBoth", propid1, propid2, valid1, valid2, [prop1, val1, "Besides", prop2, val2].join(" ")]
     })
     .addFunction("Neighbor_Before", function(arg) {
         var prop1 = Object.keys(arg)[0];
         var prop2 = Object.keys(arg[Object.keys(arg)[1]])[0]
         var val1 = arg[prop1];
         var val2 = arg["Neighbor_Before"][prop2];
         var propid1 = Object.keys(this.variabler).indexOf(prop1)
         var propid2 = Object.keys(this.variabler).indexOf(prop2)
         var valid1 = (this.variabler[prop1]).indexOf(val1)
         var valid2 = (this.variabler[prop2]).indexOf(val2)
         return ["checkLeft", propid1, propid2, valid1, valid2, [prop1, val1, "Before", prop2, val2].join(" ")]
     })
     .addFunction("Neighbor_After", function() {
         var prop1 = Object.keys(arg)[0];
         var prop2 = Object.keys(arg[Object.keys(arg)[1]])[0]
         var val1 = arg[prop1];
         var val2 = arg["Neighbor_After"][prop2];
         var propid1 = Object.keys(this.variabler).indexOf(prop1)
         var propid2 = Object.keys(this.variabler).indexOf(prop2)
         var valid1 = (this.variabler[prop1]).indexOf(val1)
         var valid2 = (this.variabler[prop2]).indexOf(val2)
         return ["checkRight", propid1, propid2, valid1, valid2, [prop1, val1, "After", prop2, val2].join(" ")]
     })
     .addFunction("House", function(arg) {
         var prop1 = Object.keys(arg)[0];
         var prop2 = prop1
         var propid1 = Object.keys(this.variabler).indexOf(prop1)
         var val1 = arg[prop1];
         var val2 = arg["House"];
         var valid1 = (this.variabler[prop1]).indexOf(val1)
         return ['checkn', propid1, propid1, valid1, val2, [prop1, val1, "House", val2].join(" ")]
     })
     .addClause({
         "Nationality": "Norwegian",
         "House": 0
     })
     .addClause({
         "Drinks": "Milk",
         "House": 2
     })
     .addClause({
         "Nationality": "Norwegian",
         "Neighbor": {
             "Color": "Blue"
         }
     })
     .addClause({
         "Nationality": "Englishman",
         "Color": "Red"
     })
     .addClause({
         "Smokes": "Blend",
         "Neighbor": {
             "Drinks": "Water"
         }
     })
     .addClause({
         "Nationality": "Swede",
         "Animals": "Dogs"
     })
     .addClause({
         "Nationality": "Dane",
         "Drinks": "Tea"
     })
     .addClause({
         "Color": "Green",
         "Neighbor_Before": {
             "Color": "White"
         }
     })
     .addClause({
         "Color": "Green",
         "Drinks": "Coffee"
     })
     .addClause({
         "Smokes": "PallMall",
         "Animals": "Birds"
     })
     .addClause({
         "Color": "Yellow",
         "Smokes": "Dunhill"
     })
     .addClause({
         "Nationality": "German",
         "Smokes": "Prince"
     })
     .addClause({
         "Smokes": "Blend",
         "Neighbor": {
             "Animals": "Cats"
         }
     })
     .addClause({
         "Animals": "Horses",
         "Neighbor": {
             "Smokes": "Dunhill"
         }
     })
     .addClause({
         "Smokes": "BlueMasters",
         "Drinks": "Bier"
     })


 /*  .addClause("$House('Nationality','Norwegian')","eq","$House().first")
    .addClause("$House('Drinks','Milk')","eq","$House().mid")
    .addClause("$House('Nationality','Englishman')","eq","$House('Color','Red')")
    .addClause("Math.abs($House('Smokes','Blend') - $House('Drinks','Water'))===1")
   */
 /*.addClause(0,"Norwegian",-1,-1,-1,-1)
    .addClause(2,-1,-1,-1,"Milk",-1)
    .addClause(-1,"Englishman","Red",-1,-1,-1,-1)
    .addClause(-1,"N Norwegian","Blue",-1,-1,-1,-1)

    .addClause("Math.abs($House('Nationality','Norwegian') - $House('Color','Blue'))===1")
    .addClause("Math.abs($House('Smokes','Blend') - $House('Drinks','Water'))===1")
    .addClause("$House('Nationality','Swede')===$House('Animals','Dogs')")
    .addClause("$House('Nationality','Dane')===$House('Drinks','Tea')")
    .addClause("($House('Color','Green')+1)===$House('Color','White')")
    .addClause("$House('Color','Green')===$House('Drinks','Coffee')")
    .addClause("$House('Smokes','PallMall')===$House('Animals','Birds')")
    .addClause("$House('Color','Yellow')===$House('Smokes','Dunhill')")
    .addClause("Math.abs($House('Smokes','Blend')-$House('Animals','Cats'))===1")
    .addClause("$House('Smokes','BlueMasters')===$House('Drinks','Bier')")
    //.addClause("Math.abs($House('Animals','Horses')-$House('Smokes','Dunhill'))===1")
    //.addClause("$House('Nationality','German')===$House('Smokes','Prince')")
*/


 /*
    The Englishman lives in the red house.<br>
    The Swede keeps dogs.<br>
    The Dane drinks tea.<br>
    The green house is just to the left of the white one.<br>
    The owner of the green house drinks coffee.<br>
    The Pall Mall smoker keeps birds.<br>
    The owner of the yellow house smokes Dunhills.<br>
    The man in the center house drinks milk.<br>
    The Norwegian lives in the first house.<br>
    The Blend smoker has a neighbor who keeps cats.<br>
    The man who smokes Blue Masters drinks bier.<br>
    The man who keeps horses lives next to the Dunhill smoker.<br>
    The German smokes Prince.<br>
    The Norwegian lives next to the blue house.<br>
    The Blend smoker has a neighbor who drinks water.<br>
*/


 //console.log(t.randoma("House"));
 //t.stats();



 t.on("status", function(per, found) {

     console.log("PER", per, found);
 })


var result = t.solve();
console.log(t.printit(result));

 /*
var Colors = ["Red", "White", "Yellow", "Blue", "Green"],
    Nationality = ["Norwegian", "Dane", "Swede", "Englishman", "German"],
    Cigarettes = ["Prince", "Blend", "Dunhill", "Blue Masters", "Pall Mall"],
    Drinks = ["Water", "Bier", "Milk", "Tea", "Coffee"],
    Animals = ["Dogs", "Birds", "Cat", "Horses", "Fish"];*/