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