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 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
00159 if (line[0] == 'c' || line == "") {
00160 }
00161
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
00179 x = BoolVarArray(*this, variables, 0, 1);
00180 }
00181
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
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
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
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
00256 Script::run<Sat,DFS,SatOptions>(opt);
00257 return 0;
00258 }
00259
00260