Fast SAT Solver (C++, GAlib)
File detail
Source code
/*
* Copyright (C) 2008 Kamil Dudka <xdudka00@stud.fit.vutbr.cz>
*
* This file is part of fss (Fast SAT Solver).
*
* fss is free software: you can redistribute it and/or modify
* it under the terms of the GNU General Public License as published by
* the Free Software Foundation, either version 3 of the License, or
* any later version.
*
* fss is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with fss. If not, see <http://www.gnu.org/licenses/>.
*/
#include <assert.h>
#include <limits.h>
#include <math.h>
#include "fssIO.h"
#include "SatProblem.h"
#include "BlindSatSolver.h"
namespace FastSatSolver {
// ////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
// LongSatItem implementation
LongSatItem::LongSatItem(int length, long fromNumber):
length_(length),
lNumber_(fromNumber)
{
}
LongSatItem::~LongSatItem() {
}
int LongSatItem::getLength() const {
return length_;
}
bool LongSatItem::getBit(int index) const {
assert(index < length_);
return (1L<<index) & lNumber_;
}
LongSatItem* LongSatItem::clone() const {
return new LongSatItem(length_, lNumber_);
}
// ////////////////////////////////////////////////////////////////////////////////////////////////////////////////////////
// BlindSatSolver implementation
struct BlindSatSolver::Private {
SatProblem *problem;
int stepWidth;
long end;
long current;
float minFitness;
float maxFitness;
double sumFitness;
SatItemVector resultSet;
void init() {
current = 0L;
minFitness = INFINITY;
maxFitness = 0.0;
sumFitness = 0.0;
}
};
BlindSatSolver::BlindSatSolver(SatProblem *problem, int stepWidth):
d(new Private)
{
const unsigned varsCount= problem->getVarsCount();
if (varsCount+2 >= LONG_BIT) {
delete d;
throw GenericException("Too much variables - can't use blind solver on this machine!");
}
d->problem = problem;
d->stepWidth = stepWidth;
d->end = 1L<<varsCount;
d->init();
}
BlindSatSolver::~BlindSatSolver() {
delete d;
}
SatProblem* BlindSatSolver::getProblem() {
return d->problem;
}
int BlindSatSolver::getSolutionsCount() {
return d->resultSet.getLength();
}
SatItemVector* BlindSatSolver::getSolutionVector() {
return new SatItemVector(d->resultSet);
}
float BlindSatSolver::minFitness() {
return d->minFitness;
}
float BlindSatSolver::avgFitness() {
return d->sumFitness / d->current;
}
float BlindSatSolver::maxFitness() {
return d->maxFitness;
}
// protected
void BlindSatSolver::initialize() {
d->init();
d->resultSet.clear();
}
// protected
void BlindSatSolver::doStep() {
const int nVars= d->problem->getVarsCount();
const int nForms= d->problem->getFormulasCount();
const int countPerStep = 1 << d->stepWidth;
for(int i=0; i< countPerStep; i++) {
if (d->current >= d->end) {
// all space explored
this->stop();
break;
}
// Evalueate fitness
LongSatItem data(nVars, d->current++);
const int nSats= d->problem->getSatsCount(&data);
const float fitness= static_cast<float>(nSats)/nForms;
// Update statistics
d->sumFitness += fitness;
if (fitness < d->minFitness)
d->minFitness = fitness;
if (fitness > d->maxFitness) {
// maxFitness increased
d->maxFitness = fitness;
this->notify();
}
if (nSats == nForms) {
// Solution found
d->resultSet.addItem(data.clone());
this->notify();
}
}
}
} // namespace FastSatSolver