Generated on Fri Jan 28 2022 04:43:06 for Gecode by doxygen 1.8.13
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  * This file is part of Gecode, the generic constraint
12  * development environment:
13  * http://www.gecode.org
14  *
15  * Permission is hereby granted, free of charge, to any person obtaining
16  * a copy of this software and associated documentation files (the
17  * "Software"), to deal in the Software without restriction, including
18  * without limitation the rights to use, copy, modify, merge, publish,
19  * distribute, sublicense, and/or sell copies of the Software, and to
20  * permit persons to whom the Software is furnished to do so, subject to
21  * the following conditions:
22  *
23  * The above copyright notice and this permission notice shall be
24  * included in all copies or substantial portions of the Software.
25  *
26  * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
27  * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
28  * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
29  * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
30  * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
31  * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
32  * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
33  *
34  */
35 
36 #include <gecode/driver.hh>
37 #include <gecode/int.hh>
38 
39 #include <fstream>
40 #include <string>
41 #include <vector>
42 
43 using namespace Gecode;
44 
49 class SatOptions : public Options {
50 public:
52  std::string filename;
54  SatOptions(const char* s)
55  : Options(s) {}
57  void parse(int& argc, char* argv[]) {
58  // Parse regular options
59  Options::parse(argc,argv);
60  // Filename, should be at position 1
61  if (argc == 1) {
62  help();
63  exit(1);
64  }
65  filename = argv[1];
66  argc--;
67  }
69  virtual void help(void) {
70  Options::help();
71  std::cerr << "\t(string) " << std::endl
72  << "\t\tdimacs file to parse (.cnf)" << std::endl;
73  }
74 };
75 
111 class Sat : public Script {
112 private:
114  BoolVarArray x;
115 public:
118  : Script(opt) {
119  parseDIMACS(opt.filename.c_str());
120  branch(*this, x, BOOL_VAR_AFC_MAX(), BOOL_VAL_MIN());
121  }
122 
124  Sat(Sat& s) : Script(s) {
125  x.update(*this, s.x);
126  }
127 
129  virtual Space*
130  copy(void) {
131  return new Sat(*this);
132  }
133 
135  virtual void
136  print(std::ostream& os) const {
137  os << "solution:\n" << x << std::endl;
138  }
139 
141  void parseDIMACS(const char* f) {
142  int variables = 0;
143  int clauses = 0;
144  std::ifstream dimacs(f);
145  if (!dimacs) {
146  std::cerr << "error: file '" << f << "' not found" << std::endl;
147  exit(1);
148  }
149  std::cout << "Solving problem from DIMACS file '" << f << "'"
150  << std::endl;
151  std::string line;
152  int c = 0;
153  while (dimacs.good()) {
154  std::getline(dimacs,line);
155  // Comments (ignore them)
156  if (line[0] == 'c' || line == "") {
157  }
158  // Line has format "p cnf <variables> <clauses>"
159  else if (variables == 0 && clauses == 0 &&
160  line[0] == 'p' && line[1] == ' ' &&
161  line[2] == 'c' && line[3] == 'n' &&
162  line[4] == 'f' && line[5] == ' ') {
163  int i = 6;
164  while (line[i] >= '0' && line[i] <= '9') {
165  variables = 10*variables + line[i] - '0';
166  i++;
167  }
168  i++;
169  while (line[i] >= '0' && line[i] <= '9') {
170  clauses = 10*clauses + line[i] - '0';
171  i++;
172  }
173  std::cout << "(" << variables << " variables, "
174  << clauses << " clauses)" << std::endl << std::endl;
175  // Add variables to array
176  x = BoolVarArray(*this, variables, 0, 1);
177  }
178  // Parse regular clause
179  else if (variables > 0 &&
180  ((line[0] >= '0' && line[0] <= '9') || line[0] == '-' || line[0] == ' ')) {
181  c++;
182  std::vector<int> pos;
183  std::vector<int> neg;
184  int i = 0;
185  while (line[i] != 0) {
186  if (line[i] == ' ') {
187  i++;
188  continue;
189  }
190  bool positive = true;
191  if (line[i] == '-') {
192  positive = false;
193  i++;
194  }
195  int value = 0;
196  while (line[i] >= '0' && line[i] <= '9') {
197  value = 10 * value + line[i] - '0';
198  i++;
199  }
200  if (value != 0) {
201  if (positive)
202  pos.push_back(value-1);
203  else
204  neg.push_back(value-1);
205  i++;
206  }
207  }
208 
209  // Create positive BoolVarArgs
210  BoolVarArgs positives(pos.size());
211  for (int i=pos.size(); i--;)
212  positives[i] = x[pos[i]];
213 
214  BoolVarArgs negatives(neg.size());
215  for (int i=neg.size(); i--;)
216  negatives[i] = x[neg[i]];
217 
218  // Post propagators
219  clause(*this, BOT_OR, positives, negatives, 1);
220  }
221  else {
222  std::cerr << "format error in dimacs file" << std::endl;
223  std::cerr << "context: '" << line << "'" << std::endl;
224  std::exit(EXIT_FAILURE);
225  }
226  }
227  dimacs.close();
228  if (clauses != c) {
229  std::cerr << "error: number of specified clauses seems to be wrong."
230  << std::endl;
231  std::exit(EXIT_FAILURE);
232  }
233  }
234 };
235 
236 
240 int main(int argc, char* argv[]) {
241 
242  SatOptions opt("SAT");
243  opt.parse(argc,argv);
244 
245  // Check whether all arguments are successfully parsed
246  if (argc > 1) {
247  std::cerr << "Could not parse all arguments." << std::endl;
248  opt.help();
249  std::exit(EXIT_FAILURE);
250  }
251 
252  // Run SAT solver
253  Script::run<Sat,DFS,SatOptions>(opt);
254  return 0;
255 }
256 
257 // STATISTICS: example-any
std::string filename
Name of the DIMACS file to parse.
Definition: sat.cpp:52
void parse(int &argc, char *argv[])
Parse options from arguments argv (number is argc)
Definition: sat.cpp:57
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:39
void update(Space &home, VarArray< Var > &a)
Update array to be a clone of array a.
Definition: array.hpp:995
Sat(Sat &s)
Constructor for cloning.
Definition: sat.cpp:124
bool pos(const View &x)
Test whether x is postive.
Definition: mult.hpp:41
Options for SAT problems.
Definition: sat.cpp:49
Computation spaces.
Definition: core.hpp:1701
Parametric base-class for scripts.
Definition: driver.hh:729
Gecode::FloatVal c(-8, 8)
BoolValBranch BOOL_VAL_MIN(void)
Select smallest value.
Definition: val.hpp:130
IntRelType neg(IntRelType irt)
Return negated relation type of irt.
Definition: irt.hpp:52
Options opt
The options.
Definition: test.cpp:97
Gecode::IntArgs i({1, 2, 3, 4})
void parseDIMACS(const char *f)
Post constraints according to DIMACS file f.
Definition: sat.cpp:141
virtual Space * copy(void)
Perform copying during cloning.
Definition: sat.cpp:130
SatOptions(const char *s)
Initialize options with file name s.
Definition: sat.cpp:54
Disjunction.
Definition: int.hh:952
Passing Boolean variables.
Definition: int.hh:712
Boolean variable array.
Definition: int.hh:808
void parse(int &argc, char *argv[])
Parse options from arguments argv (number is argc)
Definition: options.cpp:540
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:136
BoolVarBranch BOOL_VAR_AFC_MAX(double d, BranchTbl tbl)
Select variable with largest accumulated failure count with decay factor d.
Definition: var.hpp:404
virtual void help(void)
Print help message.
Definition: sat.cpp:69
Example: CNF SAT solver
Definition: sat.cpp:111
Post propagator for SetVar x
Definition: set.hh:767
int main(int argc, char *argv[])
Definition: test.cpp:208
Gecode toplevel namespace
Sat(const SatOptions &opt)
The actual problem.
Definition: sat.cpp:117
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:57
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:904
virtual void help(void)
Print help text.
Definition: options.cpp:486