OKlibrary  0.2.1.6
Learning.mac
Go to the documentation of this file.
00001 /* Oliver Kullmann, 8.6.2008 (Swansea) */
00002 /* Copyright 2008 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/Backtracking/DLL_solvers.mac")$
00023 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/ClauseSets/BasicOperations.mac")$
00024 oklib_include("OKlib/ComputerAlgebra/Satisfiability/Lisp/Reductions/GeneralisedUCP.mac")$
00025 
00026 
00027 /* The most basic learning algorithm for SAT, without conflict analysis,
00028    and with complete restart after each conflict. */
00029 /* The heuristics is as for DLL algorithms. */
00030 /* The reduction r must be at least as strong as r_1. */
00031 basic_learning(r,h) := buildq([r,h], lambda([FF],
00032  block([F0 : FF[2], result : unknown],
00033    unless result # unknown do block([F : r(F0)],
00034      if emptyp(F) then result : true
00035      elseif empty_element_p(F) then result : false
00036      else block([phi : {}],
00037        unless result # unknown do block([x : h(cs2fcs(F))],
00038          phi : adjoin(x,phi),
00039          F : r(apply_pa_cs({x},F)),
00040          if emptyp(F) then result : true
00041          elseif empty_element_p(F) then result : false
00042        ),
00043        if result = false then ( /* Learning: */
00044          F0 : adjoin(comp_sl(phi),F0), result : unknown
00045      ))),
00046  return(result))))$
00047