OKlibrary  0.2.1.6
ConstraintSatisfaction.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 1.12.2007 (Swansea) */
00002 /* Copyright 2007, 2008, 2009, 2010, 2011 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/Satisfiability/Lisp/BranchingTuples/Basic.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ConstraintProblems/Domains.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Hypergraphs/Lisp/SetSystems.mac")$
00025 
00026 
00027 /* ***************
00028    * Propagators *
00029    ***************
00030 */
00031 
00032 /*
00033   See ComputerAlgebra/Satisfiability/Lisp/ConstraintProblems/Domains.mac
00034   for the notion of "domain association".
00035 */
00036 /*
00037  A "propagator" is a function which potentially removes values from domains
00038  in a domain association. It changes the domain association in-place,
00039  and returns true iff some change (i.e., reduction) happened.
00040 */
00041 trivial_propagator(dom) := false;
00042 
00043 /* A new propagator which iterates the given one until a fixed point is
00044    reached:
00045 */
00046 prop_fixedpoint(prop) := buildq([prop], lambda([dom], block([p : false],
00047   for i : 1 thru inf do if prop(dom) then p : true else return(p))))$
00048 
00049 /* Another propagator transformer (constructing a new propagator from prop),
00050    removing values which lead to a contradiction by propagation:
00051 */
00052 look_ahead(prop) := buildq([prop], lambda([dom],
00053   block([n : length(dom), p : prop(dom)],
00054     for i : 1 thru n do block([dom_i : dom[i]],
00055       if length(dom_i) > 1 then
00056       for e in dom_i do block([copy_dom : copylist(dom)],
00057         copy_dom[i] : {e},
00058         prop(copy_dom),
00059         if min_dom_size(copy_dom) = 0 then
00060           (dom[i] : disjoin(e, dom_i), p : true))),
00061     return(p))))$
00062 
00063 
00064 /* ***********
00065    * Solvers *
00066    ***********
00067 */
00068 
00069 /* For a constraint satisfaction problem given by domain association and
00070    a propagator, return [sol,size], where size is the number of nodes
00071    in the search tree, while sol is a solution as a list of values or false
00072    iff no solution exists.
00073    The heuristics heur(dom,prop) computes a pair [variable, [list of values]]
00074    for given domain assocation and propagator. dom does not contain empty
00075    domains, and at least one domain has length at least 2. */
00076 /* Termination is guaranteed if the propagator always either removes
00077    some value or produces some empty domain, or yields a domain association
00078    where all domains are singleton sets.
00079    Correctness is guaranteed if the propagator makes sure that in case
00080    a domain association with all singletons is returned, this actually
00081    represents a solution.
00082 */
00083 constraint_backtracking(dom,prop,heur) := block([size : 1],
00084    (prop_fixedpoint(look_ahead(prop)))(dom),
00085    if min_dom_size(dom) = 0 then [false,size]
00086    elseif max_dom_size(dom) = 1 then [map(single_element,dom),size] else (
00087      block([v,val,res,loopbreak : false],
00088      [v, val] : heur(dom,prop),
00089      for e in val do (
00090        block([new_dom : copylist(dom)],
00091        new_dom[v] : {e}, res : constraint_backtracking(new_dom,prop,heur)),
00092        size : size + res[2],
00093        if listp(res[1]) then (loopbreak : true, return(true))),
00094      if loopbreak then return([res[1],size]) else return([false,size])))
00095 )$
00096 
00097 /* Variation for counting solutions; outputs the number of solutions and the
00098    size of the search tree. */
00099 constraint_backtracking_counting(dom,prop,heur) := (
00100    (prop_fixedpoint(look_ahead(prop)))(dom),
00101    if min_dom_size(dom) = 0 then [0,1]
00102    elseif max_dom_size(dom) = 1 then [1,1] else (
00103      block([v,val, count : 0, size : 1],
00104      [v, val] : heur(dom,prop),
00105      for e in val do (
00106        block([new_dom : copylist(dom), c, s],
00107        new_dom[v] : {e},
00108        [c,s] : constraint_backtracking_counting(new_dom,prop,heur),
00109        count : count + c,
00110        size : size + s
00111      )),
00112      return([count,size])
00113      )
00114    )
00115 )$
00116 
00117 
00118 /* **************
00119    * Heuristics *
00120    **************
00121 */
00122 
00123 /* For a constraint satisfaction problem given by domain association and
00124    a propagator, compute the best variable as the variable with minimal
00125    tau-value, where the branching tuple is given by the measure differences
00126    applied to the domain association before and after propagation,
00127    while the measure is the logarithm of the product of domain sizes.
00128    The ordering of values is by increasing distance.
00129 */
00130 variable_heuristics_tau(dom,prop) := block(
00131 [mu : log_prod_dom_size(dom), opt_tau:inf, opt_v, opt_dist, opt_dom],
00132  block([v:1], /* dom_v = dom[v] */
00133   for dom_v in dom do block([dist : []],
00134     if length(dom_v) > 1 then (
00135       for e in dom_v do block([new_dom : copylist(dom), tau_value],
00136         new_dom[v] : {e}, prop(new_dom),
00137         dist : cons(mu - log_prod_dom_size(new_dom), dist)
00138       ),
00139       tau_value : tau(dist),
00140       if tau_value < opt_tau then
00141         (opt_tau : tau_value, opt_v : v, opt_dist : dist, opt_dom : dom_v)
00142     ),
00143     v : v+1
00144   )
00145  ),
00146  block([L : create_list(i,i,1,length(opt_dom)),
00147         comp : lambda([i,j], is(opt_dist[i] < opt_dist[j]))],
00148    L : sort(L, comp),
00149    return([opt_v, create_list((listify(opt_dom))[i], i, L)])))$
00150 
00151 /* The trivial heuristics, which just returns the first variable with
00152   domain-size at least two and the list of its values:
00153 */
00154 trivial_variable_heuristics(dom,prop) := block([v : 1],
00155  for D in dom do
00156    if length(D) >= 2 then return([v,listify(D)])
00157    else v : v + 1)$
00158 
00159