Generated on Sat Aug 25 2012 03:32:42 for Gecode by doxygen 1.8.1.2
sat.cpp
Go to the documentation of this file.
1 /* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2 /*
3  * Main authors:
4  * Raphael Reischuk <reischuk@cs.uni-sb.de>
5  * Guido Tack <tack@gecode.org>
6  *
7  * Copyright:
8  * Raphael Reischuk, 2008
9  * Guido Tack, 2008
10  *
11  * Last modified:
12  * $Date: 2010-10-07 20:52:01 +1100 (Thu, 07 Oct 2010) $ by $Author: schulte $
13  * $Revision: 11473 $
14  *
15  * This file is part of Gecode, the generic constraint
16  * development environment:
17  * http://www.gecode.org
18  *
19  * Permission is hereby granted, free of charge, to any person obtaining
20  * a copy of this software and associated documentation files (the
21  * "Software"), to deal in the Software without restriction, including
22  * without limitation the rights to use, copy, modify, merge, publish,
23  * distribute, sublicense, and/or sell copies of the Software, and to
24  * permit persons to whom the Software is furnished to do so, subject to
25  * the following conditions:
26  *
27  * The above copyright notice and this permission notice shall be
28  * included in all copies or substantial portions of the Software.
29  *
30  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
31  * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
32  * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
33  * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
34  * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
35  * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
36  * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
37  *
38  */
39 
40 #include <gecode/driver.hh>
41 #include <gecode/int.hh>
42 
43 #include <fstream>
44 #include <string>
45 #include <vector>
46 
47 using namespace Gecode;
48 
53 class SatOptions : public Options {
54 public:
56  std::string filename;
58  SatOptions(const char* s)
59  : Options(s) {}
61  void parse(int& argc, char* argv[]) {
62  // Parse regular options
63  Options::parse(argc,argv);
64  // Filename, should be at position 1
65  if (argc == 1) {
66  help();
67  exit(1);
68  }
69  filename = argv[1];
70  argc--;
71  }
73  virtual void help(void) {
74  Options::help();
75  std::cerr << "\t(string) " << std::endl
76  << "\t\tdimacs file to parse (.cnf)" << std::endl;
77  }
78 };
79 
115 class Sat : public Script {
116 private:
118  BoolVarArray x;
119 public:
121  Sat(const SatOptions& opt) {
122  parseDIMACS(opt.filename.c_str());
123  branch(*this, x, INT_VAR_NONE, INT_VAL_MIN);
124  }
125 
127  Sat(bool share, Sat& s) : Script(share,s) {
128  x.update(*this, share, s.x);
129  }
130 
132  virtual Space*
133  copy(bool share) {
134  return new Sat(share,*this);
135  }
136 
138  virtual void
139  print(std::ostream& os) const {
140  os << "solution:\n" << x << std::endl;
141  }
142 
144  void parseDIMACS(const char* f) {
145  int variables = 0;
146  int clauses = 0;
147  std::ifstream dimacs(f);
148  if (!dimacs) {
149  std::cerr << "error: file '" << f << "' not found" << std::endl;
150  exit(1);
151  }
152  std::cout << "Solving problem from DIMACS file '" << f << "'"
153  << std::endl;
154  std::string line;
155  int c = 0;
156  while (dimacs.good()) {
157  std::getline(dimacs,line);
158  // Comments (ignore them)
159  if (line[0] == 'c' || line == "") {
160  }
161  // Line has format "p cnf <variables> <clauses>"
162  else if (variables == 0 && clauses == 0 &&
163  line[0] == 'p' && line[1] == ' ' &&
164  line[2] == 'c' && line[3] == 'n' &&
165  line[4] == 'f' && line[5] == ' ') {
166  int i = 6;
167  while (line[i] >= '0' && line[i] <= '9') {
168  variables = 10*variables + line[i] - '0';
169  i++;
170  }
171  i++;
172  while (line[i] >= '0' && line[i] <= '9') {
173  clauses = 10*clauses + line[i] - '0';
174  i++;
175  }
176  std::cout << "(" << variables << " variables, "
177  << clauses << " clauses)" << std::endl << std::endl;
178  // Add variables to array
179  x = BoolVarArray(*this, variables, 0, 1);
180  }
181  // Parse regular clause
182  else if (variables > 0 &&
183  ((line[0] >= '0' && line[0] <= '9') || line[0] == '-' || line[0] == ' ')) {
184  c++;
185  std::vector<int> pos;
186  std::vector<int> neg;
187  int i = 0;
188  while (line[i] != 0) {
189  if (line[i] == ' ') {
190  i++;
191  continue;
192  }
193  bool positive = true;
194  if (line[i] == '-') {
195  positive = false;
196  i++;
197  }
198  int value = 0;
199  while (line[i] >= '0' && line[i] <= '9') {
200  value = 10 * value + line[i] - '0';
201  i++;
202  }
203  if (value != 0) {
204  if (positive)
205  pos.push_back(value-1);
206  else
207  neg.push_back(value-1);
208  i++;
209  }
210  }
211 
212  // Create positive BoolVarArgs
213  BoolVarArgs positives(pos.size());
214  for (int i=pos.size(); i--;)
215  positives[i] = x[pos[i]];
216 
217  BoolVarArgs negatives(neg.size());
218  for (int i=neg.size(); i--;)
219  negatives[i] = x[neg[i]];
220 
221  // Post propagators
222  clause(*this, BOT_OR, positives, negatives, 1);
223  }
224  else {
225  std::cerr << "format error in dimacs file" << std::endl;
226  std::cerr << "context: '" << line << "'" << std::endl;
227  std::exit(EXIT_FAILURE);
228  }
229  }
230  dimacs.close();
231  if (clauses != c) {
232  std::cerr << "error: number of specified clauses seems to be wrong."
233  << std::endl;
234  std::exit(EXIT_FAILURE);
235  }
236  }
237 };
238 
239 
243 int main(int argc, char* argv[]) {
244 
245  SatOptions opt("SAT");
246  opt.parse(argc,argv);
247 
248  // Check whether all arguments are successfully parsed
249  if (argc > 1) {
250  std::cerr << "Could not parse all arguments." << std::endl;
251  opt.help();
252  std::exit(EXIT_FAILURE);
253  }
254 
255  // Run SAT solver
256  Script::run<Sat,DFS,SatOptions>(opt);
257  return 0;
258 }
259 
260 // STATISTICS: example-any