GaSatSolver.cpp

Go to the documentation of this file.
00001 /*
00002  * Copyright (C) 2008 Kamil Dudka <xdudka00@stud.fit.vutbr.cz>
00003  *
00004  * This file is part of fss (Fast SAT Solver).
00005  *
00006  * fss is free software: you can redistribute it and/or modify
00007  * it under the terms of the GNU General Public License as published by
00008  * the Free Software Foundation, either version 3 of the License, or
00009  * any later version.
00010  *
00011  * fss is distributed in the hope that it will be useful,
00012  * but WITHOUT ANY WARRANTY; without even the implied warranty of
00013  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
00014  * GNU General Public License for more details.
00015  *
00016  * You should have received a copy of the GNU General Public License
00017  * along with fss.  If not, see <http://www.gnu.org/licenses/>.
00018  */
00019 
00020 #include <ga/GA1DBinStrGenome.h>
00021 #include <ga/GASimpleGA.h>
00022 #include <ga/GAStatistics.h>
00023 
00024 #include "fssIO.h"
00025 #include "SatProblem.h"
00026 #include "GaSatSolver.h"
00027 
00028 //#include <ga/GASStateGA.h>
00029 //#include <ga/GAIncGA.h>
00030 //#include <ga/GADemeGA.h>
00031 
00032 typedef GASimpleGA TGeneticAlgorithm;
00033 
00034 namespace FastSatSolver {
00035 
00036   // ////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
00037   // GaSatItem implementation
00038   struct GaSatItem::Private {
00039     GABinaryString bs;
00040 
00041     Private(unsigned size): bs(size) { }
00042   };
00043   GaSatItem::GaSatItem(const GABinaryString &bs):
00044     d(new Private(bs.size()))
00045   {
00046     d->bs.copy(bs);
00047   }
00048   GaSatItem::~GaSatItem() {
00049     delete d;
00050   }
00051   int GaSatItem::getLength() const {
00052     return d->bs.size();
00053   }
00054   bool GaSatItem::getBit(int index) const {
00055     return d->bs.bit(index);
00056   }
00057   GaSatItem* GaSatItem::clone() const {
00058     return new GaSatItem(d->bs);
00059   }
00060 
00061   // ////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
00062   // SatItemGalibAdatper implementation
00063   SatItemGalibAdatper::SatItemGalibAdatper(const GABinaryString &bs):
00064     bs_(bs)
00065   {
00066   }
00067   SatItemGalibAdatper::~SatItemGalibAdatper() { }
00068   int SatItemGalibAdatper::getLength() const {
00069     return bs_.size();
00070   }
00071   bool SatItemGalibAdatper::getBit(int index) const {
00072     return bs_.bit(index);
00073   }
00074   // FIXME: There is no deep copy (optimalization)
00075   SatItemGalibAdatper* SatItemGalibAdatper::clone() const {
00076     return new SatItemGalibAdatper(bs_);
00077   }
00078 
00079   // ////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
00080   // GaSatSolver implementation
00081   struct GaSatSolver::Private {
00082     SatProblem                *problem;
00083     GaSatSolver               *solver;
00084     float                     maxFitness;
00085     GA1DBinaryStringGenome    *genome;
00086     TGeneticAlgorithm         *ga;
00087     SatItemSet                *resultSet;
00088 
00089     static float fitness(GAGenome &);
00090   };
00091   // protected
00092   GaSatSolver::GaSatSolver (SatProblem *problem, const GAParameterList &params):
00093     d(new Private)
00094   {
00095     d->problem = problem;
00096     d->solver = this;
00097     d->maxFitness = 0.0;
00098     const int varsCount = problem->getVarsCount();
00099     d->genome = new GA1DBinaryStringGenome(varsCount, Private::fitness, d);
00100     d->ga = new TGeneticAlgorithm(*(d->genome));
00101     d->ga->parameters(params);
00102     bool termUponConvergence = false;
00103     params.get("term_upon_convergence", &termUponConvergence);
00104     if (termUponConvergence)
00105       d->ga->terminator(GAGeneticAlgorithm::TerminateUponConvergence);
00106       //d->ga->terminator(GAGeneticAlgorithm::TerminateUponPopConvergence);
00107     d->resultSet = new SatItemSet;
00108   }
00109   GaSatSolver::~GaSatSolver() {
00110     delete d->resultSet;
00111     delete d->ga;
00112     delete d->genome;
00113     delete d;
00114   }
00115   GaSatSolver* GaSatSolver::create (SatProblem *problem, const GAParameterList &params) {
00116     GaSatSolver *obj = new GaSatSolver(problem, params);
00117     obj->initialize();
00118     return obj;
00119   }
00120   void GaSatSolver::registerDefaultParameters(GAParameterList &params) {
00121     TGeneticAlgorithm::registerDefaultParameters(params);
00122     const bool FALSE = false;
00123     params.add("term_upon_convergence", "convterm", GAParameter::BOOLEAN, &FALSE);
00124   }
00125   SatProblem* GaSatSolver::getProblem() {
00126     return d->problem;
00127   }
00128   const GAStatistics& GaSatSolver::getStatistics() const {
00129     return d->ga->statistics();
00130   }
00131   int GaSatSolver::getSolutionsCount() {
00132     return d->resultSet->getLength();
00133   }
00134   SatItemVector* GaSatSolver::getSolutionVector() {
00135     return d->resultSet->createVector();
00136   }
00137   float GaSatSolver::minFitness() {
00138     return d->ga->statistics().offlineMin();
00139   }
00140   float GaSatSolver::avgFitness() {
00141     return d->ga->statistics().offlineMax();
00142   }
00143   float GaSatSolver::maxFitness() {
00144     return d->maxFitness;
00145   }
00146   // protected
00147   void GaSatSolver::initialize() {
00148     GARandomSeed();
00149     d->maxFitness = 0.0;
00150     d->ga->initialize();
00151     // Now using incremental strategy
00152     // d->resultSet->clear();
00153   }
00154   // protected
00155   void GaSatSolver::doStep() {
00156     GAGeneticAlgorithm &ga= *(d->ga);
00157     ga.step();
00158     if (ga.done()) {
00159       this->stop();
00160 #if 0//ndef NDEBUG
00161       std::cerr << ">>> Stopped by GAlib terminator" << std::endl;
00162 #endif // NDEBUG
00163     }
00164   }
00165   float GaSatSolver::Private::fitness(GAGenome &genome) {
00166     // Static to non-static binding
00167     Private *d = reinterpret_cast<Private *>(genome.userData());
00168     SatProblem *problem = dynamic_cast<SatProblem *>(d->problem);
00169     GaSatSolver *solver = dynamic_cast<GaSatSolver *>(d->solver);
00170     const GABinaryString &bs= dynamic_cast<GABinaryString &>(genome);
00171     SatItemSet *resultSet= dynamic_cast<SatItemSet *>(d->resultSet);
00172 
00173     // Compute fitness
00174     SatItemGalibAdatper data(bs);
00175     const int formulasCount = problem->getFormulasCount();
00176     const int satsCount = problem->getSatsCount(&data);
00177     float fitness = static_cast<float>(satsCount)/formulasCount;
00178     if (fitness > d->maxFitness) {
00179       d->maxFitness = fitness;
00180       solver->notify();
00181     }
00182 
00183     if (formulasCount==satsCount) {
00184       resultSet->addItem(new GaSatItem(bs));
00185       solver->notify();
00186     };
00187 
00188     // TODO: scale fitness?
00189     return fitness;
00190   }
00191 
00192 
00193 } // namespace FastSatSolver
00194 

Generated on Wed Nov 5 22:30:21 2008 for Fast SAT Solver by  doxygen 1.5.4