sat.cpp
Go to the documentation of this file.00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020
00021
00022
00023
00024
00025
00026
00027
00028
00029
00030
00031
00032
00033
00034
00035
00036
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
00063 Options::parse(argc,argv);
00064
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 : Script(opt) {
00123 parseDIMACS(opt.filename.c_str());
00124 branch(*this, x, BOOL_VAR_AFC_MAX(), BOOL_VAL_MIN());
00125 }
00126
00128 Sat(bool share, Sat& s) : Script(share,s) {
00129 x.update(*this, share, s.x);
00130 }
00131
00133 virtual Space*
00134 copy(bool share) {
00135 return new Sat(share,*this);
00136 }
00137
00139 virtual void
00140 print(std::ostream& os) const {
00141 os << "solution:\n" << x << std::endl;
00142 }
00143
00145 void parseDIMACS(const char* f) {
00146 int variables = 0;
00147 int clauses = 0;
00148 std::ifstream dimacs(f);
00149 if (!dimacs) {
00150 std::cerr << "error: file '" << f << "' not found" << std::endl;
00151 exit(1);
00152 }
00153 std::cout << "Solving problem from DIMACS file '" << f << "'"
00154 << std::endl;
00155 std::string line;
00156 int c = 0;
00157 while (dimacs.good()) {
00158 std::getline(dimacs,line);
00159
00160 if (line[0] == 'c' || line == "") {
00161 }
00162
00163 else if (variables == 0 && clauses == 0 &&
00164 line[0] == 'p' && line[1] == ' ' &&
00165 line[2] == 'c' && line[3] == 'n' &&
00166 line[4] == 'f' && line[5] == ' ') {
00167 int i = 6;
00168 while (line[i] >= '0' && line[i] <= '9') {
00169 variables = 10*variables + line[i] - '0';
00170 i++;
00171 }
00172 i++;
00173 while (line[i] >= '0' && line[i] <= '9') {
00174 clauses = 10*clauses + line[i] - '0';
00175 i++;
00176 }
00177 std::cout << "(" << variables << " variables, "
00178 << clauses << " clauses)" << std::endl << std::endl;
00179
00180 x = BoolVarArray(*this, variables, 0, 1);
00181 }
00182
00183 else if (variables > 0 &&
00184 ((line[0] >= '0' && line[0] <= '9') || line[0] == '-' || line[0] == ' ')) {
00185 c++;
00186 std::vector<int> pos;
00187 std::vector<int> neg;
00188 int i = 0;
00189 while (line[i] != 0) {
00190 if (line[i] == ' ') {
00191 i++;
00192 continue;
00193 }
00194 bool positive = true;
00195 if (line[i] == '-') {
00196 positive = false;
00197 i++;
00198 }
00199 int value = 0;
00200 while (line[i] >= '0' && line[i] <= '9') {
00201 value = 10 * value + line[i] - '0';
00202 i++;
00203 }
00204 if (value != 0) {
00205 if (positive)
00206 pos.push_back(value-1);
00207 else
00208 neg.push_back(value-1);
00209 i++;
00210 }
00211 }
00212
00213
00214 BoolVarArgs positives(pos.size());
00215 for (int i=pos.size(); i--;)
00216 positives[i] = x[pos[i]];
00217
00218 BoolVarArgs negatives(neg.size());
00219 for (int i=neg.size(); i--;)
00220 negatives[i] = x[neg[i]];
00221
00222
00223 clause(*this, BOT_OR, positives, negatives, 1);
00224 }
00225 else {
00226 std::cerr << "format error in dimacs file" << std::endl;
00227 std::cerr << "context: '" << line << "'" << std::endl;
00228 std::exit(EXIT_FAILURE);
00229 }
00230 }
00231 dimacs.close();
00232 if (clauses != c) {
00233 std::cerr << "error: number of specified clauses seems to be wrong."
00234 << std::endl;
00235 std::exit(EXIT_FAILURE);
00236 }
00237 }
00238 };
00239
00240
00244 int main(int argc, char* argv[]) {
00245
00246 SatOptions opt("SAT");
00247 opt.parse(argc,argv);
00248
00249
00250 if (argc > 1) {
00251 std::cerr << "Could not parse all arguments." << std::endl;
00252 opt.help();
00253 std::exit(EXIT_FAILURE);
00254 }
00255
00256
00257 Script::run<Sat,DFS,SatOptions>(opt);
00258 return 0;
00259 }
00260
00261