OKlibrary  0.2.1.6
SplittingTrees.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 29.11.2007 (Swansea) */
00002 /* Copyright 2007, 2008, 2009, 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/Hypergraphs/Lisp/SetSystems.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Reductions/GeneralisedUCP.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Resolution/Basics.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Trees/Lisp/Basics.mac")$
00027 
00028 
00029 /* ************************************
00030    * The notion of a "splitting tree" *
00031    ************************************
00032 */
00033 
00034 /*
00035 
00036  A "boolean splitting tree" ("st") for a clause-set F is either
00037   - [[]] for "nothing done",
00038   - or [false] in case F contains the empty clause,
00039   - or [true] in case F is empty,
00040   - or [x, T0, T1], where x is a boolean literal and
00041     T0/1 is a splitting tree of <x -> 0/1> * F.
00042 
00043  Thus boolean splitting trees are labelled binary rooted trees, where inner
00044  nodes are labelled by literals, and leaves are labelled by true, false or [].
00045  Splitting trees can be seen as exactly boolean decision trees.
00046 
00047  A boolean splitting tree is complete iff no leaf labelled by [].
00048 
00049  More precisely we speak of
00050   - "formal splitting trees" (no relation to a clause-set)
00051   - "splitting trees"
00052   - "extended splitting trees" (splitting can always continue).
00053  We can refer to them all via "st", if however a distinction is needed, then
00054  "fst" resp. "est" is used. See below for precise definitions.
00055 
00056 */
00057 
00058 /* Whether T is a formal splitting tree: */
00059 fst_p(T) := lrt_p(T) and rt2_p(lrt2rt(T)) and
00060  subsetp(ll_lrt(T), {true, false,[]})$
00061 
00062 /* Whether T is a splitting tree for clause-set F: */
00063 st_p(T,F) := fst_p(T) and subsetp(il_lrt(T), flit_cs(F)) and st0_p(T,F)$
00064 /* Remark: the condition "subsetp(il_lrt(T), flit_cs(F))" is on the one hand
00065    too strong (typically we don't need it), and on the other hand not
00066    strong enough, since it is inherited to sub-trees (variables might vanish).
00067    So perhaps a revision of the concepts is needed: best seems to have
00068    two concepts, one with no requirements on the literals, one where they
00069    need to be formal literals of the *current* clause-set.
00070 */
00071 /* Whether rooted tree T, which fulfills the formal requirements for being
00072    a splitting tree for F, fulfills the splitting requirements, that is,
00073    a leaf is exactly reached when either we have [] or when the clause-set
00074    has been decided (by creating the empty clause-set resp. the empty clause):
00075 */
00076 st0_p(T,F) := if length(T)=1 then
00077    if T=[true] then is(F={})
00078    elseif T=[false] then elementp({},F)
00079    else true
00080  elseif F={} or elementp({},F) then false
00081  else block([x,T1,T2],
00082    [x,T0,T1] : T,
00083    st0_p(T0,apply_pa_cs({-x},F)) and st0_p(T1,apply_pa_cs({x},F)))$
00084 
00085 /* Testing for "extended splitting tree for clause-set F", where now there are
00086    no requirements on the splitting literals (they don't need to be literals
00087    of F), and also further splitting is possible in case one arrived already
00088    at the empty clause(-set):
00089 */
00090 est_p(T,F) := fst_p(T) and est0_p(T,F)$
00091 est0_p(T,F) := if length(T)=1 then
00092    if T=[true] then is(F={})
00093    elseif T=[false] then elementp({},F)
00094    else true
00095  else block([x,T1,T2],
00096    [x,T0,T1] : T,
00097    est0_p(T0,apply_pa_cs({-x},F)) and est0_p(T1,apply_pa_cs({x},F)))$
00098 
00099 /* Whether the formal splitting tree T is complete: */
00100 complete_stp(T) := not elementp([], ll_lrt(T))$
00101 
00102 
00103 /* ********************************
00104    * Manipulating splitting trees *
00105    ********************************
00106 */
00107 
00108 fst2st(T,F) :=
00109  if emptyp(F) then [true]
00110  elseif has_empty_element(F) then [false]
00111  elseif length(F)=1 then [[]]
00112  else block([x : first(T)],
00113   if not elementp(x, flit_cs(F)) then
00114    if nnds_lrt(second(T)) <= nnds_lrt(third(T)) then second(T) else third(T)
00115   else [x, fst2st(second(T), apply_pa_cs({-x},F)), fst2st(third(T), apply_pa_cs({x},F))])$
00116 
00117 /* Negate a splitting tree, i.e., negate the leaves: */
00118 negate_st(T) := if length(T) = 1 then [not T[1]] else
00119 [T[1], negate_st(T[2]), negate_st(T[3])]$
00120 
00121 /* Condense a splitting tree to a splitting tree representing the same
00122    boolean function, but where every inner node has one satisfiable
00123    and one unsatisfiable successor:
00124 */
00125 condense_st(T) := if length(T) = 1 then T else block(
00126  [x : T[1], T1 : condense_st(T[2]), T2 : condense_st(T[3])],
00127  if T1 = [false] and T2 = [false] then return([false])
00128  elseif T1 = [true] and T2 = [true] then return([true])
00129  else return([x, T1, T2]))$
00130 
00131 
00132 /* ***************************
00133    * Finding splitting trees *
00134    ***************************
00135 */
00136 
00137 monitorcheck_osl(name) := if oklib_monitor then (
00138   if depth <= oklib_monitor_level then (
00139     print(sconcat("M[",name,"]:"), "ENTRY (depth =", depth, ")."),
00140     print("F: ", statistics_cs(F))))$
00141 monitorcheck_osl_v(name) := if oklib_monitor then (
00142   if depth + 1 <= oklib_monitor_level then (
00143     print(sconcat("M[",name,"]:"), "depth:", depth,
00144           ", new best variable:", v, ", new min size:", min_size)))$
00145 
00146 /* For input F (a clause-set) returns a pair consisting of a splitting
00147    tree of minimum size, and its size (the number of nodes).
00148    The labels of inner nodes are variables.
00149 
00150    Monitoring shows the statistics of the input-clause-sets for the recursive
00151    calls of the procedure up to the depth given by oklib_monitor_level,
00152    and some basic information on the current best tree (for the recursive
00153    calls) once a branch was finished for depths up to oklib_monitor_level-1.
00154 */
00155 /* RENAME: optimal_st_cs */
00156 optimal_splitting_tree(F) :=
00157   optimal_splitting_tree_rec(F,0,2^(nvar_cs(F)+1)-1)$
00158 /* The recursive procedure, which also supplies an upper bound (an
00159    integer) which has to be improved, and if this is not possible
00160    then the empty list is returned. */
00161 optimal_splitting_tree_rec(F,depth,upperb) :=
00162  if upperb <= 0 then return([])
00163  elseif emptyp(F) then [[true],1]
00164  elseif has_empty_element(F) then [[false],1] else
00165   block([best_tree : [[]], min_size : inf, V : var_cs(F), break : false],
00166    monitorcheck_osl("optimal_splitting_tree"),
00167     for v in V unless break do
00168      block([osp0, osp1],
00169       if upperb <= 2 then (break : true, return()),
00170       osp0 : optimal_splitting_tree_rec(apply_pa({-v},F), depth+1, upperb-2),
00171       if osp0 = [] then return(),
00172       osp1 : optimal_splitting_tree_rec(apply_pa({v}, F), depth+1,
00173                                         upperb - osp0[2] - 1),
00174       if osp1 = [] then return(),
00175       block([new_size : osp0[2] + osp1[2] + 1],
00176        if new_size < min_size then (
00177          best_tree : [v, osp0[1], osp1[1]],
00178          min_size : new_size, upperb : min(upperb, min_size-1),
00179          monitorcheck_osl_v("optimal_splitting_tree")))),
00180     if best_tree = [[]] then return([]) else
00181       return([best_tree, min_size]))$
00182 
00183 
00184 /* ******************************
00185    * Evaluating splitting trees *
00186    ******************************
00187 */
00188 
00189 /* Counting the satisfying assignments in a splitting tree (relative to the set
00190    V of variables):
00191 */
00192 count_sat_st(st,V) := if st = [true] then 2^(length(V))
00193   elseif st = [false] then 0 else
00194   block([nV : disjoin(var_l(st[1]), V)],
00195     return(count_sat_st(st[2],nV) + count_sat_st(st[3],nV)))$
00196 
00197 /* Compute the satisfying (*partial*) assignments in a splitting tree.
00198    Returns a list which scans the true-leaves from left to right.
00199    If T is a splitting tree for clause-set F (as CNF), then the returned
00200    clause-set G (the setification of the returned list) is a hitting
00201    clause-set which as DNF is equivalent to F.
00202 */
00203 sat_pass_st(st) := sat_pass_st_a(st,{})$
00204 sat_pass_st_a(st,phi) := if st = [true] then [phi]
00205   elseif st = [false] then [] else
00206   append(sat_pass_st_a(st[2], adjoin(-st[1],phi)), sat_pass_st_a(st[3], adjoin(st[1],phi)))$
00207 /* Dually, compute the hitting clause-set (as a clause-list, scanning the
00208    tree from left to right) which (as CNF) represents the falsifying
00209    assignments.
00210 */
00211 usat_clauses_st(st) := usat_clauses_st_a(st,{})$
00212 usat_clauses_st_a(st,C) := if st = [false] then [C]
00213   elseif st = [true] then [] else
00214   append(usat_clauses_st_a(st[2], adjoin(st[1],C)), usat_clauses_st_a(st[3], adjoin(-st[1],C)))$
00215 
00216 
00217 /* Given a complete extended splitting tree for an unsatisfiable clause-set F,
00218    return a resolution tree (see Satisfiability/Lisp/Resolution/Proofs.mac for
00219    the definition of a resolution tree ("reslrt")):
00220 */
00221 st2reslrt_cs(st,F) := st2reslrt_cs_rel(st,{},F)$
00222 st2reslrt_cs_rel(st,phi,F) :=
00223   if length(st) = 1 then [first_element(analyse_pa(phi,F)[2])]
00224   else block([left_t : st2reslrt_cs_rel(st[2],adjoin(-st[1],phi),F),
00225               right_t : st2reslrt_cs_rel(st[3],adjoin(st[1],phi),F)],
00226     if elementp(st[1], left_t[1]) then
00227       if elementp(-st[1], right_t[1]) then
00228         [resolvent_l(left_t[1], right_t[1], st[1]), left_t, right_t]
00229       else right_t
00230     else left_t)$
00231 
00232 /* For a resolution-tree T compute the corresponding splitting-tree, using
00233    the resolution-literals as splitting literals, and positing false at
00234    the leaves:
00235 */
00236 reslrt2st(R) := if length(R)=1 then [false]
00237  else [resolution_literal(R[2][1],R[3][1]), reslrt2st(R[2]), reslrt2st(R[3])];
00238 
00239 /* Pruning a splitting-tree T w.r.t. a clause-set F, pruning unneccesary
00240    splittings: */
00241 treepruning_st(T,F) := reslrt2st(st2reslrt_cs(T,F))$
00242 
00243 
00244 /* ***********************************
00245    * Generators for splitting trees  *
00246    ***********************************
00247 */
00248 
00249 /* "Tree-variables": terms trv(path), where path is a path in a tree. */
00250 kill(trv)$
00251 declare(trv,noun)$
00252 declare(trv,posfun)$
00253 trv_var(v) := nounify(trv)(v)$
00254 
00255 /* The complete splitting tree of height k which is complete as tree and which
00256    has different tree-variables at each inner node.
00257    The corresponding tree-hitting clause-sets are exactly the uniform saturated
00258    minimally unsatisfiable clause-sets of deficiency 1; equivalently, exactly
00259    the unsatisfiable uniform regular hitting clause-sets.
00260 */
00261 complete_st_alldifferent(k) := complete_st_alldifferent_pref(k,[])$
00262 complete_st_alldifferent_pref(k,prefix) := if k = 0 then [false] else
00263   [trv_var(reverse(prefix)),
00264      complete_st_alldifferent_pref(k-1, cons(1,prefix)),
00265      complete_st_alldifferent_pref(k-1, cons(2,prefix))]$
00266 
00267 /* The complete splitting tree of height k and levelled height <= 1.
00268    The splitting-literals are variables trv(P), where P is the path to the
00269    current node; the false branches are the first branches.
00270    The corresponding tree-hitting clause-sets are exactly (up to isomorphism)
00271    the saturated minimally unsatisfiable Horn clause-sets.
00272 */
00273 /* RENAME: input_st */
00274 horn_st(k) := horn_st_pref(k,[])$
00275 horn_st_pref(k,prefix) := if k = 0 then [false] else
00276   [trv_var(reverse(prefix)), [false], horn_st_pref(k-1, cons(2,prefix))]$
00277 /* The variation where the list L of splitting-literals, starting from the
00278    root, together with the base-tree b, is given: */
00279 input_list_st(L,b) := if emptyp(L) then b else
00280   [first(L), [false], input_list_st(rest(L),b)]$
00281 
00282 /* More generally, the complete splitting tree of height k >= 0 and levelled
00283    height l >= 0 (if l=0 then k=0, else k is arbitrary), using different
00284    variables for all (inner) nodes:
00285 */
00286 genhorn_st(k,l) := genhorn_st_pref(k,l,[])$
00287 genhorn_st_pref(k,l,prefix) := if l=0 or k=0 then [false]
00288  elseif l=1 then horn_st_pref(k,prefix)
00289  else [trv_var(reverse(prefix)),
00290        genhorn_st_pref(k-1,l-1,cons(1,prefix)),
00291        genhorn_st_pref(k-1, l, cons(2,prefix))]$
00292 /* Remark: For the corresponding tree-hitting clause-sets see smusat_genhorn_cs
00293    in Satisfiability/Lisp/ConflictCombinatorics/HittingClauseSets.mac.
00294 */
00295 /* The satisfiable extensions, extending each leaf of genhorn_st(k,l) by
00296    one sat-branch:
00297 */
00298 genhornsat_st(k,l) := genhornsat_st_pref(k,l,[])$
00299 genhornsat_st_pref(k,l,prefix) :=
00300  if l=0 or k=0 then [trv_var(reverse(prefix)),[false],[true]]
00301  else [trv_var(reverse(prefix)),
00302        genhornsat_st_pref(k-1,l-1,cons(1,prefix)),
00303        genhornsat_st_pref(k-1, l, cons(2,prefix))]$
00304 
00305 
00306 /* ***********************
00307    * r_k splitting trees *
00308    ***********************
00309 */
00310 
00311 /*
00312  A "boolean r_k-splitting tree" for a clause-set F is either
00313   - [[]] for "nothing done",
00314   - or [false] in case r_k(F) = {{}},
00315   - or [true] in case r_k(F) = {},
00316   - or [x, T0, T1], where x is a boolean literal and
00317     T0/1 is a r_k-splitting tree of <x -> 0/1> * r_k(F).
00318 */
00319 /*
00320  So splitting trees are exactly the r_0-splitting trees.
00321 */
00322 
00323 /*
00324  A boolean r_k-splitting tree is complete iff no leaf is [[]].
00325 */
00326 
00327 /* For input F (a clause-set) returns a pair consisting of a r_k-splitting
00328    tree of minimum size, and its size.
00329    Splitting literals are always splitting variables.
00330 */
00331 optimal_r_splitting_tree(F,k) := block(
00332  [name : sconcat("optimal_r_splitting_tree(",k,")")],
00333  optimal_r_splitting_tree_rec(F,k,0,2^(nvar_cs(F)+1)-1))$
00334 optimal_r_splitting_tree_rec(F,k,depth,upperb) :=
00335  if upperb <= 0 then return([]) else
00336  block([Fr : generalised_ucp(F,k)],
00337   if Fr = {} then return([[true],1])
00338   elseif Fr = {{}} then return([[false],1]) else
00339    block([best_tree : [[]], min_size : inf, V : var_cs(Fr), break : false],
00340     monitorcheck_osl(name),
00341      for v in V unless break do
00342       block([osp0, osp1],
00343        if upperb <= 2 then (break : true, return()),
00344        osp0 : optimal_r_splitting_tree_rec(apply_pa({-v}, Fr),k, depth+1,
00345                                            upperb-2),
00346        if osp0 = [] then return(),
00347        osp1 : optimal_r_splitting_tree_rec(apply_pa({v}, Fr),k,depth+1,
00348                                            upperb - osp0[2] - 1),
00349        if osp1 = [] then return(),
00350        block([new_size : osp0[2] + osp1[2] + 1],
00351         if new_size < min_size then (
00352           best_tree : [v, osp0[1], osp1[1]],
00353           min_size : new_size, upperb : min(upperb, min_size-1),
00354           monitorcheck_osl_v(name)))),
00355     if best_tree = [[]] then return([]) else
00356       return([best_tree, min_size])))$
00357 
00358 /*
00359  An "amended r_k-splitting tree" has as labels for the non-leaf-nodes
00360  pairs [x,phi], where phi is the partial assignment yielding the
00361  reduced clause-set associated to the node, that is, phi applied to the
00362  unreduced clause-set associated with the node yields
00363  the reduced clause-set.
00364  The unreduced clause-set associated with the root is the input,
00365  while otherwise it is the branching assignment (just one variable
00366  involving) applied to the reduced clause-set associated with the
00367  parent node.
00368  Accordingly leaf-nodes are labelled with pairs [true/false,phi].
00369 */
00370 
00371 /* Given a clause-set F and an r_k-splitting tree T for F, compute
00372    the amended r_k-splitting tree.
00373 */
00374 amend_r_splitting_tree(F,T,k) := block(
00375   [x : T[1], Fr : generalised_ucp_pa(F,k)],
00376   if length(T) = 1 then return([[x,Fr[2]]])
00377   else block([
00378     T0 : amend_r_splitting_tree(apply_pa({-x},Fr[1]), T[2], k),
00379     T1 : amend_r_splitting_tree(apply_pa({x},Fr[1]), T[3], k)],
00380     return([[x,Fr[2]], T0, T1])))$
00381 
00382 /* Transforming an r_k-splitting tree T for F into a splitting tree for F: */
00383 rst2st(F,T,k) := fst2st(rst2est(F,T,k),F)$
00384 /* Expanding the r_k-steps (obtaining an extended splitting tree): */
00385 rst2est(F,T,k) :=
00386  if k=0 then T
00387  elseif k=1 then block([x : T[1], redres : ucp_lpa_0_cs(F), Fr, phi],
00388    Fr : redres[1],
00389    phi : lappend(map(listify,redres[2])),
00390    if length(T)=1 then input_list_st(phi, [x]) else
00391    input_list_st(phi, [x,rst2est(apply_pa_cs({-x},Fr),T[2],k),
00392                          rst2est(apply_pa_cs({x},Fr),T[3],k)]))
00393  else unknown$ /* not yet implemented */
00394 
00395 
00396 /* **********
00397    * Output *
00398    **********
00399 */
00400 
00401 oklib_plain_include("stringproc")$
00402 
00403 /* Output a splitting tree st as latex-ps-tree to stream s: */
00404 tex_st(s,st) := if st = [true] then printf(s, "~a", "\\TC")
00405   elseif st = [false] then printf(s, "~a", "\\Tdot")
00406   else (
00407      printf(s, "~a~a~a", "\\pstree{\\TR{$", st[1], "$}}"),
00408      printf(s, "{"), tex_st(s, st[2]), tex_st(s, st[3]), printf(s, "}")
00409 )$
00410 
00411 /* Output a splitting tree st as latex-ps-tree to a file with name n: */
00412 tex_st_f(n, st) := (block[s : openw(n)], tex_st(s, st), close(s))$
00413 
00414 /* Output a resolution tree rt as latex-ps-tree to stream s: */
00415 tex_rt(s,rt) := if length(rt) = 1 then printf(s, "~a~a~a", "\\TR{$\\set", rt[1], "$}")
00416   else (
00417      printf(s, "~a~a~a", "\\pstree{\\TR{$\\set", rt[1], "$}}"),
00418      printf(s, "{"), tex_rt(s, rt[2]), tex_rt(s, rt[3]), printf(s, "}")
00419 )$
00420 
00421 /* Output a resolution tree st as latex-ps-tree to a file with name n: */
00422 tex_rt_f(n, rt) := (block[s : openw(n)], tex_rt(s, rt), close(s))$
00423