OKlibrary  0.2.1.6
LinearEquations.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 11.5.2013 (Swansea) */
00002 /* Copyright 2013 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 
00024 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/PartialAssignments.mac")$
00028 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Substitutions.mac")$
00029 oklib_include("OKlib/ComputerAlgebra/NumberTheory/Lisp/Auxiliary.mac")$
00030 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/Generators.mac")$
00031 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Generators/Pigeonhole.mac")$
00032 
00033 
00034 /* *********************
00035    * Parity conditions *
00036    *********************
00037 */
00038 
00039 /* The repetition-free clause-list of full clauses over variables 1, ..., n,
00040    such that the satisfying assignments are given by the condition that the
00041    sum over the values is even resp. odd, that is, the list of full clauses
00042    having an odd resp. even number of negative literals; the order is
00043    lexicographical:
00044 */
00045 even_parity_cl(n) :=
00046   sublist(all_tass_l(setn(n)),
00047           lambda([C], oddp(sum_l(map(negsignum, listify(C))))))$
00048 /* Now supplying the list V of variables: */
00049 even_parity_wv_cl(V) :=
00050   sublist(all_tass_l(setify(V)),
00051           lambda([C], oddp(sum_l(map(negsignum, listify(C))))))$
00052 /* As formal clause-list: */
00053 even_parity_fcl(n) := [create_list(i,i,1,n),even_parity_cl(n)]$
00054 
00055 odd_parity_cl(n) :=
00056   sublist(all_tass_l(setn(n)),
00057           lambda([C], evenp(sum_l(map(negsignum, listify(C))))))$
00058 /* Now supplying the list V of variables: */
00059 odd_parity_wv_cl(V) :=
00060   sublist(all_tass_l(setify(V)),
00061           lambda([C], evenp(sum_l(map(negsignum, listify(C))))))$
00062 /* As formal clause-list: */
00063 odd_parity_fcl(n) := [create_list(i,i,1,n),odd_parity_cl(n)]$
00064 
00065 
00066 /* **********************
00067    * Parity constraints *
00068    **********************
00069 */
00070 
00071 /*
00072   A "(boolean) parity-constraint" ("prt") is a list L of literals with
00073   different underlying variables, with meaning "sum_{x in L} x = 0",
00074   where the sum takes places in the 2-element field {0,1} (i.e., the sum
00075   is xor).
00076   A "general (boolean) parity-constraint" ("gprt") is a pair [L,e], where
00077   L is a list of literals (arbitrary) and e in {0,1}. Again, the meaning is
00078   "sum_{x in L} x = 0".
00079 */
00080 
00081 prt2gprt(P) := [P,0]$
00082 
00083 /* Simplifying a general parity-constraint P to a parity-constraint or to
00084    false iff P is unsatisfiable, sorted in ascending order by absolute values,
00085    and such that at most one literal is negative, which then is the first
00086    literal:
00087 */
00088 gprt2prt(P) := block([L:first(P), e:second(P), res:{}],
00089  for x in L do
00090    if elementp(x,res) then res : disjoin(x,res)
00091    elseif elementp(-x,res) then (res : disjoin(-x,res), e : 1-e)
00092    else
00093      if pos_l(x) then res : adjoin(x,res)
00094      else (res : adjoin(-x,res), e : 1-e),
00095  res : listify(res),
00096  if e=1 then
00097    if emptyp(res) then false
00098    else cons(-first(res), rest(res))
00099  else res)$
00100 /* Remark: gprt2prt(P) is a normalform for P, with two general
00101    parity-constraints P1, P2 being equivalent (having the same satisfying
00102    assignments) iff gprt2prt(P1) = gprt2prt(P2).
00103 */
00104 
00105 /* Equivalence of (general) parity constaints: */
00106 equiv_gprt(P1,P2) := is(gprt2prt(P1) = gprt2prt(P2))$
00107 equiv_prt(P1,P2) := is(gprt2prt([P1,0]) = gprt2prt([P2,0]))$
00108 
00109 
00110 /* Adding together a list of (general) parity-constraints and simplifying the
00111    result:
00112 */
00113 addgprt2prt(L) :=
00114  gprt2prt([lappend(map(first,L)), mod(sum_l(map(second,L)),2)])$
00115 addprt2prt(L) := addgprt2prt(map(prt2gprt,L))$
00116 
00117 
00118 /* **********************************
00119    * Translating parity constraints *
00120    **********************************
00121 */
00122 
00123 /* Direct translation: */
00124 prt2cl_0(P) :=
00125  if evenp(sum_l(map(negsignum, listify(P)))) then
00126    even_parity_wv_cl(map(var_l,P))
00127  else odd_parity_wv_cl(map(var_l,P))$
00128 /* Remark: this directly generalises even_parity_wv_cl(V). */
00129 
00130 /* Translating the sequence of partial equations, using the list aux of
00131    auxiliary variables fulfilling length(aux) >= length(P)-2:
00132 */
00133 prt2cl_aux_1(P,aux) := if length(P) <= 2 then prt2cl_0(P)
00134  else block([F : prt2cl_0([P[1],P[2],aux[1]])],
00135   P : rest(P,2),
00136   while length(P) > 1 do (
00137     F : append(F, prt2cl_0([P[1],aux[1],aux[2]])),
00138     P : rest(P), aux : rest(aux)
00139   ),
00140   append(F, prt2cl_0([P[1],aux[1]])))$
00141 
00142 /* A generator for unsatisfiable clause-sets of hardness n and w-hardness 2
00143    (for n >= 2), via translating the prt's [1,...,n], and [1,...,n-1,-n]:
00144 */
00145 gen_2xor_fcl(n) := if n<=2 then full_fcl(n) else
00146  [listn(3*n-4),
00147   append(prt2cl_aux_1(listn(n), listmn(n+1,2*n-2)),
00148          prt2cl_aux_1(endcons(-n,listn(n-1)), listmn(2*n-1,3*n-4)))]$
00149 
00150 output_gen_2xor_fcl(n,filename) :=
00151  outputext_fcl(
00152    sconcat("2 xor-clauses with contradiction, ", n, " basic variables.
00153 c Created by the OKlibrary at ", timedate(), "."),
00154    gen_2xor_fcl(n),
00155    filename)$
00156 
00157 output_gen_2xor_stdname(n) := output_gen_2xor_fcl(n,
00158  sconcat("TwoXORclauses-",n,".cnf"))$
00159 
00160 
00161 /* Translating equalities. */
00162 
00163 /* For a set S of literals, translate the condition that they all shall be
00164    equal:
00165 */
00166 seteqlit2cl(S) := if emptyp(S) then []
00167  elseif not emptyp(intersection(S,comp_sl(S))) then [{}]
00168  else block([x],
00169   S:listify(S), x:first(S),
00170   lappend(map(lambda([y], prt2cl_0([x,y])), rest(S))))$
00171 
00172 
00173 /* Translation of two xor-clauses. */
00174 
00175 /* Using the UC-translation for the two parity-constraints, plus the
00176    UC-translation for the sum of the two parity constraints, where actually
00177    general parity-constraints are allowed:
00178 */
00179 gprt2s2cl_aux_2(P1,aux1,P2,aux2,aux3) :=
00180  block([S1:gprt2prt(P1), S2:gprt2prt(P2), S3],
00181   S3 : addgprt2prt([P1,P2]),
00182   if S1=false or S2=false or S3=false then [{}]
00183   else append(prt2cl_aux_1(S1,aux1), prt2cl_aux_1(S2,aux2), prt2cl_aux_1(S3,aux3)))$
00184 
00185 
00186 /* An improved translation, not using the third (derived) constraint, but
00187    "sharing common sub-expressions", that is, the value of the common part
00188    is used via the appropriate (auxiliary) variable in the larger constraint:
00189 */
00190 gprt2s2cl_aux_s(P1,aux1,P2,aux2) :=
00191  block([S1:gprt2prt(P1), S2:gprt2prt(P2)],
00192   if S1=false or S2=false or addgprt2prt([[S1,0],[S2,0]])=false then [{}]
00193   elseif emptyp(S2) or S1=S2 then prt2cl_aux_1(S1,aux1)
00194   elseif emptyp(S1) then prt2cl_aux_1(S2,aux2)
00195   else block([e1:0, e2:0, I],
00196    if neg_l(first(S1)) then (e1:1, S1:cons(-first(S1),rest(S1))),
00197    if neg_l(first(S2)) then (e2:1, S2:cons(-first(S2),rest(S2))),
00198    S1:setify(S1), S2:setify(S2),
00199    I : intersection(S1, S2),
00200    if emptyp(I) then
00201      return(append(prt2cl_aux_1(gprt2prt([S1,e1]),aux1), prt2cl_aux_1(gprt2prt([S2,e2]),aux2))),
00202    if length(S1)>length(S2) then block([S:S2,a:aux2],S2:S1,S1:S,aux2:aux1,aux1:a),
00203    S1 : append(listify(I), listify(setdifference(S1,I))),
00204    S2 : listify(setdifference(S2,I)),
00205    if length(I)=length(S1) then (
00206      e2 : e2 + e1,
00207      return(append(prt2cl_aux_1(gprt2prt([S1,e1]),aux1), prt2cl_aux_1(gprt2prt([S2,e2]),aux2)))
00208    )
00209    elseif length(I)=1 then S2 : cons(first(S1), S2)
00210    else S2 : cons(aux1[length(I)-1], S2),
00211    if e1=1 then S1 : endcons(-last(S1),rest(S1,-1)),
00212    return(append(prt2cl_aux_1(S1,aux1), prt2cl_aux_1(gprt2prt([S2,e2]),aux2)))
00213   ))$
00214 /* Remark: The order of clauses is as given by gprt2prt and prt2cl_aux_1. */
00215 
00216 /* A generator for unsatisfiable clause-sets, with p >= 1 the common
00217    "parity part", and q >= 0 the "pigeonhole part":
00218    The main variables are 1,...,p and the variables php(i,j) of weak_php(m,n)
00219    with n=2*q and m=n+1.
00220    We have two parity-constraints, namely that, using v_1,...,v_p for
00221    the variables 1,...,p, "+" for xor, and S = v_1+...+v_{p-1}:
00222      S + v_p + php(1,1) + ... + php(1,q) = 0
00223      S - v_p + php(1,q+1) + ... + php(1,n) = 0.
00224    From this follows that
00225      php(1,1) + ... + php(1,n) = 1.
00226    And then we have weak_php_cs(m,n) minus the clause
00227      {php(1,1), ... php(1,n)}
00228    (which enforces, that php(1,1) = ... = php(1,n) = 0).
00229    For s=0 the translation sprt2cl_aux_1 is used, for s=1 the translation
00230    gprt2s2cl_aux_s.
00231 */
00232 /* TODO: the natural-number-variables should be numbered without gap (
00233    currently this is not the case for aux2). */
00234 /* TODO: we need the ordered version. */
00235 /* TODO: we need the standardised version. */
00236 /* TODO: for s=2 the two parity-constraints are replaced by
00237    php(1,1) + ... + php(1,n) = 1.
00238 */
00239 parityphp_cs(p,q,s) := block([n:2*q, m:2*q+1, PH, C, P1,P2,aux1,a,aux2,P],
00240  PH : weak_php_cs(m,n),
00241  C : create_list(php_var(1,j),j,1,n),
00242  PH : disjoin(setify(C), PH),
00243  P1 : append(listn(p),rest(C,-q)),
00244  P2 : append(listn(p-1),[-p],rest(C,q)),
00245  a : p+1+length(P1)-2,
00246  aux1 : listmn(p+1, a-1),
00247  aux2 : listmn(a, a + length(P2)-2 -1),
00248  if s=0 then
00249   P : sprt2cl_aux_1([[P1,aux1],[P2,aux2]])
00250  else
00251   P : gprt2s2cl_aux_s([P1,0],aux1,[P2,0],aux2),
00252  union(PH,cl2cs(P)))$
00253 parityphp_fcl(p,q,s) := cs2fcl(parityphp_cs(p,q,s))$
00254 
00255 output_parityphp_cs(p,q,s,filename) := block(
00256  [FF : standardise_fcl(parityphp_fcl(p,q,s))],
00257   output_fcl_v(
00258     sconcat("2 parity-constraints plus PHP, p=", p, ", q=", q, ", s=", s, ".
00259 c Created by the OKlibrary at ", timedate(), "."),
00260     FF[1], filename, FF[2]))$
00261 
00262 output_parityphp_stdname(p,q,s) := output_parityphp_cs(p,q,s,
00263  sconcat("ParityPHP-",p,"_",q,"_",s,".cnf"))$
00264 
00265 
00266 /* Finally general systems of parity constraints ("sprt"). */
00267 
00268 
00269 /* For a list L of parity constraints the prime implicates per constraint: */
00270 sprt2cl_0(L) := lappend(map(prt2cl_0,L))$
00271 
00272 
00273 /* For a list of pairs [P,aux], where aux is the list of auxiliary variables
00274    (or literals; all new), applying translation prt2cl_aux_1 per pair:
00275 */
00276 sprt2cl_aux_1(L) := lappend(map(lambda([p],apply(prt2cl_aux_1,p)), L))$
00277 
00278 /* Adding to sprt2cl_aux_1(L) all (valid) equalities between auxiliary
00279    variables and their complements (using seteqlit2cl to produce the
00280    equality between sets C of literals, where the C are taken in (built-in)
00281    lexicographical order):
00282 */
00283 sprt2cl_aux_1e(L) := block([h:sm2hm({}), V:{}, E],
00284   for p in L do block([i:2, x:first(p), a:second(p)],
00285     if length(x) >= 3 then
00286       for y in take_l(length(x)-2, a) do (
00287         V : adjoin(y,V), V : adjoin(-y,V),
00288         set_hm(h,y,gprt2prt([take_l(i,x),0])),
00289         set_hm(h,-y,gprt2prt([take_l(i,x),1])),
00290         i:i+1
00291       )
00292     ),
00293     E : equiv_classes(V, lambda([y1,y2], is(ev_hm(h,y1)=ev_hm(h,y2)))),
00294     E : equiv_classes(E, lambda([C,D], is(comp_sl(C)=D))),
00295     E : listify(map(first_element, E)),
00296     append(sprt2cl_aux_1(L), lappend(map(seteqlit2cl, E))))$
00297 
00298 
00299 /* Extending a set SP of parity-constraints by all xor-clauses (modulo
00300    equivalence, without the empty parity-constraint) which follow, replacing
00301    the original xor-clauses by their standardisation:
00302 */
00303 closure_sprt(SP) := block(
00304  [E : disjoin([],map(lambda([s], addprt2prt(listify(s))), disjoin({},powerset(SP))))],
00305   if elementp(false,E) then {false} else E)$
00306 
00307