00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020 #include <iostream>
00021 #include <iomanip>
00022 #include <string>
00023 #include <ga/GAParameter.h>
00024 #include <ga/GAStatistics.h>
00025 #include "fssIO.h"
00026 #include "SatProblem.h"
00027 #include "BlindSatSolver.h"
00028 #include "GaSatSolver.h"
00029 #include "SatSolverObserver.h"
00030
00031 using std::string;
00032 using namespace FastSatSolver;
00033 using namespace FastSatSolver::StreamDecorator;
00034
00035
00036 template <
00037 class OBSERVER,
00038 class SUBJECT,
00039 class ARG>
00040 inline OBSERVER* createAttached(SUBJECT *subject, ARG &arg) {
00041 OBSERVER *observer= new OBSERVER(subject, arg);
00042 subject->addObserver(observer);
00043 return observer;
00044 }
00045
00046 int main(int argc, char *argv[]) {
00047 if (argc < 3) {
00048 std::cerr <<
00049 "Usage\n"
00050 "=====\n"
00051 "fss NAME VALUE [NAME VALUE [NAME VALUE [...]]]\n"
00052 "where NAME is name of parameter and VALUE its value\n"
00053 "\n"
00054 "Possible parameters are (abbreviation in parenthesis)\n"
00055 "=====================================================\n"
00056 "input_file(input)............... File containing SAT problem specification.\n"
00057 " '-' means standard input.\n"
00058 "color_output(color)............. 1/0 turns on/off console colored output.\n"
00059 "verbose_mode(verbose)........... 1/0 turns on/off GAlib verbose mode.\n"
00060 "blind_solver(blind)............. Switch between blind and GA solver.\n"
00061 " 1 means blind solver,\n"
00062 " 0 means GA solver(default).\n"
00063 "step_width(stepw)............... (only for blind solver) granularity of solver's\n"
00064 " notifications and control. Default is 16.\n"
00065 "min_count_of_solutions(minslns). Minimal count of solutions requested.\n"
00066 "max_count_of_solutions(maxslns). Maximal count of solutions to look for.\n"
00067 "max_count_of_runs(maxruns)...... GA is restarted for max. maxruns times if\n"
00068 " not all minslns solutions are found.\n"
00069 "max_time_per_run(maxtime)....... Run is be stopped unconditionally if maxtime\n"
00070 " time is exceed (in miliseconds).\n"
00071 "term_upon_convergence(convterm). 0 -> Run is be stopped after ngen generations.\n"
00072 " 1 -> Run is be stopped upon convergence.\n"
00073 "\n"
00074 "NOTE\n"
00075 "====\n"
00076 "There are more parameters for GA solver. Consider GAlib documentation,\n"
00077 "especially its class GASimpleGA.\n";
00078 return 1;
00079 }
00080 int exitCode = 0;
00081
00082
00083 SatProblem *satProblem = 0;
00084 AbstractSatSolver *satSolver = 0;
00085 ProgressWatch *progressWatch = 0;
00086 SolutionsCountStop *slnsCountStop = 0;
00087 TimedStop *timedStop = 0;
00088 FitnessWatch *fitnessWatch = 0;
00089 ResultsWatch *resultsWatch = 0;
00090 SatItemVector *results = 0;
00091 try {
00092
00093 GAParameterList params;
00094
00095 GaSatSolver::registerDefaultParameters(params);
00096
00097
00098 const char DEF_INPUT_FILE[] = "";
00099 const GABoolean DEF_VERBOSE_MODE = gaFalse;
00100 const GABoolean DEF_COLOR_OUTPUT = gaFalse;
00101 const GABoolean DEF_BLIND_SOLVER = gaFalse;
00102 const int DEF_MIN_COUNT_OF_SOLUTIONS = 1;
00103 const int DEF_MAX_COUNT_OF_SOLUTIONS = 8;
00104 const int DEF_MAX_COUNT_OF_RUNS = 8;
00105 const int DEF_MAX_TIME_PER_RUN = 0;
00106 const int DEF_STEP_WIDTH = 16;
00107
00108
00109 params.add("verbose_mode", "verbose", GAParameter::BOOLEAN, &DEF_VERBOSE_MODE);
00110 params.add("color_output", "color", GAParameter::BOOLEAN, &DEF_COLOR_OUTPUT);
00111 params.add("blind_solver", "blind", GAParameter::BOOLEAN, &DEF_BLIND_SOLVER);
00112 params.add("input_file", "input", GAParameter::STRING, &DEF_INPUT_FILE);
00113 params.add("min_count_of_solutions", "minslns", GAParameter::INT, &DEF_MIN_COUNT_OF_SOLUTIONS);
00114 params.add("max_count_of_solutions", "maxslns", GAParameter::INT, &DEF_MAX_COUNT_OF_SOLUTIONS);
00115 params.add("max_count_of_runs", "maxruns", GAParameter::INT, &DEF_MAX_COUNT_OF_RUNS);
00116 params.add("max_time_per_run", "maxtime", GAParameter::INT, &DEF_MAX_TIME_PER_RUN);
00117 params.add("step_width", "stepw", GAParameter::INT, &DEF_STEP_WIDTH);
00118
00119
00120 params.parse(argc, argv, gaTrue);
00121
00122
00123 GABoolean useBlindSolver= DEF_BLIND_SOLVER;
00124 params.get("blind_solver", &useBlindSolver);
00125
00126
00127 GABoolean useColorOutput= DEF_COLOR_OUTPUT;
00128 params.get("color_output", &useColorOutput);
00129 Color::enable(useColorOutput);
00130
00131
00132 GABoolean verboseMode= DEF_VERBOSE_MODE;
00133 params.get("verbose_mode", &verboseMode);
00134
00135
00136 const char *szFileName=
00137 static_cast<const char *>
00138 (params("input_file")->value());
00139 if (0==szFileName)
00140 szFileName = DEF_INPUT_FILE;
00141
00142
00143 int minSlns= DEF_MIN_COUNT_OF_SOLUTIONS;
00144 params.get("min_count_of_solutions", &minSlns);
00145 if (minSlns <= 0) {
00146 printError("min_count_of_solutions out of range, using default");
00147 minSlns = DEF_MIN_COUNT_OF_SOLUTIONS;
00148 }
00149
00150
00151 int maxSlns= DEF_MAX_COUNT_OF_SOLUTIONS;
00152 params.get("max_count_of_solutions", &maxSlns);
00153 if (maxSlns <= 0) {
00154 printError("max_count_of_solutions out of range, using default");
00155 maxSlns = DEF_MAX_COUNT_OF_SOLUTIONS;
00156 }
00157 if (maxSlns < minSlns)
00158 maxSlns = minSlns;
00159
00160
00161
00162 int maxRuns= DEF_MAX_COUNT_OF_RUNS;
00163 params.get("max_count_of_runs", &maxRuns);
00164 if (maxRuns <= 0) {
00165 printError("max_count_of_runs out of range, using default");
00166 maxRuns = DEF_MAX_COUNT_OF_RUNS;
00167 }
00168
00169
00170 int maxTime= DEF_MAX_TIME_PER_RUN;
00171 params.get("max_time_per_run", &maxTime);
00172 if (maxTime < 0) {
00173 printError("max_time_per_run out of range, using default");
00174 maxTime = DEF_MAX_TIME_PER_RUN;
00175 }
00176
00177
00178 int stepWidth= DEF_STEP_WIDTH;
00179 params.get("step_width", &stepWidth);
00180 if (stepWidth <= 0) {
00181 printError("step_width out of range, using default");
00182 stepWidth = DEF_STEP_WIDTH;
00183 }
00184
00185 if (useBlindSolver) {
00186
00187 if (maxRuns != DEF_MAX_COUNT_OF_RUNS) {
00188 printError("Parameter 'max_count_of_runs' is irrelevant for blind solver");
00189 }
00190 maxRuns = 1;
00191 } else {
00192
00193 if (stepWidth != DEF_STEP_WIDTH) {
00194 printError("Parameter 'step_width' is irrelevant for GA solver");
00195 stepWidth = DEF_STEP_WIDTH;
00196 }
00197 }
00198
00199 if (verboseMode)
00200 std::cout << Color(C_CYAN) << params << Color() << std::endl;
00201
00202
00203 satProblem = new SatProblem;
00204
00205
00206 static const char INPUT_STDIN[] = "-";
00207 if (0==strcmp(szFileName, INPUT_STDIN))
00208 satProblem->loadFromInput();
00209 else
00210 satProblem->loadFromFile(szFileName);
00211 if (satProblem->hasError())
00212 throw GenericException("Invalid input data");
00213
00214
00215 const int varsCount = satProblem->getVarsCount();
00216 std::cout << Color(C_YELLOW) << "--- Formulas count: " << Color(C_RED) << satProblem->getFormulasCount() << std::endl;
00217 std::cout << Color(C_YELLOW) << "--- Variables count: " << Color(C_RED) << varsCount << std::endl;
00218 std::cout << Color(C_YELLOW) << "--- Variables: " << Color();
00219 for(int i=0; i< varsCount; i++) {
00220 std::cout << Color(C_RED) << satProblem->getVarName(i) << Color();
00221 if (i==varsCount-1)
00222 std::cout << Color() << std::endl;
00223 else
00224 std::cout << ", ";
00225 }
00226
00227
00228 if (useBlindSolver) {
00229
00230
00231 satSolver = new BlindSatSolver(satProblem, stepWidth);
00232 std::cout << Color(C_LIGHT_BLUE) << ">>> Using blind solver" << Color() << std::endl;
00233
00234
00235 const int progressBits = satProblem->getVarsCount()-stepWidth;
00236 if (progressBits > 0) {
00237 progressWatch = new ProgressWatch(satSolver, 1<<progressBits, std::cout);
00238 satSolver->addObserver(progressWatch);
00239 }
00240 } else {
00241
00242
00243 satSolver = GaSatSolver::create(satProblem, params);
00244 std::cout << Color(C_LIGHT_BLUE) << ">>> Using GAlib solver" << Color() << std::endl;
00245 }
00246
00247
00248 fitnessWatch = createAttached<FitnessWatch>(satSolver, std::cout);
00249
00250
00251 resultsWatch = createAttached<ResultsWatch>(satSolver, std::cout);
00252
00253
00254 slnsCountStop = createAttached<SolutionsCountStop>(satSolver, maxSlns);
00255
00256 if (maxTime)
00257
00258 timedStop = createAttached<TimedStop>(satSolver, maxTime);
00259
00260 int totalSolutions = 0;
00261 float timeTotal = 0.0;
00262 for(int i=0; i<maxRuns; i++) {
00263 if (1<maxRuns)
00264 std::cout << Color(C_GREEN) << ">>> Run" << std::setw(4) << i+1 << " of" << std::setw(4) << maxRuns << Color() << std::endl;
00265
00266
00267 satSolver->reset();
00268 fitnessWatch->reset();
00269
00270
00271 satSolver->start();
00272
00273
00274 delete results;
00275 results= satSolver->getSolutionVector();
00276 const int runSolutions= results->getLength() - totalSolutions;
00277 totalSolutions+= runSolutions;
00278 const float timeElapsed= satSolver->getTimeElapsed()/1000.0;
00279 timeTotal+= timeElapsed;
00280 std::cout
00281 << Color(C_GREEN) << "<<< Found" << std::setw(5) << runSolutions << " solutions"
00282 << " in " << FixedFloat(3,2) << timeElapsed << " s" << Color() << std::endl;
00283 if (1<maxRuns) std::cout
00284 << Color(C_RED) << "<<< Total" << std::setw(5) << totalSolutions << " solutions"
00285 << " in " << FixedFloat(3,2) << timeTotal << " s" << Color() << std::endl;
00286 std::cout << std::endl;
00287
00288 if (totalSolutions >= minSlns)
00289
00290 break;
00291 }
00292 std::cout << Color(C_LIGHT_BLUE);
00293 results->writeOut(satSolver->getProblem(), std::cout);
00294 std::cout << Color() << std::endl;
00295
00296 if (verboseMode && !useBlindSolver) {
00297 GaSatSolver *gaSolver= dynamic_cast<GaSatSolver *>(satSolver);
00298 GAStatistics stats= gaSolver->getStatistics();
00299 std::cout << std::endl << Color(C_CYAN) << stats << Color() << std::endl;
00300 }
00301 }
00302 catch (GenericException e) {
00303 printError(e.getText());
00304 exitCode = 1;
00305 }
00306
00307 delete results;
00308 delete resultsWatch;
00309 delete fitnessWatch;
00310 delete timedStop;
00311 delete slnsCountStop;
00312 delete progressWatch;
00313 delete satSolver;
00314 delete satProblem;
00315
00316 return exitCode;
00317 }
00318