OKlibrary  0.2.1.6
DLL_solvers.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 24.12.2007 (Swansea) */
00002 /* Copyright 2007, 2008, 2009, 2010, 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 
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00025 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Hypergraphs.mac")$
00026 oklib_include("OKlib/ComputerAlgebra/Graphs/Lisp/Basic.mac")$
00027 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/Statistics.mac")$
00028 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Counting/InclusionExclusion.mac")$
00029 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Reductions/GeneralisedUCP.mac")$
00030 oklib_include("OKlib/ComputerAlgebra/DataStructures/Lisp/Lists.mac")$
00031 oklib_include("OKlib/ComputerAlgebra/Trees/Lisp/Basics.mac")$
00032 
00033 
00034 /* **********************************
00035    * Backtracking without reduction *
00036    **********************************
00037 */
00038 
00039 /* The simplest scheme: input is a formal clause-set FF, and the return value
00040    is true or false.
00041    The heuristics h gets as input a formal clause-set, which is neither empty
00042    nor contains the empty clause, and has to return either 0 in case the input
00043    was determined unsatisfiable, or a literal where then this literal is first
00044    set to true. */
00045 
00046 dll_simplest(FF, h) := if emptyp(FF[2]) then true
00047  elseif empty_element_p(FF[2]) then false
00048  else block([x : h(FF)], 
00049     if x=0 then return(false) else
00050     return(dll_simplest(apply_pa_fcs({x}, FF), h) or 
00051            dll_simplest(apply_pa_fcs({-x}, FF), h)))$
00052 
00053 /* The variation where instead of "true" a satisfying partial assignment is
00054    returned: */
00055 dll_simplest_spa(FF,h) := if emptyp(FF[2]) then {}
00056  elseif empty_element_p(FF[2]) then false
00057  else block([x : h(FF), res],
00058     if x=0 then return(false),
00059     res : dll_simplest_spa(apply_pa_fcs({x}, FF), h),
00060     if res # false then return(adjoin(x,res)),
00061     res : dll_simplest_spa(apply_pa_fcs({-x}, FF), h),
00062     if res # false then return(adjoin(-x,res)) else 
00063       return(false))$
00064 
00065 /* The variation where the return value is the computed (complete) splitting
00066    tree (representing now all solutions): */
00067 dll_simplest_st(FF, h) := if emptyp(FF[2]) then [true]
00068  elseif empty_element_p(FF[2]) then [false]
00069  else block([x : h(FF)],
00070     if x=0 then return([false]) else
00071     return([-x,
00072             dll_simplest_st(apply_pa_fcs({x}, FF), h),
00073             dll_simplest_st(apply_pa_fcs({-x}, FF), h)]))$
00074 
00075 
00076 /* ***********************************
00077    * Backtracking with r_k-reduction *
00078    ***********************************
00079 */
00080 
00081 /* ATTENTION: In the following the heuristic is not yet allowed to return 0;
00082    likely this should be updated.
00083 */
00084 
00085 monitorcheck_dll(name,red) := if oklib_monitor then (
00086   print(sconcat("M[",name,"]:"), "Entry (reduction =", red, ")."),
00087     print("F: ", statistics_fcs(FF)),
00088     print("Fr: ", statistics_fcs(cs_to_fcs(Fr))))$
00089 
00090 dll_rk(FF, h, k) := block([Fr : generalised_ucp(FF[2],k)],
00091   monitorcheck_dll("dll_rk",k),
00092   if emptyp(Fr) then true
00093   elseif empty_element_p(Fr) then false
00094   else block([V : var_cs(Fr)], block([x : h([V,Fr])],
00095     return(dll_rk(apply_pa_f({x}, [V,Fr]), h, k) 
00096            or dll_rk(apply_pa_f({-x}, [V,Fr]), h, k)))))$
00097 
00098 /* The variation where the return value is the computed r_k-splitting tree. */
00099 dll_rk_st(FF, h, k) := block([Fr : generalised_ucp(FF[2],k)],
00100   monitorcheck_dll("dll_rk_st",k),
00101   if emptyp(Fr) then [true]
00102   elseif empty_element_p(Fr) then [false]
00103   else block([V : var_cs(Fr)], block([x : h([V,Fr])], 
00104     return([-x,
00105             dll_rk_st(apply_pa_f({x}, [V,Fr]), h, k),
00106             dll_rk_st(apply_pa_f({-x}, [V,Fr]), h, k)]))))$
00107 
00108 
00109 /* *****************************************
00110    * Backtracking with arbitrary reduction *
00111    *****************************************
00112 */
00113 
00114 
00115 /* the reduction takes a clause-set and returns a clause-set */
00116 dll_red(FF, h, red) := block([Fr : red(FF[2])],
00117   monitorcheck_dll("dll_red", red),
00118   if emptyp(Fr) then true
00119   elseif empty_element_p(Fr) then false
00120   else block([V : var_cs(Fr)], block([x : h([V,Fr])], 
00121     return(dll_red(apply_pa_f({x}, [V,Fr]), h, red) 
00122            or dll_red(apply_pa_f({-x}, [V,Fr]), h, red)))))$
00123 
00124 /* dll_red(FF, h, lambda([F], generalised_ucp(F,k))) = dll_rk(FF, h, k) */
00125 
00126 /* The variation where the return value is the computed r-splitting tree. */
00127 dll_red_st(FF, h, red) := block([Fr : red(FF[2])],
00128   monitorcheck_dll("dll_red_st", red),
00129   if emptyp(Fr) then [true]
00130   elseif empty_element_p(Fr) then [false]
00131   else block([V : var_cs(Fr)], block([x : h([V,Fr])], 
00132     return([-x,
00133             dll_red_st(apply_pa_f({x}, [V,Fr]), h, red),
00134             dll_red_st(apply_pa_f({-x}, [V,Fr]), h, red)]))))$
00135 
00136 /* Amend the splitting tree with the distances used by the heuristics;
00137    so this time the "amended heuristics" returns a pair [x,L],
00138    and non-leaf-nodes a labelled with pairs [x,L], while
00139    leaf-nodes are still just labelled with [true] or [false].
00140    Here L is the list of distance-pairs used by the heuristic.
00141 
00142    So such an "amended splitting tree" ("ast") has as labels at
00143    inner nodes pairs [x,L], where x is the splitting literal, while L is the
00144    list of pairs of distances (each pair handling the two branches) for the
00145    distance functions (used for tie-breaking: if the projections
00146    of the first pairs are equal, consider the second pair etc.).
00147 */
00148 dll_red_st_dist(FF, ah, red) := block([Fr : red(FF[2])],
00149   monitorcheck_dll("dll_red_st_dist", red),
00150   if emptyp(Fr) then [true]
00151   elseif empty_element_p(Fr) then [false]
00152   else block([V : var_cs(Fr)], block([H : ah([V,Fr]), x], 
00153     x : H[1],
00154     return([[-x, map(reverse, H[2])],
00155             dll_red_st_dist(apply_pa_f({x}, [V,Fr]), ah, red),
00156             dll_red_st_dist(apply_pa_f({-x}, [V,Fr]), ah, red)]))))$
00157 
00158 
00159 /* *******************************
00160    * Simple heuristics for DLL   *
00161    *******************************
00162 */
00163 
00164 /* *** Heuristics aiming at small trees *** */
00165 
00166 /* The simplest heuristics: return the first variable. */
00167 dll_heuristics_first_formal(FF) := first(FF[1])$
00168 
00169 /* Instantiations of SAT solvers: */
00170 dll_simplest_trivial1(FF) := dll_simplest(FF, dll_heuristics_first_formal)$
00171 dll_simplest_spa_trivial1(FF) := dll_simplest_spa(FF, dll_heuristics_first_formal)$
00172 dll_simplest_st_trivial1(FF) := dll_simplest_st(FF, dll_heuristics_first_formal)$
00173 dll_rk_trivial1(FF,k) := dll_rk(FF, dll_heuristics_first_formal, k)$
00174 dll_rk_st_trivial1(FF,k) := dll_rk_st(FF, dll_heuristics_first_formal, k)$
00175 
00176 
00177 /* The second-simplest heuristics: return the literal of the first
00178    literal-occurrence. */
00179 dll_heuristics_first_real(FF) := first(first(FF[2]))$
00180 
00181 /* Instantiations of SAT solvers: */
00182 dll_simplest_trivial2(FF) := dll_simplest(FF, dll_heuristics_first_real)$
00183 dll_simplest_spa_trivial2(FF) := dll_simplest_spa(FF, dll_heuristics_first_real)$
00184 dll_simplest_st_trivial2(FF) := dll_simplest_st(FF, dll_heuristics_first_real)$
00185 dll_rk_trivial2(FF,k) := dll_rk(FF, dll_heuristics_first_real, k)$
00186 dll_rk_st_trivial2(FF,k) := dll_rk_st(FF, dll_heuristics_first_real, k)$
00187 
00188 
00189 /* Heuristics: first literal in first shortest clause */
00190 dll_heuristics_first_shortest_clause(FF) := block([ml : inf, x],
00191  for C in FF[2] do if length(C) < ml then (ml : length(C), x : first(C)),
00192   return(x))$
00193 
00194 /* Instantiations of SAT solvers: */
00195 dll_simplest_first_shortest_clause(FF) := dll_simplest(FF, dll_heuristics_first_shortest_clause)$
00196 dll_simplest_st_first_shortest_clause(FF) := dll_simplest_st(FF, dll_heuristics_first_shortest_clause)$
00197 dll_rk_first_shortest_clause(FF,k) := dll_rk(FF, dll_heuristics_first_shortest_clause, k)$
00198 dll_rk_st_first_shortest_clause(FF,k) := dll_rk_st(FF, dll_heuristics_first_shortest_clause, k)$
00199 
00200 
00201 /* The first variable in the first shortest positive clause: */
00202 dll_heuristics_first_shortest_positive_clause(FF) := block([ml : inf, x : 0],
00203  for C in FF[2] do if posp_c(C) and length(C) < ml then
00204   (ml : length(C), x : first(C)),
00205  x)$
00206 
00207 /* Instantiations of SAT solvers: */
00208 dll_simplest_first_shortest_positive_clause(FF) := dll_simplest(FF, dll_heuristics_first_shortest_positive_clause)$
00209 dll_simplest_st_first_shortest_positive_clause(FF) := dll_simplest_st(FF, dll_heuristics_first_shortest_positive_clause)$
00210 dll_rk_first_shortest_positive_clause(FF,k) := dll_rk(FF, dll_heuristics_first_shortest_positive_clause, k)$
00211 dll_rk_st_first_shortest_positive_clause(FF,k) := dll_rk_st(FF, dll_heuristics_first_shortest_positive_clause, k)$
00212 
00213 
00214 /* Heuristics: choose a variable occurring most often, and choose the sign
00215    first which satisfies most clauses.
00216 */
00217 
00218 dll_heuristics_max_var(FF) := block(
00219  [v : max_variable_degree_v_cs(FF[2])[2]],
00220  if literal_degree_cs(FF[2],v) >= literal_degree_cs(FF[2],-v) then
00221    return(v) else return(-v))$
00222 
00223 /* Instantiations of SAT solvers: */
00224 dll_simplest_max_var(FF) := dll_simplest(FF, dll_heuristics_max_var)$
00225 dll_simplest_st_max_var(FF) := dll_simplest_st(FF, dll_heuristics_max_var)$
00226 dll_rk_max_var(FF,k) := dll_rk(FF, dll_heuristics_max_var, k)$
00227 dll_rk_st_max_var(FF,k) := dll_rk_st(FF, dll_heuristics_max_var, k)$
00228 
00229 
00230 /* For comparison: choose variable occurring least often, and choose sign
00231    first which satisfies fewest clauses:
00232 */
00233 
00234 dll_heuristics_min_var(FF) := block(
00235  [v : min_variable_degree_v_cs(FF[2])[2]],
00236  if literal_degree_cs(FF[2],v) >= literal_degree_cs(FF[2],-v) then
00237    return(v) else return(-v))$
00238 
00239 /* Instantiations of SAT solvers: */
00240 dll_simplest_min_var(FF) := dll_simplest(FF, dll_heuristics_min_var)$
00241 dll_simplest_st_min_var(FF) := dll_simplest_st(FF, dll_heuristics_min_var)$
00242 dll_rk_min_var(FF,k) := dll_rk(FF, dll_heuristics_min_var, k)$
00243 dll_rk_st_min_var(FF,k) := dll_rk_st(FF, dll_heuristics_min_var, k)$
00244 
00245 
00246 /* *** Heuristics for a good representation of the set of satisfying
00247    assignments (thus "satisfiability-driven"). *** */
00248 
00249 /* Given an approximation A for SAT-probability, returns the heuristics,
00250    which chooses the literal maximising A(<x -> 1> * FF). At least one 
00251    literal x must yield a value A > minf. */
00252 /* MG: Could some of this not be generalised to some sort of  maximise(f) 
00253    function? */
00254 choose_most_sat_literal_h(A) := buildq([A], lambda([FF],
00255   block([L : literals_v(FF[1]), opta : minf, optx],
00256     for x in L do block([a : A(apply_pa_f({x}, FF))],
00257       if a > opta then (opta : a, optx : x)),
00258     return(optx))))$
00259 
00260 johnson_heuristic : choose_most_sat_literal_h(satprob_hitting_f)$
00261 
00262 
00263 /* Heuristics: choose a literal occurring most often;
00264    in case of ties, the return value is implementation-defined. */
00265 dll_heuristics_max_lit(FF) := max_literal_degree_l_cs(FF[2])[2]$
00266 
00267 dll_simplest_max_lit(FF) := dll_simplest(FF, dll_heuristics_max_lit)$
00268 dll_simplest_st_max_lit(FF) := dll_simplest_st(FF, dll_heuristics_max_lit)$
00269 dll_rk_max_lit(FF,k) := dll_rk(FF, dll_heuristics_max_lit, k)$
00270 dll_rk_st_max_lit(FF,k) := dll_rk_st(FF, dll_heuristics_max_lit, k)$
00271 
00272 
00273 /* Heuristics: choose a literal occurring most often and do additional
00274    "lookahead" to try to avoid ties (hence tb "tie break"). */
00275 /* Returns a literal with the maximum literal degree from the given clause-set
00276    using lookahead up to depth d, considering n tied literals at each stage if
00277    ties occur for a maximum literal. */
00278 dll_heuristics_max_lit_tb(d,n) :=
00279   buildq([d,n],lambda([FF],max_literal_degree_tb_l_cs(FF,d,n)[1]))$
00280 
00281 
00282 /* ****************************
00283    * Heuristics via distances *
00284    ****************************
00285 */
00286 
00287 /* Heuristics scheme given by a list of distances and projections (for 
00288    lexicographical ordering in case of ties) and an approximation of
00289     satisfiability probability; look-ahead by reduction r (a map from
00290     clause-sets to clause-sets). */
00291 /* If the distance yields <= 0 then the whole branching is disqualified,
00292    if the distance yields infinity, then this branching is chosen 
00293    immediately. */
00294 /* A projection is the better the smaller. Inputs are positive and
00295    not infinity, and the same for the output. */
00296 /* If there are less projections than distances, then the last projection
00297    is reused. */
00298 
00299 /* A helper-function which determines whether a value evaluates to inf.
00300    Ignores presence of minf; Maxima evaluates 0*inf to 0. */
00301 equivinfp(x) := is(not freeof(inf, x))$
00302 
00303 /* A helper-function for evaluating a branching variable:
00304    Using dynamic binding for F, F1, F0 and v. */
00305 evaluating_branching_variable(d) := block([x,d0,d1],
00306   x : v, d1 : d(F, F1),
00307   if equivinfp(d1) then return([x])
00308   elseif d1 <= 0 then return([]) else (
00309     x : -v, d0 : d(F, F0),
00310     if equivinfp(d0) then (return([x]))
00311     elseif d0 <= 0 then return([])
00312     else return([d1,d0])))$
00313 
00314 /* Helper-function for lexicographical ordering of lists:
00315    returns true if A < B */
00316 lexicographical_orderp(A,B) :=
00317   if A = [] then if B = [] then false else true
00318   elseif B = [] then false
00319   elseif A[1] < B[1] then true
00320   elseif A[1] > B[1] then false
00321   else lexicographical_orderp(rest(A),rest(B))$
00322 
00323 monitorcheck_hld(name) := if oklib_monitor then (
00324   print(sconcat("M[",name,"]:"), "immediate:", immediate, ", best_proj:", best_proj))$
00325 monitorcheck_hld_v(name) := if oklib_monitor then (
00326   if oklib_monitor_level >= 1 then (
00327     print(sconcat("M[",name,"]: LOOP "),  "variable:", v, ", immediate:", immediate, ", ignore:", ignore, ", distances:", D)))$
00328 
00329 heuristics_lookahead_distances(r, distances, projections, satprob) :=
00330  block([nd : length(distances), np : length(projections)],
00331   buildq([r, distances, projections, satprob, nd, np], lambda([FF],
00332    block(
00333     [F : FF[2], best_var, branch_lit, best_proj : [inf], immediate : false, Fbest],
00334     for v in FF[1] unless immediate do 
00335      block([E, F0,F1, D : [], P : [], ignore : false],
00336       F1 : r(apply_pa({v},F)), F0 : r(apply_pa({-v},F)),
00337       for i : 1 thru nd do (
00338         E : evaluating_branching_variable(distances[i]),
00339         if length(E) = 0 then (ignore : true, return(false)),
00340         if length(E) = 1 then (
00341           branch_lit : E[1], immediate : true, return(false)
00342         ),
00343         D : endcons(E,D)
00344       ),
00345       monitorcheck_hld_v("heuristics_lookahead_distances"),
00346       if ignore or immediate then return(false),
00347       for i : 1 thru nd do block([p : projections[min(np,i)]],
00348         P : endcons(p(D[i][1], D[i][2]), P)),
00349       if lexicographical_orderp(P, best_proj) then (
00350         best_proj : P, best_var : v, Fbest : [F1,F0]
00351       )
00352     ),
00353     monitorcheck_hld("heuristics_lookahead_distances"),
00354     if immediate then return(branch_lit),
00355     if best_proj = [inf] then
00356       error("heuristics_lookahead_distances: all variables disabled!"),
00357     if satprob(Fbest[1]) >= satprob(Fbest[2]) then return(best_var)
00358     else return(-best_var)
00359    ))))$
00360 
00361 /* The amended variation, returning the list of associated distances;
00362    additionally a list of monitoring distances can be specified.
00363    For the list of distances returned at a node, the number of "deciding"
00364    distances can vary if inf-values occur, however there are always
00365    length(mon_distances) many monitoring-distances. */
00366 amended_heuristics_lookahead_distances(r, distances, projections, satprob, mon_distances) :=
00367  block([nd : length(distances), np : length(projections), nm : length(mon_distances)],
00368   buildq([r, distances, projections, satprob, mon_distances, nd, np, nm], lambda([FF],
00369    block(
00370     [F : FF[2], best_var, branch_lit, best_proj : [inf], immediate : false, Fbest, best_dist],
00371     for v in FF[1] unless immediate do 
00372      block([E, F0,F1, D : [], P : [], ignore : false],
00373       F1 : r(apply_pa({v},F)), F0 : r(apply_pa({-v},F)),
00374       for i : 1 thru nd do (
00375         E : evaluating_branching_variable(distances[i]),
00376         if length(E) = 0 then (ignore : true, return(false)),
00377         if length(E) = 1 then (
00378           branch_lit : E[1], immediate : true,
00379           if branch_lit > 0 then E : [inf,0] else E : [0,inf],
00380           best_dist : endcons(E,D),
00381           Fbest : [F1,F0],
00382           return(false)
00383         ),
00384         D : endcons(E,D)
00385       ),
00386       monitorcheck_hld_v("amended_heuristics_lookahead_distances"),
00387       if ignore or immediate then return(false),
00388       for i : 1 thru nd do block([p : projections[min(np,i)]],
00389         P : endcons(p(D[i][1], D[i][2]), P)),
00390       if lexicographical_orderp(P, best_proj) then (
00391         best_proj : P, best_var : v, Fbest : [F1,F0], best_dist : D
00392       )
00393     ),
00394     monitorcheck_hld("amended_heuristics_lookahead_distances"),
00395     for i : 1 thru nm do block([md : mon_distances[i]],
00396       best_dist : endcons([md(F,Fbest[1]),md(F,Fbest[2])], best_dist)),
00397     if not immediate then (
00398       if best_proj = [inf] then
00399         error("heuristics_lookahead_distances: all variables disabled!"),
00400       if satprob(Fbest[1]) >= satprob(Fbest[2]) then 
00401         branch_lit : best_var 
00402       else
00403         branch_lit : -best_var
00404     ),
00405     if branch_lit < 0 then best_dist : map(reverse, best_dist),
00406     return([branch_lit, best_dist])
00407    ))))$
00408 
00409 
00410 /* For an amended splitting tree T ("ast"), extract the tree labelled
00411    with distances (pairs of real numbers, at inner nodes; formally a
00412    tree with branching tuples, that is, "tbt") given by the 
00413    ith distance function:
00414 */
00415 ast2tbt(T,i) :=
00416   if length(T)=1 then T else
00417   cons(T[1][2][i], map(lambda([t],ast2tbt(t,i)), rest(T)))$
00418 
00419 /* Check that inf-branches of an ast T are trivial, using the number m of 
00420    monitoring distances (which are to be ignored); returns the empty list
00421    if for every inner node with some pair of distances containing inf
00422    the corresponding branches lead directly to a leaf, while otherwise for the
00423    first offending nodes from the root the appended lists containing the
00424    (amended) node-label, the list of branch-indices (either 1 or 2) where
00425    at least one of the two branches is inf, and the number of nodes in these
00426    inf-subtrees is returned. If there are two relevant pairs containing a
00427    distance inf, then false is returned.
00428    The motivation is as follows: The m distance-pairs at the end of the
00429    list of distance-pairs are just computed for monitoring, and otherwise
00430    ignored. Now a distance inf must mean, that following the corresponding
00431    branch will lead to an immediate decision --- it is assumed that
00432    the DLL-solver chooses immediately this "shortcut", without further
00433    investigating the other distances.
00434 */
00435 check_inf_branches_ast(T,m) := block([l : length(T), rel_distances, inf_ind],
00436   if l = 1 then return([]),
00437   rel_distances : rest(T[1][2],-m),
00438   inf_ind : sublist_indices(rel_distances, lambda([d], member(inf,d))),
00439   if not emptyp(inf_ind) then (
00440     if length(inf_ind) # 1 then return(false),
00441     inf_ind : sublist_indices(rel_distances[inf_ind[1]], lambda([x],is(x=inf))),
00442     if not every_s(lambda([i], is(nnds_lrt(T[1+i]) = 1)), inf_ind) then
00443       return(append([T[1], inf_ind], create_list(nnds_lrt(T[1+i]),i,inf_ind)))
00444   ),
00445   return(lappend(map(lambda([T2],check_inf_branches_ast(T2,m)), rest(T)))))$
00446 
00447 /* Counts nodes containing some inf-distance-value */
00448 count_inf_branches(T,m) := block([l : length(T), flag : 0],
00449   if l = 1 then return(0),
00450   if not emptyp(sublist_indices(rest(T[1][2],-m), lambda([d], member(inf,d))))
00451     then flag : 1,
00452   return(flag + sum(count_inf_branches(T[i],m),i,2,l)))$
00453 
00454 /* Collapses nodes where all branches except of one are inf-branches
00455    (such nodes are hidden reductions); m is the number of monitoring
00456    distances (to be ignored, as with check_inf_branches_ast; it is assumed 
00457    that not both branches are inf-branches): */
00458 /* RENAME: collapse_inf_branches_ast */
00459 collapse_inf_branches(T,m) := block(
00460   [l : length(T), rel_distances, inf_ind, other],
00461   if l = 1 then return(T),
00462   rel_distances : rest(T[1][2],-m),
00463   inf_ind : sublist_indices(rel_distances, lambda([d], member(inf,d))),
00464   if not emptyp(inf_ind) then (
00465     inf_ind : sublist_indices(rel_distances[inf_ind[1]],lambda([x],is(x=inf))),
00466     if length(inf_ind) = l-2 then (
00467       other : listify(setdifference(setmn(1,l-1),setify(inf_ind)))[1],
00468       T : T[1+other],
00469       return(collapse_inf_branches(T,m)))
00470   ),
00471   return(cons(T[1], map(lambda([T2],collapse_inf_branches(T2,m)), rest(T)))))$
00472 collapse_inf_branches_ast(T,m) := collapse_inf_branches(T,m)$
00473 
00474 
00475 /* *************
00476    * Distances *    
00477    *************
00478 */
00479 
00480 /* Distances have as input two clause-sets Ffrom, Fto,
00481    and return a real number or inf.
00482 */
00483 
00484 /* The trivial distance */
00485 trivial_distance(Ffrom,Fto) := 1$
00486 
00487 /* The difference in the number of variables */
00488 delta_n(Ffrom,Fto) := nvar_cs(Ffrom) - nvar_cs(Fto)$
00489 
00490 /* The difference in the number of clauses */
00491 delta_c(Ffrom,Fto) := ncl_cs(Ffrom) - ncl_cs(Fto)$
00492 
00493 /* The difference in the number of literal occurrences */
00494 delta_l(Ffrom,Fto) := nlitocc_cs(Ffrom) - nlitocc_cs(Fto)$
00495 
00496 /* The scheme for the weighted number of new clauses (wf, the
00497    weight function, takes natural numbers >= 2 as inputs (the clause-lengths),
00498    and returns positive real numbers). */
00499 wn_newclauses(wf) := buildq([wf], lambda([Ffrom,Fto],
00500   block([nC : listify(setdifference(Fto, Ffrom))],
00501     return(sum(wf(length(nC[i])),i,1,length(nC))))))$
00502 /* The variation of wn_newclauses where instances of 2-CLS are detected: */
00503 wn_newclauses_2(wf)  := buildq([wf], lambda([Ffrom,Fto],
00504   if max_rank_cs(Fto) <= 2 then inf else
00505    block([nC : listify(setdifference(Fto, Ffrom))],
00506     return(sum(wf(length(nC[i])),i,1,length(nC))))))$
00507 
00508 /* Just the number of new clauses of length k */
00509 n_newclauses(k) := buildq([k], lambda([Ffrom,Fto],
00510   length(setdifference(scls_k(Fto,k), scls_k(Ffrom,k)))))$
00511 
00512 
00513 /* ***************
00514    * Projections *
00515    ***************
00516 */
00517 
00518 /* For binary clauses: */
00519 
00520 /* We have tau2. */
00521 
00522 prod_proj(x,y) := 1/(x*y)$
00523 
00524 
00525 /* *********************************
00526    * Satisfiability approximations *
00527    *********************************
00528 */
00529 
00530 /* These "approximations" are just real numbers, and the greater the
00531    higher the probability of satisfiability.
00532    The value inf says the formula is surely satisfiable, the value
00533    minf says the forrmula is surely unsatisfiable.
00534 */
00535 
00536 /* The trivial approximation of satprob(F) ("approximation of order 0") */
00537 trivial_sat_approx(F) := 1$
00538 
00539 /* The first-order approximation of satprob(F) (a lower bound on the true
00540    probability), increased to inf if sat is established */
00541 firstorder_sat_approx(F) := block([a : satprob_hitting(F)],
00542  if a > 0 then return(inf) else return(a))$
00543 
00544 /* The logarithm of the probability that a random assignment over the 
00545    variables in the given clause-set satisfies a random clause-set 
00546    drawn with the same number of clauses of the same lengths as the
00547    given clause-set. */
00548 /* With the exception that log(1) = 0 is translated to inf. */
00549 /* See probsatrand in
00550 ComputerAlgebra/Satisfiability/Lisp/Counting/RandomClauseSets.mac. */
00551 logprobrand(F) := if F = {} then inf else 
00552  block([L : ncl_list_cs(F)],
00553   if L[1][1] = 0 then return(minf) else
00554   return(sum(L[i][2] * float(log(1-2^(-L[i][1]))), i, 1, length(L))))$
00555 
00556 /* The reciprocal maximum over all clauses C of the sums of 2^(-|D|) over 
00557    neighbours D of C in the common-variable graph, as motivated by
00558    the asymetric local lemma of Lovasz. */
00559 /* Compare with locallemma_sattest_asymmetric in
00560    ComputerAlgebra/Satisfiability/Lisp/Counting/Degrees.mac. */
00561 locallemma_satapprox(F) := if F = {} then inf else 
00562   if empty_element_p(F) then minf else 
00563    block([G : g2mg(cvg_cs(F)), m : 0, c],
00564     c : graph_order(G),
00565     for i : 1 thru c do block([N : neighbors(i, G), s : 0],
00566       for j in N do
00567         s : s + 2^(-length(get_vertex_label(j,G))),
00568       m : max(m,s)),
00569     if m = 0 then return(inf)
00570     elseif m <= 1/4 then return(inf)
00571     else return(1/m))$
00572 
00573 /* As in [Hooker, Vinai, 1995], the variation of locallemma_satapprox
00574    using the sum instead of the max. */
00575 locallemmasum_satapprox(F) := if F = {} then inf else 
00576   if empty_element_p(F) then minf else 
00577    block([G : g2mg(cvg_cs(F)), S : 0, c],
00578     c : graph_order(G),
00579     for i : 1 thru c do block([N : neighbors(i, G), s : 0],
00580       for j in N do
00581         s : s + 2^(-length(get_vertex_label(j,G))),
00582       S : S + s),
00583     if S = 0 then return(inf)
00584     else return(1/S))$
00585 
00586 
00587 /* ******************************************
00588    * Current (best) solvers at Maxima level *
00589    ******************************************
00590 */
00591 
00592 /*
00593   "Best" here means only that for the small(!) tasks at Maxima-level
00594   it currently seems most appropriate.
00595 
00596   When a SAT solver is needed, but is just instrumental, then the "current"
00597   solvers provided here shall be used (using dynamic scoping when for
00598   special circumstances a different solver shall be used).
00599 */
00600 
00601 /* Standard solver (input a formal clause-set, output true or false): */
00602 current_satsolver : dll_simplest_first_shortest_clause$
00603 /* Now returning a (complete) splitting tree: */
00604 current_satsolver_st : dll_simplest_st_max_lit$
00605