OKlibrary  0.2.1.6
Proofs.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 23.9.2011 (Swansea) */
00002 /* Copyright 2011, 2012 Oliver Kullmann
00003 This file is part of the OKlibrary. OKlibrary is free software; you can redistribute
00004 it and/or modify it under the terms of the GNU General Public License as published by
00005 the Free Software Foundation and included in this library; either version 3 of the
00006 License, or any later version. */
00007 
00022 oklib_include("OKlib/ComputerAlgebra/Trees/Lisp/Basics.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Resolution/Basics.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/Pigeonhole.mac")$
00026 
00027 
00028 
00029 /* ******************
00030    * Basic concepts *
00031    ******************
00032 */
00033 
00034 /*
00035   A "resolution proof as a list" ("resl") is a list, where each entry is
00036   either a clause (an "axiom") or a pair consisting of a clause
00037   (the "resolvent") and a pair of (smaller) indices (the indices of the
00038   "parent clauses").
00039 
00040   A "resolution tree" ("reslrt") is a labelled rooted tree (lrt) T where T is
00041   a binary tree such that each inner node is the resolvent of its two children.
00042   The notion of an lrt is defined in ComputerAlgebra/Trees/Lisp/Basics.mac.
00043 */
00044 
00045 
00046 /* ************************************
00047    * Checking the defining properties *
00048    ************************************
00049 */
00050 
00051 /* Is list L a resolution proof as a list: */
00052 resl_p(L) := listp(L) and block([is_resl : true, L_i],
00053   for i : 1 thru length(L) while is_resl do (
00054     L_i : L[i],
00055     is_resl : c_p(L_i) or
00056       (listp(L_i) and is(length(L_i) = 2) and
00057         c_p(L_i[1]) and listp(L_i[2]) and block([ind_l : L_i[2]],
00058           is(length(ind_l) = 2) and integerp(ind_l[1]) and integerp(ind_l[2])
00059           and is(0 < ind_l[1]) and is(ind_l[1] < i) and is(0 < ind_l[2]) and
00060           is(ind_l[2] < i) and
00061           if c_p(L[ind_l[1]]) and c_p(L[ind_l[2]]) then
00062             (resolvable(L[ind_l[1]],L[ind_l[2]]) and
00063              is(resolvent(L[ind_l[1]],L[ind_l[2]]) = L_i[1]))
00064           else if c_p(L[ind_l[1]]) and not(c_p(L[ind_l[2]])) then
00065             (resolvable(L[ind_l[1]],L[ind_l[2]][1]) and
00066              is(resolvent(L[ind_l[1]],L[ind_l[2]][1]) = L_i[1]))
00067           else if not(c_p(L[ind_l[1]])) and c_p(L[ind_l[2]]) then
00068             (resolvable(L[ind_l[1]][1],L[ind_l[2]]) and
00069              is(resolvent(L[ind_l[1]][1],L[ind_l[2]]) = L_i[1]))
00070           else
00071             (resolvable(L[ind_l[1]][1],L[ind_l[2]][1]) and
00072              is(resolvent(L[ind_l[1]][1],L[ind_l[2]][1]) = L_i[1])) ))),
00073     return(is_resl))$
00074 
00075 /* Is list L a resolution refutation as a list: */
00076 resl_ref_p(L) :=
00077   resl_p(L) and (member({},L) or member({}, resolvents_resl2cl(L)))$
00078 
00079 /* Is T a "resolution tree": */
00080 reslrt_p(T) := listp(T) and
00081   if length(T) = 1 then c_p(T[1]) /* Leaves must be clauses */
00082   else is(length(T) = 3) and c_p(T[1]) and
00083        reslrt_p(T[2]) and reslrt_p(T[3]) and
00084        resolvable(T[2][1],T[3][1]) and is(resolvent(T[2][1],T[3][1]) = T[1])$
00085 
00086 
00087 /* ************************************
00088    * Other properties                 *
00089    ************************************
00090 */
00091 
00092 /* Is L irredundant (we create any unused resolvents): */
00093 irredundant_ref_resl(L) := block([used_indices, unused_indices],
00094   used_indices :
00095     setify(lappend(
00096         map(lambda([R], R[2]),
00097           sublist(L, lambda([R],not(c_p(R))) )))),
00098   unused_indices : setdifference(setn(length(L)-1),used_indices),
00099   return(is(unused_indices = {})))$
00100 
00101 
00102 /* ************************************
00103    * Extraction                       *
00104    ************************************
00105 */
00106 
00107 /* Axioms of a resolution list as a clause-list: */
00108 axioms_resl2cl(L) := sublist(L,c_p)$
00109 
00110 /* Resolvents of a resolution list as a clause-list: */
00111 resolvents_resl2cl(L) := map(lambda([a],a[1]), sublist(L,listp))$
00112 
00113 
00114 /* ************************************
00115    * Modifying proofs                 *
00116    ************************************
00117 */
00118 
00119 
00120 /* Renaming variables in a resolution proof L where the renaming is given as
00121    a hashmap h mapping literals to literals: */
00122 rename_resl(L,h) :=
00123   map(lambda([R],
00124         if c_p(R) then substitute_c(R,h)
00125         else [substitute_c(R[1],h),R[2]]), L)$
00126 
00127 
00128 /* ************************************
00129    * Generators                       *
00130    ************************************
00131 */
00132 
00133 
00134 /* A polynomial-size resolution proof for weak_php_unsat_ext_uni_fcs(n): */
00135 php_ext_uni_resl(n) := block([axioms, resolvents_cl : [], c2i_h : sm2hm({}), p2q_h : sm2hm({})],
00136   axioms : weak_php_unsat_ext_uni_fcs(n),
00137   /* Create all the resolutions storing explicitly the clauses, not indices;
00138      we map clauses to indices later. */
00139   /* Small clauses for each level */
00140   resolvents_cl : append(resolvents_cl, reverse(
00141     create_list(
00142       [[{-php_ext_var(l,i,j),php_ext_var(l+1,i,j),-php_ext_var(l+1,k,j)},
00143          [{-php_ext_var(l,i,j),php_ext_var(l+1,i,j),php_ext_var(l+1,l+2,j)},
00144            {-php_ext_var(l+1,l+2,j), -php_ext_var(l+1,k,j)}]],
00145        [{-php_ext_var(l,i,j),-php_ext_var(l+1,k,j)},
00146          [{-php_ext_var(l,i,j),php_ext_var(l+1,i,j),-php_ext_var(l+1,k,j)},
00147            {-php_ext_var(l+1,i,j), -php_ext_var(l+1,k,j)}]],
00148        [{-php_ext_var(l,k,j),php_ext_var(l+1,k,j),-php_ext_var(l+1,i,j)},
00149          [{-php_ext_var(l,k,j),php_ext_var(l+1,k,j),php_ext_var(l+1,l+2,j)},
00150            {-php_ext_var(l+1,l+2,j), -php_ext_var(l+1,i,j)}]],
00151        [{-php_ext_var(l,k,j),-php_ext_var(l+1,i,j)},
00152          [{-php_ext_var(l,k,j),php_ext_var(l+1,k,j),-php_ext_var(l+1,i,j)},
00153            {-php_ext_var(l+1,i,j), -php_ext_var(l+1,k,j)}]],
00154        [{-php_ext_var(l,k,j),-php_ext_var(l,i,j),php_ext_var(l+1,k,l+1)},
00155          [{-php_ext_var(l,k,j),php_ext_var(l+1,k,j),php_ext_var(l+1,k,l+1)},
00156            {-php_ext_var(l,i,j),-php_ext_var(l+1,k,j)}]],
00157        [{-php_ext_var(l,k,j),-php_ext_var(l,i,j),php_ext_var(l+1,i,l+1)},
00158          [{-php_ext_var(l,i,j),php_ext_var(l+1,i,j),php_ext_var(l+1,i,l+1)},
00159            {-php_ext_var(l,k,j),-php_ext_var(l+1,i,j)}]],
00160        [{-php_ext_var(l,k,j),-php_ext_var(l,i,j),-php_ext_var(l+1,k,l+1)},
00161          [{-php_ext_var(l,k,j),-php_ext_var(l,i,j),php_ext_var(l+1,i,l+1)},
00162            {-php_ext_var(l+1,k,l+1),-php_ext_var(l+1,i,l+1)}]],
00163        [{-php_ext_var(l,k,j),-php_ext_var(l,i,j)},
00164          [{-php_ext_var(l,k,j),-php_ext_var(l,i,j),-php_ext_var(l+1,k,l+1)},
00165           {-php_ext_var(l,k,j),-php_ext_var(l,i,j),php_ext_var(l+1,k,l+1)}]]],
00166        l,1,n-1, i,1,l+1, j, 1,l, k, 1, i-1))),
00167   /* Long clauses for each level */
00168   resolvents_cl : append(resolvents_cl, lappend( reverse(
00169     create_list(
00170       append(
00171         create_list(
00172           [[ setify(
00173                append(
00174                  create_list(php_ext_var(l,i,j_t), j_t, 1, j),
00175                  create_list(php_ext_var(l+1,i,j_t), j_t, j+1, l+1))),
00176              [setify(
00177                append(
00178                  create_list(php_ext_var(l,i,j_t), j_t, 1, j-1),
00179                  create_list(php_ext_var(l+1,i,j_t), j_t, j, l+1))),
00180              {php_ext_var(l,i,j),-php_ext_var(l+1,i,j)} ]]],
00181           i, 1, l+1, j, 1, l),
00182         create_list(
00183           [[ setify(
00184                append(
00185                  create_list(php_ext_var(l,i,j_t), j_t, 1, j),
00186                  create_list(php_ext_var(l+1,l+2,j_t), j_t, j+1, l+1),
00187                  [-php_ext_var(l+1,i,l+1)])),
00188              [setify(
00189                append(
00190                  create_list(php_ext_var(l,i,j_t), j_t, 1, j-1),
00191                  create_list(php_ext_var(l+1,l+2,j_t), j_t, j, l+1),
00192                  if j > 1 then [-php_ext_var(l+1,i,l+1)] else [])),
00193              {php_ext_var(l,i,j),-php_ext_var(l+1,i,l+1),-php_ext_var(l+1,l+2,j)} ]]],
00194           i,1,l+1,j, 1, l),
00195         create_list(
00196           [[ setify(
00197                append(
00198                  create_list(php_ext_var(l,i,j_t), j_t, 1, l),
00199                  [-php_ext_var(l+1,i,l+1)])),
00200              [setify(
00201                append(
00202                  create_list(php_ext_var(l,i,j_t), j_t, 1, l),
00203                  [php_ext_var(l+1,l+2,l+1),-php_ext_var(l+1,i,l+1)])),
00204              {-php_ext_var(l+1,i,l+1),-php_ext_var(l+1,l+2,l+1)} ]]],
00205           i,1,l+1),
00206         create_list(
00207           [[ setify(
00208              create_list(php_ext_var(l,i,j_t), j_t, 1, l)),
00209              [setify(
00210                append(
00211                  create_list(php_ext_var(l,i,j_t), j_t, 1, l),
00212                  [-php_ext_var(l+1,i,l+1)])),
00213               setify(
00214                append(
00215                  create_list(php_ext_var(l,i,j_t), j_t, 1, l),
00216                  [php_ext_var(l+1,i,l+1)])) ]]],
00217           i,1,l+1)),
00218     l,1,n-1)))),
00219   /* Finally derive the empty clause: */
00220   if n > 0 then
00221     resolvents_cl : append(resolvents_cl,
00222       [[[ {-php_ext_var(1,2,1)},
00223        [{-php_ext_var(1,1,1), -php_ext_var(1,2,1)},
00224        {php_ext_var(1,1,1)}]],
00225        [{},
00226          [{php_ext_var(1,2,1)},
00227          {-php_ext_var(1,2,1)}]]]]),
00228   /* Map clauses to indices and php_ext_var(n+1,i,j) to php_var(i,j) */
00229   resolvents_cl : append(listify(axioms[2]),lappend(resolvents_cl)),
00230   resolvents_cl : map(
00231     lambda([R,i],
00232       if c_p(R) then (set_hm(c2i_h,R,i), R)
00233       else (set_hm(c2i_h, R[1], i),
00234             [R[1], map(lambda([C],ev_hm(c2i_h,C)),R[2])])),
00235     resolvents_cl,
00236     create_list(i,i,1,length(resolvents_cl))),
00237   return(resolvents_cl))$
00238 /* The resolution proof of weak_php_unsat_ext_fcs(n): */
00239 php_ext_resl(n) := rename_resl(php_ext_uni_resl(n),sm2hm(var_ephp2php_sm(n)))$
00240 
00241 
00242 /* Statistics for php_ext_uni_resl: */
00243 nvar_php_ext_uni_resl(n) := nvar_weak_php_unsat_ext(n)$
00244 ncl_php_ext_uni_resl(n) := (6*n^4+11*n^3+3*n^2+4*n+6)/6$
00245 
00246 
00247 
00248