fss.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 <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 // Create observer OBSERVER and attach it to subject
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   // Used for final clean-up on exit
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     // Parse cmd-line parameters
00093     GAParameterList params;
00094     // GaSatSolver-specific parameters
00095     GaSatSolver::registerDefaultParameters(params);
00096 
00097     // Default values of parameters
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     // Register extra parameters
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     // parse using GAParameterList class
00120     params.parse(argc, argv, gaTrue);
00121 
00122     // true for blind solver, false for GA solver
00123     GABoolean useBlindSolver= DEF_BLIND_SOLVER;
00124     params.get("blind_solver", &useBlindSolver);
00125 
00126     // turn on/off color output (using escape squences)
00127     GABoolean useColorOutput= DEF_COLOR_OUTPUT;
00128     params.get("color_output", &useColorOutput);
00129     Color::enable(useColorOutput);
00130 
00131     // turn on/off GAlib verbose mode
00132     GABoolean verboseMode= DEF_VERBOSE_MODE;
00133     params.get("verbose_mode", &verboseMode);
00134 
00135     // Read input file name
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     // Minimum of solutions (to declare as solution)
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     // Maximum number of solutions (solver stop when reached)
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     // Maximum nuber of runs (if satisfaction is not reachable)
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     // Maximum time elapsed for one run, 0 means infinity
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     // Step width (only for blind solver)
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       // exclude parameters for blind solver
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       // exclude parameters for GA solver
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     // Create SAT problem instace
00203     satProblem = new SatProblem;
00204 
00205     // Read input data
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     // Write out compilation statistics
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     // create desired solver
00228     if (useBlindSolver) {
00229 
00230       // create blind solver
00231       satSolver = new BlindSatSolver(satProblem, stepWidth);
00232       std::cout << Color(C_LIGHT_BLUE) << ">>> Using blind solver" << Color() << std::endl;
00233 
00234       // attach progress indicator
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       // create GA solver
00243       satSolver = GaSatSolver::create(satProblem, params);
00244       std::cout << Color(C_LIGHT_BLUE) << ">>> Using GAlib solver" << Color() << std::endl;
00245     }
00246 
00247     // Display message if maxFitness is increased
00248     fitnessWatch = createAttached<FitnessWatch>(satSolver, std::cout);
00249 
00250     // Display message if solution is discovered
00251     resultsWatch = createAttached<ResultsWatch>(satSolver, std::cout);
00252 
00253     // Stop progress after maxSlns solutions are found
00254     slnsCountStop = createAttached<SolutionsCountStop>(satSolver, maxSlns);
00255 
00256     if (maxTime)
00257       // Run will be stopped if its time exceeds
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       // Initialization
00267       satSolver->reset();
00268       fitnessWatch->reset();
00269 
00270       // Start progress
00271       satSolver->start();
00272 
00273       // Fetch progresse's results
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         // minSlns reached, cancel rest of runs
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   // Final clean-up
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 

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