this repo has no description
dekker.one
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
43using namespace Gecode;
44
45/** \brief Options for %SAT problems
46 *
47 * \relates SAT
48 */
49class SatOptions : public Options {
50public:
51 /// Name of the DIMACS file to parse
52 std::string filename;
53 /// Initialize options with file name \a s
54 SatOptions(const char* s)
55 : Options(s) {}
56 /// Parse options from arguments \a argv (number is \a argc)
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 }
68 /// Print help message
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
76/**
77 * \brief %Example: CNF SAT solver
78 *
79 * SAT finds assignments of Boolean variables such
80 * that a set of clauses is satisfied or shows that
81 * no such assignment exists.
82 *
83 * This example parses a dimacs CNF file in which
84 * the constraints are specified. For each line of
85 * the file a clause propagator is posted.
86 *
87 * Format of dimacs CNF files:
88 *
89 * A dimacs file starts with comments (each line
90 * starts with c). The number of variables and the
91 * number of clauses is defined by the line
92 *
93 * p cnf \<variables\> \<clauses\>
94 *
95 * Each of the subsequent lines specifies a clause.
96 * A positive literal is denoted by a positive
97 * integer, a negative literal is denoted by the
98 * corresponding negative integer. Each line is
99 * terminated by 0.
100 *
101 * c sample CNF file
102 * p cnf 3 2
103 * 3 -1 0
104 * 1 2 -1 0
105 *
106 * Benchmarks on satlib.org, for instance,
107 * are in the dimacs CNF format.
108 *
109 * \ingroup Example
110 */
111class Sat : public Script {
112private:
113 /// The Boolean variables
114 BoolVarArray x;
115public:
116 /// The actual problem
117 Sat(const SatOptions& opt)
118 : Script(opt) {
119 parseDIMACS(opt.filename.c_str());
120 branch(*this, x, BOOL_VAR_AFC_MAX(), BOOL_VAL_MIN());
121 }
122
123 /// Constructor for cloning
124 Sat(Sat& s) : Script(s) {
125 x.update(*this, s.x);
126 }
127
128 /// Perform copying during cloning
129 virtual Space*
130 copy(void) {
131 return new Sat(*this);
132 }
133
134 /// Print solution
135 virtual void
136 print(std::ostream& os) const {
137 os << "solution:\n" << x << std::endl;
138 }
139
140 /// Post constraints according to DIMACS file \a f
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
237/** \brief Main-function
238 * \relates SAT
239 */
240int 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