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 <assert.h> 00021 #include <limits.h> 00022 #include <math.h> 00023 #include "fssIO.h" 00024 #include "SatProblem.h" 00025 #include "BlindSatSolver.h" 00026 00027 namespace FastSatSolver { 00028 00029 // //////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// 00030 // LongSatItem implementation 00031 LongSatItem::LongSatItem(int length, long fromNumber): 00032 length_(length), 00033 lNumber_(fromNumber) 00034 { 00035 } 00036 LongSatItem::~LongSatItem() { 00037 } 00038 int LongSatItem::getLength() const { 00039 return length_; 00040 } 00041 bool LongSatItem::getBit(int index) const { 00042 assert(index < length_); 00043 return (1L<<index) & lNumber_; 00044 } 00045 LongSatItem* LongSatItem::clone() const { 00046 return new LongSatItem(length_, lNumber_); 00047 } 00048 00049 // //////////////////////////////////////////////////////////////////////////////////////////////////////////////////////// 00050 // BlindSatSolver implementation 00051 struct BlindSatSolver::Private { 00052 SatProblem *problem; 00053 int stepWidth; 00054 long end; 00055 long current; 00056 float minFitness; 00057 float maxFitness; 00058 double sumFitness; 00059 SatItemVector resultSet; 00060 00061 void init() { 00062 current = 0L; 00063 minFitness = INFINITY; 00064 maxFitness = 0.0; 00065 sumFitness = 0.0; 00066 } 00067 }; 00068 BlindSatSolver::BlindSatSolver(SatProblem *problem, int stepWidth): 00069 d(new Private) 00070 { 00071 const unsigned varsCount= problem->getVarsCount(); 00072 if (varsCount+2 >= LONG_BIT) { 00073 delete d; 00074 throw GenericException("Too much variables - can't use blind solver on this machine!"); 00075 } 00076 d->problem = problem; 00077 d->stepWidth = stepWidth; 00078 d->end = 1L<<varsCount; 00079 d->init(); 00080 } 00081 BlindSatSolver::~BlindSatSolver() { 00082 delete d; 00083 } 00084 SatProblem* BlindSatSolver::getProblem() { 00085 return d->problem; 00086 } 00087 int BlindSatSolver::getSolutionsCount() { 00088 return d->resultSet.getLength(); 00089 } 00090 SatItemVector* BlindSatSolver::getSolutionVector() { 00091 return new SatItemVector(d->resultSet); 00092 } 00093 float BlindSatSolver::minFitness() { 00094 return d->minFitness; 00095 } 00096 float BlindSatSolver::avgFitness() { 00097 return d->sumFitness / d->current; 00098 } 00099 float BlindSatSolver::maxFitness() { 00100 return d->maxFitness; 00101 } 00102 // protected 00103 void BlindSatSolver::initialize() { 00104 d->init(); 00105 d->resultSet.clear(); 00106 } 00107 // protected 00108 void BlindSatSolver::doStep() { 00109 const int nVars= d->problem->getVarsCount(); 00110 const int nForms= d->problem->getFormulasCount(); 00111 const int countPerStep = 1 << d->stepWidth; 00112 for(int i=0; i< countPerStep; i++) { 00113 if (d->current >= d->end) { 00114 // all space explored 00115 this->stop(); 00116 break; 00117 } 00118 00119 // Evalueate fitness 00120 LongSatItem data(nVars, d->current++); 00121 const int nSats= d->problem->getSatsCount(&data); 00122 const float fitness= static_cast<float>(nSats)/nForms; 00123 00124 // Update statistics 00125 d->sumFitness += fitness; 00126 if (fitness < d->minFitness) 00127 d->minFitness = fitness; 00128 00129 if (fitness > d->maxFitness) { 00130 // maxFitness increased 00131 d->maxFitness = fitness; 00132 this->notify(); 00133 } 00134 00135 if (nSats == nForms) { 00136 // Solution found 00137 d->resultSet.addItem(data.clone()); 00138 this->notify(); 00139 } 00140 } 00141 } 00142 00143 00144 } // namespace FastSatSolver 00145