Generated on Fri Jul 13 2018 06:08:21 for Gecode by doxygen 1.8.14
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: 2017-02-16 12:11:51 +0100 (Thu, 16 Feb 2017) $ by $Author: schulte $
13  * $Revision: 15434 $
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:
122  : Script(opt) {
123  parseDIMACS(opt.filename.c_str());
124  branch(*this, x, BOOL_VAR_AFC_MAX(), BOOL_VAL_MIN());
125  }
126 
128  Sat(bool share, Sat& s) : Script(share,s) {
129  x.update(*this, share, s.x);
130  }
131 
133  virtual Space*
134  copy(bool share) {
135  return new Sat(share,*this);
136  }
137 
139  virtual void
140  print(std::ostream& os) const {
141  os << "solution:\n" << x << std::endl;
142  }
143 
145  void parseDIMACS(const char* f) {
146  int variables = 0;
147  int clauses = 0;
148  std::ifstream dimacs(f);
149  if (!dimacs) {
150  std::cerr << "error: file '" << f << "' not found" << std::endl;
151  exit(1);
152  }
153  std::cout << "Solving problem from DIMACS file '" << f << "'"
154  << std::endl;
155  std::string line;
156  int c = 0;
157  while (dimacs.good()) {
158  std::getline(dimacs,line);
159  // Comments (ignore them)
160  if (line[0] == 'c' || line == "") {
161  }
162  // Line has format "p cnf <variables> <clauses>"
163  else if (variables == 0 && clauses == 0 &&
164  line[0] == 'p' && line[1] == ' ' &&
165  line[2] == 'c' && line[3] == 'n' &&
166  line[4] == 'f' && line[5] == ' ') {
167  int i = 6;
168  while (line[i] >= '0' && line[i] <= '9') {
169  variables = 10*variables + line[i] - '0';
170  i++;
171  }
172  i++;
173  while (line[i] >= '0' && line[i] <= '9') {
174  clauses = 10*clauses + line[i] - '0';
175  i++;
176  }
177  std::cout << "(" << variables << " variables, "
178  << clauses << " clauses)" << std::endl << std::endl;
179  // Add variables to array
180  x = BoolVarArray(*this, variables, 0, 1);
181  }
182  // Parse regular clause
183  else if (variables > 0 &&
184  ((line[0] >= '0' && line[0] <= '9') || line[0] == '-' || line[0] == ' ')) {
185  c++;
186  std::vector<int> pos;
187  std::vector<int> neg;
188  int i = 0;
189  while (line[i] != 0) {
190  if (line[i] == ' ') {
191  i++;
192  continue;
193  }
194  bool positive = true;
195  if (line[i] == '-') {
196  positive = false;
197  i++;
198  }
199  int value = 0;
200  while (line[i] >= '0' && line[i] <= '9') {
201  value = 10 * value + line[i] - '0';
202  i++;
203  }
204  if (value != 0) {
205  if (positive)
206  pos.push_back(value-1);
207  else
208  neg.push_back(value-1);
209  i++;
210  }
211  }
212 
213  // Create positive BoolVarArgs
214  BoolVarArgs positives(pos.size());
215  for (int i=pos.size(); i--;)
216  positives[i] = x[pos[i]];
217 
218  BoolVarArgs negatives(neg.size());
219  for (int i=neg.size(); i--;)
220  negatives[i] = x[neg[i]];
221 
222  // Post propagators
223  clause(*this, BOT_OR, positives, negatives, 1);
224  }
225  else {
226  std::cerr << "format error in dimacs file" << std::endl;
227  std::cerr << "context: '" << line << "'" << std::endl;
228  std::exit(EXIT_FAILURE);
229  }
230  }
231  dimacs.close();
232  if (clauses != c) {
233  std::cerr << "error: number of specified clauses seems to be wrong."
234  << std::endl;
235  std::exit(EXIT_FAILURE);
236  }
237  }
238 };
239 
240 
244 int main(int argc, char* argv[]) {
245 
246  SatOptions opt("SAT");
247  opt.parse(argc,argv);
248 
249  // Check whether all arguments are successfully parsed
250  if (argc > 1) {
251  std::cerr << "Could not parse all arguments." << std::endl;
252  opt.help();
253  std::exit(EXIT_FAILURE);
254  }
255 
256  // Run SAT solver
257  Script::run<Sat,DFS,SatOptions>(opt);
258  return 0;
259 }
260 
261 // STATISTICS: example-any
std::string filename
Name of the DIMACS file to parse.
Definition: sat.cpp:56
void parse(int &argc, char *argv[])
Parse options from arguments argv (number is argc)
Definition: sat.cpp:61
Sat(bool share, Sat &s)
Constructor for cloning.
Definition: sat.cpp:128
void branch(Home home, const FloatVarArgs &x, FloatVarBranch vars, FloatValBranch vals, FloatBranchFilter bf, FloatVarValPrint vvp)
Branch over x with variable selection vars and value selection vals.
Definition: branch.cpp:43
void update(Space &home, bool share, VarImpVar< VarImp > &y)
Update this variable to be a clone of variable y.
Definition: var.hpp:128
bool pos(const View &x)
Test whether x is postive.
Definition: mult.hpp:45
Options for SAT problems.
Definition: sat.cpp:53
Computation spaces.
Definition: core.hpp:1748
Parametric base-class for scripts.
Definition: driver.hh:703
Gecode::FloatVal c(-8, 8)
BoolValBranch BOOL_VAL_MIN(void)
Select smallest value.
Definition: val.hpp:134
Gecode::IntArgs i(4, 1, 2, 3, 4)
IntRelType neg(IntRelType irt)
Return negated relation type of irt.
Definition: irt.hpp:56
Options opt
The options.
Definition: test.cpp:101
void parseDIMACS(const char *f)
Post constraints according to DIMACS file f.
Definition: sat.cpp:145
SatOptions(const char *s)
Initialize options with file name s.
Definition: sat.cpp:58
Disjunction.
Definition: int.hh:933
virtual Space * copy(bool share)
Perform copying during cloning.
Definition: sat.cpp:134
Passing Boolean variables.
Definition: int.hh:693
Boolean variable array.
Definition: int.hh:789
void parse(int &argc, char *argv[])
Parse options from arguments argv (number is argc)
Definition: options.cpp:510
Post propagator for f(x \diamond_{\mathit{op}} y) \sim_r z \f$ void rel(Home home
virtual void print(std::ostream &os) const
Print solution.
Definition: sat.cpp:140
BoolVarBranch BOOL_VAR_AFC_MAX(double d, BranchTbl tbl)
Select variable with largest accumulated failure count with decay factor d.
Definition: var.hpp:408
virtual void help(void)
Print help message.
Definition: sat.cpp:73
Example: CNF SAT solver
Definition: sat.cpp:115
Post propagator for SetVar x
Definition: set.hh:784
int main(int argc, char *argv[])
Definition: test.cpp:212
Gecode toplevel namespace
Sat(const SatOptions &opt)
The actual problem.
Definition: sat.cpp:121
void positive(int n, const char *l)
Check whether n is in range and strictly positive, otherwise throw out of limits with information l...
Definition: limits.hpp:61
Options for scripts
Definition: driver.hh:366
void clause(Home home, BoolOpType o, const BoolVarArgs &x, const BoolVarArgs &y, int n, IntPropLevel)
Post domain consistent propagator for Boolean clause with positive variables x and negative variables...
Definition: bool.cpp:910
virtual void help(void)
Print help text.
Definition: options.cpp:463