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 ¶ms): 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 ¶ms) { 00116 GaSatSolver *obj = new GaSatSolver(problem, params); 00117 obj->initialize(); 00118 return obj; 00119 } 00120 void GaSatSolver::registerDefaultParameters(GAParameterList ¶ms) { 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