Generated on Fri Oct 19 11:24:49 2018 for Gecode by doxygen 1.6.3

sat.cpp

Go to the documentation of this file.
00001 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
00002 /*
00003  *  Main authors:
00004  *     Raphael Reischuk <reischuk@cs.uni-sb.de>
00005  *     Guido Tack <tack@gecode.org>
00006  *
00007  *  Copyright:
00008  *     Raphael Reischuk, 2008
00009  *     Guido Tack, 2008
00010  *
00011  *  This file is part of Gecode, the generic constraint
00012  *  development environment:
00013  *     http://www.gecode.org
00014  *
00015  *  Permission is hereby granted, free of charge, to any person obtaining
00016  *  a copy of this software and associated documentation files (the
00017  *  "Software"), to deal in the Software without restriction, including
00018  *  without limitation the rights to use, copy, modify, merge, publish,
00019  *  distribute, sublicense, and/or sell copies of the Software, and to
00020  *  permit persons to whom the Software is furnished to do so, subject to
00021  *  the following conditions:
00022  *
00023  *  The above copyright notice and this permission notice shall be
00024  *  included in all copies or substantial portions of the Software.
00025  *
00026  *  THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
00027  *  EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
00028  *  MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
00029  *  NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
00030  *  LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
00031  *  OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
00032  *  WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
00033  *
00034  */
00035 
00036 #include <gecode/driver.hh>
00037 #include <gecode/int.hh>
00038 
00039 #include <fstream>
00040 #include <string>
00041 #include <vector>
00042 
00043 using namespace Gecode;
00044 
00049 class SatOptions : public Options {
00050 public:
00052   std::string filename;
00054   SatOptions(const char* s)
00055     : Options(s) {}
00057   void parse(int& argc, char* argv[]) {
00058     // Parse regular options
00059     Options::parse(argc,argv);
00060     // Filename, should be at position 1
00061     if (argc == 1) {
00062       help();
00063       exit(1);
00064     }
00065     filename = argv[1];
00066     argc--;
00067   }
00069   virtual void help(void) {
00070     Options::help();
00071     std::cerr << "\t(string) " << std::endl
00072               << "\t\tdimacs file to parse (.cnf)" << std::endl;
00073   }
00074 };
00075 
00111 class Sat : public Script {
00112 private:
00114   BoolVarArray x;
00115 public:
00117   Sat(const SatOptions& opt)
00118     : Script(opt) {
00119     parseDIMACS(opt.filename.c_str());
00120     branch(*this, x, BOOL_VAR_AFC_MAX(), BOOL_VAL_MIN());
00121   }
00122 
00124   Sat(Sat& s) : Script(s) {
00125     x.update(*this, s.x);
00126   }
00127 
00129   virtual Space*
00130   copy(void) {
00131     return new Sat(*this);
00132   }
00133 
00135   virtual void
00136   print(std::ostream& os) const {
00137     os << "solution:\n" << x << std::endl;
00138   }
00139 
00141   void parseDIMACS(const char* f) {
00142     int variables = 0;
00143     int clauses = 0;
00144     std::ifstream dimacs(f);
00145     if (!dimacs) {
00146       std::cerr << "error: file '" << f << "' not found" << std::endl;
00147       exit(1);
00148     }
00149     std::cout << "Solving problem from DIMACS file '" << f << "'"
00150               << std::endl;
00151     std::string line;
00152     int c = 0;
00153     while (dimacs.good()) {
00154       std::getline(dimacs,line);
00155       // Comments (ignore them)
00156       if (line[0] == 'c' || line == "") {
00157       }
00158       // Line has format "p cnf <variables> <clauses>"
00159       else if (variables == 0 && clauses == 0 &&
00160                line[0] == 'p' && line[1] == ' ' &&
00161                line[2] == 'c' && line[3] == 'n' &&
00162                line[4] == 'f' && line[5] == ' ') {
00163         int i = 6;
00164         while (line[i] >= '0' && line[i] <= '9') {
00165           variables = 10*variables + line[i] - '0';
00166           i++;
00167         }
00168         i++;
00169         while (line[i] >= '0' && line[i] <= '9') {
00170           clauses = 10*clauses + line[i] - '0';
00171           i++;
00172         }
00173         std::cout << "(" << variables << " variables, "
00174                   << clauses << " clauses)" << std::endl << std::endl;
00175         // Add variables to array
00176         x = BoolVarArray(*this, variables, 0, 1);
00177       }
00178       // Parse regular clause
00179       else if (variables > 0 &&
00180       ((line[0] >= '0' && line[0] <= '9') || line[0] == '-' || line[0] == ' ')) {
00181         c++;
00182         std::vector<int> pos;
00183         std::vector<int> neg;
00184         int i = 0;
00185         while (line[i] != 0) {
00186           if (line[i] == ' ') {
00187             i++;
00188             continue;
00189           }
00190           bool positive = true;
00191           if (line[i] == '-') {
00192             positive = false;
00193             i++;
00194           }
00195           int value = 0;
00196           while (line[i] >= '0' && line[i] <= '9') {
00197             value = 10 * value + line[i] - '0';
00198             i++;
00199           }
00200           if (value != 0) {
00201             if (positive)
00202               pos.push_back(value-1);
00203             else
00204               neg.push_back(value-1);
00205             i++;
00206           }
00207         }
00208 
00209         // Create positive BoolVarArgs
00210         BoolVarArgs positives(pos.size());
00211         for (int i=pos.size(); i--;)
00212           positives[i] = x[pos[i]];
00213 
00214         BoolVarArgs negatives(neg.size());
00215         for (int i=neg.size(); i--;)
00216           negatives[i] = x[neg[i]];
00217 
00218         // Post propagators
00219         clause(*this, BOT_OR, positives, negatives, 1);
00220       }
00221       else {
00222         std::cerr << "format error in dimacs file" << std::endl;
00223         std::cerr << "context: '" << line << "'" << std::endl;
00224         std::exit(EXIT_FAILURE);
00225       }
00226     }
00227     dimacs.close();
00228     if (clauses != c) {
00229       std::cerr << "error: number of specified clauses seems to be wrong."
00230                 << std::endl;
00231       std::exit(EXIT_FAILURE);
00232     }
00233   }
00234 };
00235 
00236 
00240 int main(int argc, char* argv[]) {
00241 
00242   SatOptions opt("SAT");
00243   opt.parse(argc,argv);
00244 
00245   // Check whether all arguments are successfully parsed
00246   if (argc > 1) {
00247     std::cerr << "Could not parse all arguments." << std::endl;
00248     opt.help();
00249     std::exit(EXIT_FAILURE);
00250   }
00251 
00252   // Run SAT solver
00253   Script::run<Sat,DFS,SatOptions>(opt);
00254   return 0;
00255 }
00256 
00257 // STATISTICS: example-any