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