proplog_min.js

(function(A){function D(q){var k=(new Date).getTime(),k=String(k-u);0===k.length?k="000":1===k.length?k="00"+k:2===k.length&&(k="0"+k);C("<div>"+k+": "+q+"</div>",x)}function C(q,k){var f=document.getElementById(k),b=document.createElement("div");for(b.innerHTML=q;b.firstChild;)f.appendChild(b.firstChild)}var x="process",u=0;A.solve=function(q,k,f){A.clear_output();window.setTimeout(function(){a:{var b=q,j,r,w;u=(new Date).getTime();D("starting to parse");b=proplog_parse.parse(b);j=[];if("number"==
typeof b[0])D("parsed, detected dimacs syntax"),r=b,b=r.shift();else if("error"===b[0]){D("Syntax error: "+b[0]);C("Syntax error: "+b[0],"result");break a}else D("parsed, detected formula syntax"),j=proplog_convert.formula_to_cnf(b),j=proplog_convert.rename_vars_in_clauses(j),b=j[0],r=j[1],j=j[2];D("got "+r.length+" clauses, max var "+b);"dpll_better"==k&&(w=proplog_dpll.dpll(r,b,f,j));"dpll_old"==k?w=proplog_olddpll.olddpll(r,b,f,j):"dpll_naive"==k?w=proplog_naivedpll.naivedpll(r,b,f,j):"truth_table_naive"==
k?w=proplog_searchtable.searchtable(r,b,"leaves",f,j):"truth_table_better"==k&&(w=proplog_searchtable.searchtable(r,b,"nodes",f,j));"resolution_naive"==k?w=proplog_naiveres.naiveres(r,b,f,j):"resolution_better"==k&&(w=proplog_res.resolution(r,b,f,j));D(w[1]);if(!1!==w[0]){if("resolution_naive"==k||"resolution_better"==k){if(b="Clause set is <b>true</b> for some assignment of values to variables.",!0!=w[0]&&0<w[0].length){b+=" A partial suitable assignment is: ";for(r=0;r<w[0].length;r++)b+=w[0][r]+
" "}}else{b="Clause set is <b>true</b> if we assign values to variables as: ";for(r=0;r<w[0].length;r++)b+=w[0][r]+" "}C(b,"result")}else C("Clause set is <b>false</b> for all possible assignments to variables.","result")}},100)};A.build=function(q,k){A.clear_output();window.setTimeout(function(){var f;u=(new Date).getTime();D("starting to parse");q?(f=proplog_parse.parse(q),"error"===f[0]?C("Parse error: "+f[1],"result"):("parse_tree"==k?("number"===typeof f[0]?(D("parsed, detected dimacs syntax"),
f.shift()):D("parsed, detected formula syntax"),f=JSON.stringify(f),f=f.replace(/"/g,"")):"truth_table"==k?("number"===typeof f[0]?D("parsed, detected dimacs syntax"):D("parsed, detected formula syntax"),f=proplog_convert.print_truthtable(f)):"cnf"==k&&("number"===typeof f[0]?(D("parsed, detected dimacs syntax"),f.shift()):(D("detected formula syntax"),f=proplog_convert.formula_to_cnf(f)),f=proplog_convert.parsed_print(f,[])),D("finished"),f="<tt>"+f.replace(/\n/g,"<br>")+"</tt>",C(f,"result"))):
C("No input.","result")},100)};A.clear_output=function(){var q=document.getElementById(x);q.innerHTML="";q=document.getElementById("result");q.innerHTML=""}})(this.proplog_ui={});(function(A){function D(f,b){var j,r,w,b=u(f,b);j=!1;x(f,b,"-")?(j=!0,b++):x(f,b,"~")&&(j=!0,b++);w=C(f,b);if(k(w))return w;r=w[0];b=w[1];j&&(r=["-",r]);for(b=u(f,b);;){j=null;!0===x(f,b,"&")?(j="&",b++):!0===x(f,b,"and")?(j="&",b+=3):!0===x(f,b,"+")?(j="+",b++):!0===x(f,b,"xor")?(j="+",b+=3):!0===x(f,b,"|")?(j="V",b++):!0===x(f,b,"v")?(j="V",b++):!0===x(f,b,"V")?(j="V",b++):!0===x(f,b,"or")?(j="V",b+=3):!0===x(f,b,"->")?(j="->",b+=2):!0===x(f,b,"=>")?(j="->",b+=2):!0===x(f,b,"<->")?(j="<->",b+=3):
!0===x(f,b,"<=>")&&(j="<->",b+=3);if(null===j)break;w=C(f,b);if(k(w))return w;r=[j,r,w[0]];b=w[1];b=u(f,b);if(b>=f.length)break}return[r,b]}function C(f,b){var j,r,w,a,b=u(f,b);a=!1;x(f,b,"-")?(a=!0,b++,b=u(f,b)):x(f,b,"~")&&(a=!0,b++,b=u(f,b));for(w=b;;)if(j=f.charAt(w),r=f.charCodeAt(w),w<f.length&&(48<=r&&57>=r||65<=r&&122>=r))w++;else{if(w>b)return j=f.substring(b,w),a?[["-",j],w]:[j,w];break}if("("===j){b++;w=D(f,b);if(k(w))return w;j=w[0];b=w[1];b=u(f,b);if(")"!==f.charAt(b))return q("right parenthesis missing");
b++;return a?[["-",j],b]:[j,b]}return")"===j?q("extra right parenthesis at "+f.substring(b)):q("unexpected text "+j+" encountered at "+f.substring(b))}function x(f,b,j){return 1===j.length?f.charAt(b)===j?!0:!1:f.substr(b,j.length)===j?!0:!1}function u(f,b){for(var j;b<f.length;)if(j=f.charAt(b)," "===j||"\t"===j||"\n"===j||"\r"===j)b++;else break;return b}function q(f){return["error",f]}function k(f){return"string"!==typeof f&&"error"===f[0]?!0:!1}A.parse=function(f){var b;b=A.parse_dimacs(f);return 0!==
b[0]&&1<b.length&&0<b[1].length?b:b=A.parse_formula(f)};A.parse_tree=function(f){var b,j,f=A.parse(f);if(k(f))return"syntax error: "+f[1];if("number"==typeof f[0]){j=["&"];for(b=1;b<f.length;b++)1<f[b].length?j.push(["V"].concat(f[b])):1===f[b].length&&j.push(f[b][0]);return JSON.stringify(j)}return JSON.stringify(f)};A.parse_dimacs=function(f){var b,j,r,k,a,m,e,c;b=[];c=0;j=f.split("\n");for(k=0;k<j.length;k++)if((r=j[k].trim())&&!(0===r.lastIndexOf("c",0)||0===r.lastIndexOf("p",0))){f=[];r=r.split(" ");
for(a=0;a<r.length;a++)if(m=r[a])if(m=parseInt(m),!isNaN(m)){if(0===m)break;e=m;0>e&&(e*=-1);e>c&&(c=e);f.push(m)}f&&b.push(f)}b.unshift(c);return b};A.parse_formula=function(f){var b,j,r;b=D(f,0);if(k(b))return b;j=b[0];r=b[1];b=u(f,r);return b<f.length?q("remaining text at "+f.substring(r)):j}})(this.proplog_parse={});(function(A){function D(a,m,e){var c,g;c=typeof a;if(a)if("number"===c)e=a,0>a&&(r.push("-"),j++,e=0-a),(c=m[e])&&(e=c),a=String(e),r.push(a),j+=a.length;else if("string"===c)r.push(a),j+=a.length;else if(!(2>a.length))if(c=a[0],"-"===c)r.push("-"),j++,D(a[1],m,e+1);else{0<e&&(r.push("("),j+=1);for(g=1;g<a.length;g++)D(a[g],m,e+1),g<a.length-1&&(r.push(" "+c+" "),j+=c.length+2);0<e&&(r.push(")"),j+=1)}}function C(a,m,e){var c,g,d;for(c=1;c<a.length;c++)g=a[c],d=typeof g,"number"===d||"string"===d?
e[g]?a[c]=e[g]:(b++,e[g]=b,m[b]=g,a[c]=b):C(g,m,e)}function x(a,m){var e,c;e=typeof a;if("number"===e||"string"===e)return m?a:"number"===e?0-a:"string"===e&&0===a.lastIndexOf("-",0)?a.substring(1):["-",a];if(2>a.length)return["error","op must have some arguments"];e=a[0];if("-"===e)return x(a[1],!m);if("&"===e||"V"===e){e=m?[e]:"&"===e?["V"]:["&"];for(c=1;c<a.length;c++)e.push(x(a[c],m));return e}if("->"===e){e=m?["V"]:["&"];for(c=1;c<a.length-1;c++)e.push(x(a[c],!m));e.push(x(a[a.length-1],m));
return e}return"+"===e?3!==a.length?["error","+ must have two arguments"]:e=m?["V",["&",x(a[1],!1),x(a[2],!0)],["&",x(a[1],!0),x(a[2],!1)]]:["V",["&",x(a[1],!0),x(a[2],!0)],["&",x(a[1],!1),x(a[2],!1)]]:"<->"===e?3!==a.length?["error","<-> must have two arguments"]:e=m?["&",["V",x(a[1],!1),x(a[2],!0)],["V",x(a[1],!0),x(a[2],!1)]]:["V",["&",x(a[1],!0),x(a[2],!1)],["&",x(a[1],!1),x(a[2],!0)]]:"error"}function u(a){var m,e,c,g,d;c=typeof a;if("number"===c||"string"===c)return a;m=a[0];if("-"===m)return a;
if("&"===m){m=["&"];for(e=1;e<a.length;e++)if(g=u(a[e]),c=typeof g,"number"===c||"string"===c||"-"===g[0]||"V"===g[0])m.push(g);else for(c=1;c<g.length;c++)m.push(g[c]);return m}if("V"===m){d=["V"];m=[];for(e=1;e<a.length;e++)if(g=u(a[e]),c=typeof g,"number"===c||"string"===c||"-"===g[0])d.push(g);else if("&"===g[0])m.push(g);else for(c=1;c<g.length;c++)d.push(g[c]);if(0===m.length)return d;var l,h;l=[d];d=[];for(a=0;a<m.length;a++){c=m[a];d=[];for(e=1;e<c.length;e++)for(g=0;g<l.length;g++)h=l[g].slice(),
h.push(c[e]),d.push(h);l=d}c=d;m=["&"];for(e=0;e<c.length;e++)m.push(u(c[e]));return m}return["error","op not allowed"]}function q(a,m,e){var c,g,d,l;c=typeof a;if(a){if("number"===c)return e=a,0>a&&(r.push("-"),j++,e=0-a),(c=m[e])&&(e=c),m=String(e),r.push(m),j+=m.length,a;if("string"===c)return r.push(a),j+=a.length,a;if(2>a.length)return null;c=a[0];if("-"===c)return r.push("-"),l=j,j++,["-",l,q(a[1],m,e+1)];d=[c,0];0<e&&(r.push("("),j+=1);for(g=1;g<a.length;g++)d.push(q(a[g],m,e+1)),g<a.length-
1&&(r.push(" "+c+" "),l=j+1,j+=c.length+2);0<e&&(r.push(")"),j+=1);d[1]=l;return d}}function k(a,m,e){var c,g,d,l,h;if("number"===typeof a)return m[a];c=a[0];g=a[1];if("-"===c)return d=k(a[2],m,e+1),h=1===d?0:1,w[g]=f(h,e),h;if("V"===c){h=0;for(c=2;c<a.length;c++)d=k(a[c],m,e+1),1===d&&(h=1);w[g]=f(h,e);return h}if("&"===c){h=1;for(c=2;c<a.length;c++)d=k(a[c],m,e+1),0===d&&(h=0);w[g]=f(h,e);return h}if("->"===c){h=0;for(c=2;c<a.length-1;c++)d=k(a[c],m),0===d&&(h=1);d=k(a[a.length-1],m,e+1);1===d&&
(h=1);w[g]=f(h,e);return h}if("<->"===c){h=1;d=k(a[2],m,e+1);for(c=3;c<a.length;c++)l=k(a[c],m,e+1),d!==l&&(h=0);w[g]=f(h,e);return h}return"+"===c?(d=k(a[2],m,e+1),l=k(a[3],m,e+1),d+=l,h=1===d?1:0,w[g]=f(h,e),h):-1}function f(a,m){return 0<m?String(a):"<b>"+String(a)+"</b>"}var b=0,j=0,r=[],w=[];A.parsed_print=function(a,m){var e;e=typeof a;if(!a)return"";if("number"===e||"string"===e)return String(a);if(1>a.length)return"";if("string"===typeof a[0])return r=[],j=0,D(a,m,0),e=r.join(""),e=e.replace(/\"/g,
"");var c,g,d,l,h,b;r=[];for(e=j=0;e<a.length;e++){g=a[e];1!=g.length&&(r.push("("),j++);for(c=0;c<g.length;c++)d=g[c],h="",b=typeof d,"string"===b?l=String(d):"number"===b?(0>d?(l=0-d,h="-"):l=d,l=m[l]?m[l]:String(l)):"-"===d[0]&&(l=d[1],h="-"),r.push(h+l),j+=h.length+l.length,c<g.length-1&&(r.push(" V "),j+=3);1!=c&&(r.push(")"),j++);e<a.length-1&&(r.push(" & "),j+=3);r.push("\n");j++}e=r.join("");return e=e.replace(/\"/g,"")};A.rename_vars_in_clauses=function(a){var m={},e=[],c,g,d,l,h,b=0;for(c=
0;c<a.length;c++){d=a[c];for(g=0;g<d.length;g++){l=d[g];h=!1;if("string"===typeof l)0===l.lastIndexOf("-",0)&&(l=l.substring(1),h=!0);else if("number"===typeof l)0>l&&(l=0-l,h=!0);else if(2===l.length&&"-"===l[0])l=l[1],h=!0;else return[0,"error: not a clause list",[]];m[l]?l=m[l]:(b++,m[l]=b,e[b]=l,l=b);d[g]=h?0-l:l}}return[b,a,e]};A.rename_vars_in_formula=function(a){var m=[];b=0;if("number"===typeof a||"string"===typeof a)return[1,1,[0,a]];C(a,m,{});return[b,a,m]};A.formula_to_cnf=function(a){var b,
e,c,g,a=x(a,!0);if("error"===a)return a;a=u(a);b=typeof a;if("string"===b||"number"===b||"-"===a[0])return[[a]];if("V"===a[0])return a.shift(),[a];e=[];for(c=1;c<a.length;c++)g=a[c],b=typeof g,"string"===b||"number"===b||"-"===g[0]?e.push([g]):(g.shift(),e.push(g));return e};A.print_truthtable=function(a){var b,e;if(!a)return"";"number"===typeof a[0]?(e="dpll",a.shift(),b=A.rename_vars_in_clauses(a)):(e="formula",b=A.rename_vars_in_formula(a));a=b[0];var c=b[1];b=b[2];var g,d,l,h,f,s,y,v;y=new Int32Array(a+
1);v=[];d=[];r=[];j=0;if("dpll"===e){g="value";for(h=1;h<b.length;h++)b[h]=String(b[h])}else{c=q(c,b,0);g=r.join("");g=g.replace(/\"/g,"");w=[];for(h=0;h<g.length;h++)w.push("&nbsp;")}for(f=1;f<=a;f++)d.push(b[f]);s=d.join(" ")+" | "+g;v.push(s);d="";for(f=0;f<s.length;f++)d+="&ndash;";v.push(d);g=Math.pow(2,a);if(1024<g)a="Table would contain "+g+" rows: our printing limit is 1024 rows.";else{for(h=0;h<g;h++){d=[];for(l=1;l<=a;l++){f=h>>>a-l;f%=2;y[l]=f?1:0;d.push(y[l]);s="";for(f=0;f<b[l].length;f++)s+=
"&nbsp;";d.push(s)}if("dpll"==e){b:{var i=s=f=l=void 0,p=void 0,u=p=void 0;for(l=0;l<c.length;l++){s=c[l];i=!1;for(f=0;f<s.length;f++)if(p=s[f],0>p?(p=0-p,u=0):u=1,y[p]==u){i=!0;break}if(!i){l="0";break b}}l="1"}s=l}else k(c,y,0),s=w.join("");d.push("&#124; ");d.push(s);v.push(d.join(""))}a=v.join("\n")}return a}})(this.proplog_convert={});(function(A){function D(C){var x,u,q,k;if(0>C)return[];if(1==C)return[[1],[-1]];x=D(C-1);q=[];for(k=0;k<x.length;k++)u=x[k].slice(),u.push(C),q.push(u),u=x[k].slice(),u.push(0-C),q.push(u);return q}A.generate_problem=function(C,x){var u,q,k;if(!C)return"";C=parseInt(C);if(isNaN(C))return"";if("all_combinations"===x)u=D(C);else if("small_unsat"===x){u=C;var f;q=[];k=[];for(f=1;f<=u;f++)k.push(f);q.push(k);for(f=1;f<=u;f++)q.push([0-f]);u=q}else if("random_3-sat"===x){u=C;var b,j,r,w;if(2>u)u=[];else{f=
4*u;q=[];for(b=0;b<f;b++){k=[];for(j=0;3>j;j++)r=Math.random(),r=0.5>r?-1:1,w=Math.random(),w=Math.floor(w*u+1),0>k.indexOf(r*w)&&k.push(r*w);q.push(k)}u=q}}else u=[];q="";for(k=0;k<u.length;k++)q=q+u[k].join(" ")+"\n";return q}})(this.proplog_generate={});(function(A){function D(g,d,l,h,b,f,m,j){var i,p;d>e&&(e=d);if(0!==g){if(q){p="assigning var ";for(i=0;i<g;i++)p+=u(j[i])+" ";x(d,p)}a:{var k,n,t,B,z,E,F,H,G,A,J,L;r++;L="";for(i=E=0;i<g;i++)n=j[i],0>n?h[0-n]=-1:h[n]=1;for(;E<g;){i=j[E++];p=0-i;F=0>i?f[p]:m[i];H=F[0];for(i=1;i<=H;i++){t=F[i];G=!0;J=A=0;for(k=2;k<t.length;k++)if(n=t[k],0>n?(B=h[0-n],z=-1):(B=h[n],z=1),0===B){if(0<A){t[0]===p?(n===t[1]&&(n=J),t[0]=n):(n===t[0]&&(n=J),t[1]=n);k=0>n?m[0-n]:f[n];k[0]++;k[k[0]]=t;F[i]=F[H];F[0]--;H--;i--;
G=!1;break}A++;J=n}else if(B===z){G=!1;break}if(G){if(0===A){q&&x(d,"value is false");for(k=0;k<g;k++)n=j[k],0>n?h[0-n]=0:h[n]=0;g=2*Math.pow(r,1.5);for(k=2;k<t.length;k++)n=t[k],0>n?c[0-n]+=g:c[n]+=g;g=!1;break a}a++;j[g]=J;g++;0>J?(t=0-J,z=-1):(t=J,z=1);h[t]=z;q&&(L+=J+" ")}}}q&&(x(d,"value is undetermined"),0<L.length&&x(d,"derived units "+L));if(1===g)g=j[0];else{p=new Int32Array(g);for(i=0;i<g;i++)p[i]=j[i];g=p}}}else q&&x(d,"search called without assigning vars"),g=0;if(!0===g)return C(h),!0;
if(!1===g)return!1;F=c;w++;L=-1E3;E=0;for(i=1;i<h.length;i++)0===h[i]&&(p=F[i],p>=L&&(L=p,E=i));i=E;if(0===i)return C(h),!0;q&&x(d,"splitting variable "+u(i));j[0]=i;if(p=D(1,d+1,l,h,b,f,m,j))return!0;j[0]=0-i;if(p=D(1,d+1,l,h,b,f,m,j))return!0;if("number"===typeof g)0>g?h[0-g]=0:0!==g&&(h[g]=0);else for(i=0;i<g.length;i++)d=g[i],0>d?h[0-d]=0:h[d]=0;return!1}function C(g){var d;for(d=1;d<g.length;d++)0!==g[d]&&j.push(u(d*g[d]))}function x(g,d){var a,h="";if(q&&"console"==k){for(a=0;a<g;a++)h+=" ";
console.log(h+d)}else if(q&&"text"==k){for(a=0;a<g;a++)h+=" ";f.push(h+d)}else if(q&&"html"==k){for(a=0;a<g;a++)h+="&nbsp;";f.push("<div><tt>"+h+"</tt>"+d+"</div>")}}function u(g){var d,a;return g&&b&&0<b.length?(0>g?(d=0-g,a="-"):(d=g,a=""),b.length>d&&b[d]?a+b[d]:String(g)):String(g)}var q=!1,k="text",f=[],b=[],j=[],r=0,w=0,a=0,m=0,e=0,c;A.dpll=function(g,d,l,h){var M,s,y,v;l?(q=!0,k=l):q=!1;b=h?h:!1;e=m=a=w=r=0;f=[];j=[];var l=g,i,d=0;v=[];for(h=0;h<l.length;h++){s=l[h];g=s.length;y=new Int32Array(g+
2);y[0]=0;for(M=y[1]=0;M<g;M++)i=s[M],y[M+2]=i,i=0>i?0-i:i,i>d&&(d=i);v.push(y)}l=[d,v];d=l[0];g=l[1];y=new Int32Array(d+1);l=new Int32Array(d+1);for(v=0;v<=d;v++)l[v]=0;h=new Int32Array(d+1);M=Array(d+1);for(v=0;v<=d;v++)M[v]=[];s=Array(d+1);for(v=0;v<=d;v++)s[v]=[];c=Array(d+1);for(v=0;v<=d;v++)c[v]=1;a:{var p,I,n,t,B,z,E,F;v=g.sort(function(g,d){return g.length-d.length});g=[];for(d=0;d<v.length;d++){i=v[d];z=!1;F=E=0;for(p=2;p<i.length;p++){n=i[p];t=0-n;0>n?(I=0-n,B=-1):(I=n,B=1);if(l[I]===B){z=
!0;break}if(l[I]===0-B)i[p]=0,E++;else{for(I=2;I<p;I++){if(i[I]===t){z=!0;break}i[I]===n&&(i[p]=0,F++)}if(z)break}}if(z)m++;else{p=i.length-(E+F);if(2===p){g=!1;break a}if(3===p){a++;for(I=2;I<i.length;I++)if(0!==i[I]){n=i[I];break}0>n?(I=0-n,B=-1):(I=n,B=1);l[I]=B}else{if(p!==i.length){t=new Int32Array(p);t[0]=i[0];t[1]=i[1];I=0;for(p=2;p<i.length;p++)0!==i[p]&&(t[I]=i[p],I++);i=t}g.push(i)}}}if(q){n="units detected or derived during preprocessing: ";for(d=1;d<l.length;d++)0!==l[d]&&(n+=" "+d);x(0,
n);console.log(n)}}if(!1===g)return q&&f.push("contradiction found during simplification"),[!1,f.join("\r\n")];if(0===g.length)return C(l),q&&f.push("assignment found during simplification"),[j,f.join("\r\n")];n=g;for(g=0;g<n.length;g++){v=n[g];p=v.length;for(d=2;d<p;d++)i=v[d],0>i?(i=0-i,z=-1):z=1,t=l[i],0===t&&(t=h[i],0===t?h[i]=z:t===0-z?h[i]=2:2<=t&&(5>p?t=20:6>p?t=15:(t=10-(p-2),0>t&&(t=1)),h[i]+=t))}d=[];for(g=v=1;g<h.length;g++)t=h[g],2>t?(d.push(g),l[g]=0>t?-1:1,c[g]=0):0!==l[g]?c[g]=0:(c[g]=
h[g],c[g]>v&&(v=c[g]));if(0<d.length){if(q){v="pure vars eliminated: ";for(g=0;g<d.length;g++)v+=u(d[g])+" ";x(0,v)}p=[];for(g=0;g<n.length;g++){v=n[g];t=!1;for(d=2;d<v.length;d++)if(i=v[d],i=0>i?0-i:i,0===c[i]){m++;t=!0;break}t||p.push(v)}n=p}if(q){v="initial variable activities: ";for(g=1;g<c.length;g++)v+=u(g)+":"+c[g]+" ";x(0,v)}g=n;if(0===g.length)return C(l),q&&f.push("assignment found during pure literal elimination"),[j,f.join("\r\n")];n=g;for(d=0;d<n.length;d++){p=n[d];i=0;for(v=2;v<p.length;v++)t=
p[v],z=0>t?s[0-t]:M[t],2>i?(p[i]=t,i++,z.unshift(p)):z.push(0)}for(d=1;d<s.length;d++){z=s[d];for(v=0;v<z.length&&0!==z[v];v++);s[d].unshift(v);z=M[d];for(v=0;v<z.length&&0!==z[v];v++);M[d].unshift(v)}l=D(0,0,g,l,h,M,s,y);h="search finished: unit propagations count is "+r;h+=", units derived count is "+a;h+=", max depth is "+e;f.push(h);return l?[j,f.join("\r\n")]:[!1,f.join("\r\n")]}})(this.proplog_dpll={});(function(A){function D(g,d,a,h,b,f,j,v,i){var p;b>c&&(c=b);if(0!==a){k&&u(b,"assigning var "+q(a)+" to "+h);i[0]=a*h;a:{var a=1,r,n,t,B,z,E,F,A,G,K;w++;K="";for(h=B=0;h<a;h++)n=i[h],0>n?d[0-n]=-1:d[n]=1;for(;B<a;){n=i[B++];z=0>n?j[0-n]:v[n];for(h=0;h<z.length;h++){E=z[h];F=!0;for(r=G=A=0;r<E.length;r++)if(n=E[r],0>n?(t=d[0-n],p=-1):(t=d[n],p=1),0===t){if(0<A){F=!1;break}A++;G=n}else if(t===p){F=!1;break}if(F){if(0===A){k&&u(b,"value is false");for(r=0;r<a;r++)n=i[r],0>n?d[0-n]=0:d[n]=0;a=!1;break a}m++;
i[a]=G;a++;0>G?(r=0-G,p=-1):(r=G,p=1);d[r]=p;k&&(K+=G+" ")}}}k&&(u(b,"value is undetermined"),0<K.length&&u(b,"derived units "+K));if(1===a)a=i[0];else{p=new Int32Array(a);for(h=0;h<a;h++)p[h]=i[h];a=p}}}else k&&u(b,"search called without assigning a var before"),a=0;if(!0===a)return x(d),!0;if(!1===a)return!1;h=C(g,d,f);if(0===h)return x(d),!0;if("number"!==typeof h){e++;h=h[0];0>h?(h=0-h,p=-1):p=1;k&&u(b,"pure variable "+q(h)+", sign "+p);if(D(g,d,h,p,b+1,f,j,v,i))return!0;if("number"===typeof a)0>
a?d[0-a]=0:0!==a&&(d[a]=0);else for(b=0;b<a.length;b++)g=a[b],0>g?d[0-g]=0:d[g]=0;return!1}k&&u(b,"splitting variable "+q(h));k&&u(b,"splitting variable "+q(h));if((p=D(g,d,h,1,b+1,f,j,v,i))||(p=D(g,d,h,-1,b+1,f,j,v,i)))return!0;if("number"===typeof a)0>a?d[0-a]=0:0!==a&&(d[a]=0);else for(b=0;b<a.length;b++)g=a[b],0>g?d[0-g]=0:d[g]=0;return!1}function C(g,d,b){var h,e,c,f,m,i,j,k,n;a++;for(h=0;h<b.length;h++)b[h]=0;for(h=0;h<g.length;h++){j=g[h];m=0;n=k=j.length;for(e=0;e<k;e++)if(c=j[e],0>c?(c=0-
c,i=-1):i=1,f=d[c],f===i){m=1;break}else f===0-i&&n--;if(0===m&&0<n)for(e=0;e<k;e++)c=j[e],0>c?(c=0-c,i=-1):i=1,f=d[c],0===f&&(m=b[c],0===m?b[c]=i:m===0-i?b[c]=2:2<=m&&(3>n?i=20:4>n?i=15:(i=10-n,0>i&&(i=1)),b[c]+=i))}c=i=0;g=[];for(h=1;h<b.length;h++)m=b[h],0!==m&&(2>m&&0===d[h]&&g.push(m*h),m>i&&0===d[h]&&(i=m,c=h));if(0!==g.length)return g;if(0>c)return 0-c;if(0<c)return c;for(h=1;h<d.length;h++)if(0===d[h])return h;return 0}function x(a){var d;for(d=1;d<a.length;d++)0!==a[d]&&r.push(q(d*a[d]))}
function u(a,d){var e,c="";if(k&&"console"==f){for(e=0;e<a;e++)c+=" ";console.log(c+d)}else if(k&&"text"==f){for(e=0;e<a;e++)c+=" ";b.push(c+d)}else if(k&&"html"==f){for(e=0;e<a;e++)c+="&nbsp;";b.push("<div><tt>"+c+"</tt>"+d+"</div>")}}function q(a){var d,b;return a&&j&&0<j.length?(0>a?(d=0-a,b="-"):(d=a,b=""),j.length>d&&j[d]?b+j[d]:String(a)):String(a)}var k=!1,f="text",b=[],j=[],r=[],w=0,a=0,m=0,e=0,c=0;A.olddpll=function(g,d,l,h){var q,s,y,v;l?(k=!0,f=l):k=!1;j=h?h:!1;c=e=m=a=w=0;b=[];r=[];if(!d)for(q=
d=0;q<g.length;q++){h=g[q];for(l=0;l<h.length;l++)s=0>h[l]?0-h[l]:h[l],s>d&&(d=s)}v=new Int32Array(d+1);l=new Int32Array(d+1);for(q=0;q<=d;q++)l[q]=0;h=new Int32Array(d+1);s=Array(d+1);for(q=0;q<=d;q++)s[q]=[];y=Array(d+1);for(q=0;q<=d;q++)y[q]=[];var i,p,u,n,t,x,d=[];for(q=0;q<g.length;q++){u=g[q];for(i=0;i<u.length;i++){n=u[i];t=0-n;x=!1;for(p=0;p<i;p++)if(u[p]===t){x=!0;break}x||(0>n?y[t].push(u):s[n].push(u),d.push(u))}}l=D(d,l,0,0,0,h,s,y,v);h="finished: unit propagations count is "+w;h+=", units derived count is "+
m;h+=", var selections count is "+a;h+=", pure literal count is "+e;h+=", max depth is "+c;b.push(h);return l?[r,b.join("\r\n")]:[!1,b.join("\r\n")]}})(this.proplog_olddpll={});(function(A){function D(a,f,e,c,g){var d;g>w&&(w=g);0!==e?(u&&C(g,"setting var "+x(e)+" to "+c),f[e]=c):u&&C(g,"search called without setting a var before");a:{var l,h,k,s,q,v,i,p,A,n,t;j++;A=[];for(t="";;){p=!0;n=[];for(c=0;c<a.length;c++){s=a[c];for(d=i=v=q=0;d<s.length;d++)if(l=s[d],0>l?(h=0-l,k=-1):(h=l,k=1),h=f[h],h===k){q=1;break}else 0===h&&(v++,i=l);if(1!==q){if(0===v){u&&C(g,"value is false");for(d=0;d<A.length;d++)f[A[d]]=0;c=-1;break a}else 1===v&&(r++,n.push(i));0!==v&&(p=!1)}}if(p){u&&
C(g,"value is true");c=1;break a}if(0===n.length)break;else for(d=0;d<n.length;d++)l=n[d],0>l?(h=0-l,k=-1):(h=l,k=1),f[h]=k,A.push(h),u&&(t+=x(l)+" ")}u&&(C(g,"value is undetermined"),0<A.length&&C(g,"derived units "+t));c=A}if(1===c){for(a=1;a<f.length;a++)0!==f[a]&&b.push(x(a*f[a]));f[e]=0;return!0}if(-1===c)return f[e]=0,!1;d=0;for(e=1;e<f.length;e++)if(0===f[e]){d=e;break}if(0!==d){u&&C(g,"splitting variable "+x(d));if(D(a,f,d,1,g+1)||D(a,f,d,-1,g+1))return!0;for(e=f[d]=0;e<c.length;e++)f[c[e]]=
0;return!1}console.log("Error in the satisfiable_at");show_process("Error in the satisfiable_at")}function C(a,b){var e,c="";if(u&&"console"==q){for(e=0;e<a;e++)c+=" ";console.log(c+b)}else if(u&&"text"==q){for(e=0;e<a;e++)c+=" ";k.push(c+b)}else if(u&&"html"==q){for(e=0;e<a;e++)c+="&nbsp;";k.push("<div><tt>"+c+"</tt>"+b+"</div>")}}function x(a){var b,e;return a&&f&&0<f.length?(0>a?(b=0-a,e="-"):(b=a,e=""),f.length>b&&f[b]?e+f[b]:String(a)):String(a)}var u=!1,q="text",k=[],f=[],b=[],j=0,r=0,w=0;A.naivedpll=
function(a,m,e,c){var g,d;e?(u=!0,q=e):u=!1;f=c?c:!1;w=r=j=0;k=[];b=[];if(!m)for(e=m=0;e<a.length;e++){g=a[e];for(c=0;c<g.length;c++)d=0>g[c]?0-g[c]:g[c],d>m&&(m=d)}c=new Int32Array(m+1);for(e=0;e<=m;e++)c[e]=0;a=D(a,c,0,0,0);m="finished: unit propagations count is "+j;m+=", units derived count is "+r;m+=", max depth is "+w;k.push(m);return a?[b,k.join("\r\n")]:[!1,k.join("\r\n")]}})(this.proplog_naivedpll={});(function(A){function D(a,f,e,c,g){f[e]=c;e===f.length-1&&j++;u&&C(g,"setting var "+x(e)+" to "+c);if("leaves"!==w||e===f.length-1){a:{var d,l,h,k,s,q,v;r++;v=!0;for(c=0;c<a.length;c++){k=a[c];s=0;q=!0;for(d=0;d<k.length;d++)if(l=k[d],h=1,0>l&&(l*=-1,h=-1),l=f[l],l===h){s=1;break}else 0===l&&(q=!1);if(1!==s&&q){u&&C(g,"value is false");c=-1;break a}q||(v=!1)}v?(u&&C(g,"value is true"),c=1):(u&&C(g,"value is undetermined"),c=0)}if(1===c){for(a=1;a<f.length;a++)0!==f[a]&&b.push(x(a*f[a]));f[e]=0;return!0}if(-1===
c)return f[e]=0,!1}if(e<f.length-1){if(D(a,f,e+1,1,g+1)||D(a,f,e+1,-1,g+1))return f[e]=0,!0;f[e]=0;return!1}console.log("Error in the satisfiable_by_table algorithm");show_process("Error in the satisfiable_by_table algorithm")}function C(a,b){var e,c="";if(u&&"console"==q){for(e=0;e<a;e++)c+=" ";console.log(c+b)}else if(u&&"text"==q){for(e=0;e<a;e++)c+=" ";k.push(c+b)}else if(u&&"html"==q){for(e=0;e<a;e++)c+="&nbsp;";k.push("<div><tt>"+c+"</tt>"+b+"</div>")}}function x(a){var b,e;return a&&f&&0<f.length?
(0>a?(b=0-a,e="-"):(b=a,e=""),f.length>b&&f[b]?e+f[b]:String(a)):String(a)}var u=!1,q="text",k=[],f=[],b=[],j=0,r=0,w="nodes";A.searchtable=function(a,m,e,c,g){var d;w=e;c?(u=!0,q=c):u=!1;f=g?g:!1;j=r=0;k=[];b=[];if(!m)for(e=m=0;e<a.length;e++){g=a[e];for(c=0;c<g.length;c++)d=0>g[c]?0-g[c]:g[c],d>m&&(m=d)}c=new Int32Array(m+1);for(e=0;e<=m;e++)c[e]=0;a=D(a,c,1,1,1)||D(a,c,1,-1,1);m="finished: evaluations count is "+r;m+=", leaves count is "+j;k.push(m);return a?[b,k.join("\r\n")]:[!1,k.join("\r\n")]}})(this.proplog_searchtable=
{});(function(A){function D(b,a){var f,e="";if(x&&"console"==u){for(f=0;f<b;f++)e+=" ";console.log(e+a)}else if(x&&"text"==u){for(f=0;f<b;f++)e+=" ";q.push(e+a)}else if(x&&"html"==u){for(f=0;f<b;f++)e+="&nbsp;";q.push("<div><tt>"+e+"</tt>"+a+"</div>")}}function C(b){var a,f="";if(!0===b)return"tautology";if(!b)return"empty";for(a=0;a<b.length;a++){var e;e=b[a];var c=void 0,g=void 0;e&&k&&0<k.length?(0>e?(c=0-e,g="-"):(c=e,g=""),e=k.length>c&&k[c]?g+k[c]:String(e)):e=String(e);f+=e+" "}return f}var x=
!1,u="text",q=[],k=[],f=[],b=0,j=0,r=0;A.naiveres=function(w,a,m,e){var c,g,d,l,h,A,s;m?(x=!0,u=m):x=!1;k=e?e:!1;r=j=b=0;q=[];f=[];m=[];g=new Int32Array(2*a+1);for(a=!0;0<w.length;){e=w.shift();x&&D(0,"selected "+C(e));c=!1;for(d=0;d<m.length;d++){a:{l=m[d];var y=s=A=h=void 0;if(l.length>e.length)l=!1;else{for(h=0;h<l.length;h++){s=l[h];y=!1;for(A=0;A<e.length;A++)if(e[A]===s){y=!0;break}if(!y){l=!1;break a}}l=!0}}if(l){c=!0;break}}if(c)x&&D(1," was subsumed");else{b++;for(d=0;d<m.length;d++){c=m[d];
x&&D(2,"processed "+C(c));for(l=0;l<e.length;l++){h=e[l];A=0-h;for(h=0;h<c.length;h++)if(A===c[h]){j++;a:{s=e;for(var y=c,v=l,i=h,p=g,I=void 0,n=void 0,t=void 0,B=void 0,z=void 0,E=void 0,F=void 0,H=void 0,G=n=void 0,I=0,n=1;3>n;n++){1===n?(t=s,B=v):(t=y,B=i);for(z=0;z<t.length;z++)if(z!==B){F=t[z];H=0-F;G=!1;for(E=0;E<I;E++){if(p[E]===F){G=!0;break}if(p[E]===H){s=!0;break a}}G||(p[I++]=F)}}if(0===I)s=!1;else{n=new Int32Array(I);for(E=0;E<I;E++)n[E]=p[E];s=n}}x&&D(4,"derived "+C(s));if(!1===s){a=
!1;break}!0!==s&&(r++,w.push(s))}}if(!a)break}if(!a)break;m.push(e)}}w="finished: selected clauses: "+b;w+=", generated clauses: "+j;w+=", kept clauses: "+r;q.push(w);return a?(f=!0,[f,q.join("\r\n")]):[!1,q.join("\r\n")]}})(this.proplog_naiveres={});(function(A){function D(a,d){0>a?d[0-a]=-1:d[a]=1}function C(a,d){100>a.length?d[a.length].push(a):d[99].push(a)}function x(a){var d,b;for(b=1;100>b;b++)if(d=a[b],0<d.length)return a[b].shift();return!1}function u(a,b,e,c){var f,j,k,m,i,p;for(j=m=f=0;j<a.length;j++)if(k=a[j],k!=m){0>k?(m=-1,i=0-k):(m=1,i=k);if(0!==b[i]){if(b[i]===m){if(1<a.length)return!0;c[f++]=k}}else c[f++]=k;m=k}if(0===f)return!1;for(b=0;b<e.length;b++)if(m=e[b],m.length<=f){for(j=i=0;j<m.length;j++){k=m[j];for(p=!1;i<f&&c[i]<=
k;i++)if(c[i]===k){p=!0;i++;break}if(!p)break}if(p)return!0}if(f===a.length)return a;a=new Int32Array(f);for(j=0;j<f;j++)a[j]=c[j];return a}function q(a,d){var c,e="";if(b&&"console"==j){for(c=0;c<a;c++)e+=" ";console.log(e+d)}else if(b&&"text"==j){for(c=0;c<a;c++)e+=" ";r.push(e+d)}else if(b&&"html"==j){for(c=0;c<a;c++)e+="&nbsp;";r.push("<div><tt>"+e+"</tt>"+d+"</div>")}}function k(a){var b,c;return a&&w&&0<w.length?(0>a?(b=0-a,c="-"):(b=a,c=""),w.length>b&&w[b]?c+w[b]:String(a)):String(a)}function f(a){var b,
c="";if(!0===a)return"tautology";if(!a)return"empty";for(b=0;b<a.length;b++)c+=k(a[b])+" ";return c}var b=!1,j="text",r=[],w=[],a=[],m=0,e=0,c=0;A.resolution=function(g,d,l,h){var A,s,y,v,i,p,I,n;l?(b=!0,j=l):b=!1;w=h?h:!1;c=e=m=0;r=[];a=[];A=[];I=new Int32Array(2*d+1);l=new Int32Array(d+1);for(s=0;s<d+1;s++)l[s]=0;h=Array(100);for(s=0;100>s;s++)h[s]=[];b&&q(0,"starting to process input unit clauses");for(s=0;s<g.length;s++)if(i=g[s],1===i.length){p=i[0];0>p?(v=-1,p=0-p):v=1;if(0!==l[p]){if(l[p]===
v)continue;q(0,"empty clause derived from "+f(i));r.push("Finished while preprocessing.");return[!1,r.join("\r\n")]}D(i[0],l);C(i,h)}b&&q(0,"input unit clauses processed, starting to process non-unit");v=!0;for(s=0;s<g.length;s++)if(i=g[s],!(2>i.length)){a:{n=y=y=p=void 0;for(p=1;p<i.length;p++){y=i[p];n=0-y;for(y=0;y<p;y++)if(i[y]===n){p=!0;break a}}p=!1}if(!p){p=[];y=0;n=i.length-1;for(var t=void 0,B=void 0,z=void 0,E=void 0;;)if(25>=n-y){for(B=y+1;B<=n;B++){z=i[B];for(t=B-1;t>=y&&i[t]>z;)i[t+1]=
i[t--];i[t+1]=z}if(0==p.length)break;n=p.pop();y=p.pop()}else{E=y+n>>1;t=y+1;B=n;z=i[E];i[E]=i[t];i[t]=z;i[y]>i[n]&&(z=i[y],i[y]=i[n],i[n]=z);i[t]>i[n]&&(z=i[t],i[t]=i[n],i[n]=z);i[y]>i[t]&&(z=i[y],i[y]=i[t],i[t]=z);for(E=i[t];;){do t++;while(i[t]<E);do B--;while(i[B]>E);if(B<t)break;z=i[t];i[t]=i[B];i[B]=z}i[y+1]=i[B];i[B]=E;n-t+1>=B-y?(p.push(t),p.push(n),n=B-1):(p.push(y),p.push(B-1),y=t)}i=u(i,l,[],I);if(!1===i)return b&&q(0,"empty clause derived from "+f(g[s])),r.push("Finished while preprocessing."),
[!1,r.join("\r\n")];if(!0!==i&&(C(i,h),v))for(y=p=0;y<i.length;y++)if(!(0>i[y])&&(p++,1<p)){v=!1;break}}}b&&(q(0,"input non-unit clauses processed "),v?q(0,"observation: clause set is horn"):q(0,"observation: clause set is not horn"));g=Array(d+1);for(s=0;s<=d;s++)g[s]=[];v=Array(d+1);for(s=0;s<=d;s++)v[s]=[];for(d=!0;s=x(h);){b&&q(0,"selected candidate "+f(s));a:{i=l;p=g;y=v;n=I;for(var F=B=t=void 0,H=void 0,G=H=F=F=z=void 0,K=void 0,J=E=void 0,B=F=t=0;B<s.length;B++)if(z=s[B],z!=F){0>z?(F=-1,H=
0-z):(F=1,H=z);if(0!==i[H]){if(i[H]===F)if(1<s.length){s=!0;break a}else n[t++]=z}else n[t++]=z;F=z}if(0===t)s=!1;else{for(H=0;H<t;H++){z=n[H];J=0>z?y[0-z]:p[z];for(G=0;G<J.length;G++)if(K=J[G],K.length<=t){for(B=F=0;B<K.length;B++){z=K[B];for(E=!1;F<t&&n[F]<=z;F++)if(n[F]===z){E=!0;F++;break}if(!E)break}if(E){s=!0;break a}}}if(t!==s.length){s=new Int32Array(t);for(B=0;B<t;B++)s[B]=n[B]}}}if(!s){d=!1;break}if(!0===s)b&&q(1,"subsumed");else{b&&q(0,"preprocessed to "+f(s));m++;i=s[0];0>i?(i=0-i,i=g[i]):
i=v[i];for(p=0;p<i.length;p++)if(y=i[p],!0!==y){b&&q(2,"processed "+f(y));e++;a:{n=s;for(var t=y,B=I,z=l,L=G=J=K=K=G=H=F=E=void 0,L=J=void 0,E=n.length,H=F=0;H<t.length;H++)if(0!==H)if(K=t[H],J=0-K,0>K?(G=-1,L=J):(G=1,L=K),0!==z[L]){if(z[L]===G){n=!0;break a}}else{L=!1;for(G=0;G<E;G++)if(0!==G){if(n[G]===K){L=!0;break}if(n[G]===J){n=!0;break a}}L||(B[F++]=K)}if(0===F&&2>E)n=!1;else{J=new Int32Array(E-1+F);for(K=G=H=0;H<E&&G<F;)0===H?H++:n[H]<=B[G]?J[K++]=n[H++]:J[K++]=B[G++];for(;H<E;H++)0!==H&&(J[K++]=
n[H]);for(;G<F;G++)J[K++]=B[G];n=J}}if(!1===n){d=!1;break}if(!0===n)b&&q(4,"derived clause a tautology or subsumed");else{c++;1===n.length&&D(n[0],l);b&&q(4,"kept "+f(n));C(n,h);a:if(E=z=B=t=void 0,n.length>y.length)y=!1;else{for(t=B=0;t<n.length;t++){z=n[t];for(E=!1;B<y.length&&y[B]<=z;B++)if(y[B]===z){E=!0;B++;break}if(!E){y=!1;break a}}y=!0}y&&(i[p]=!0)}}if(!d)break;1===s.length&&D(s[0],l);i=A;p=g;y=void 0;y=s[0];0>y?v[0-y].push(s):p[y].push(s);i.push(s)}}h="finished: selected clauses: "+m;h+=
", generated clauses: "+e;h+=", kept clauses: "+c;r.push(h);if(d){a=[];for(s=0;s<l.length;s++)0!==l[s]&&a.push(k(s*l[s]));0==a.length&&(a=!0);return[a,r.join("\r\n")]}return[!1,r.join("\r\n")]}})(this.proplog_res={});