this repo has no description
dekker.one
1/* -*- mode: C++; c-basic-offset: 2; indent-tabs-mode: nil -*- */
2/*
3 * Main authors:
4 * Vincent Barichard <Vincent.Barichard@univ-angers.fr>
5 *
6 * Copyright:
7 * Vincent Barichard, 2013
8 *
9 * Last modified:
10 * $Date$ by $Author$
11 * $Revision$
12 *
13 * This file is part of Quacode:
14 * http://quacode.barichard.com
15 *
16 * This file is based on gecode/examples/sat.cpp
17 * and is under the same license as given below:
18 *
19 * Main authors:
20 * Raphael Reischuk <reischuk@cs.uni-sb.de>
21 * Guido Tack <tack@gecode.org>
22 *
23 * Copyright:
24 * Raphael Reischuk, 2008
25 * Guido Tack, 2008
26 *
27 * This file is part of Gecode, the generic constraint
28 * development environment:
29 * http://www.gecode.org
30 *
31 * Permission is hereby granted, free of charge, to any person obtaining
32 * a copy of this software and associated documentation files (the
33 * "Software"), to deal in the Software without restriction, including
34 * without limitation the rights to use, copy, modify, merge, publish,
35 * distribute, sublicense, and/or sell copies of the Software, and to
36 * permit persons to whom the Software is furnished to do so, subject to
37 * the following conditions:
38 *
39 * The above copyright notice and this permission notice shall be
40 * included in all copies or substantial portions of the Software.
41 *
42 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
43 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
44 * MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
45 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
46 * LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
47 * OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
48 * WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
49 *
50 */
51
52#include <fstream>
53#include <string>
54#include <vector>
55
56#include <quacode/qspaceinfo.hh>
57#include <gecode/driver.hh>
58
59
60using namespace Gecode;
61
62/** \brief Options for %SAT problems
63 *
64 */
65class QDimacsOptions : public Options {
66public:
67 /// Print strategy or not
68 Gecode::Driver::BoolOption _printStrategy;
69 /// Parameter to decide between optimized quantified constraints or usual ones
70 Driver::BoolOption _qConstraint;
71 /// Name of the QDIMACS file to parse
72 std::string filename;
73 /// Initialize options with file name \a s
74 QDimacsOptions(const char* s, bool _qConstraint0)
75 : Options(s),
76 _printStrategy("-printStrategy","Print strategy",false),
77 _qConstraint("-quantifiedConstraints",
78 "whether to use quantified optimized constraints",
79 _qConstraint0)
80 {
81 add(_printStrategy);
82 add(_qConstraint);
83 }
84 /// Parse options from arguments \a argv (number is \a argc)
85 void parse(int& argc, char* argv[]) {
86 // Parse regular options
87 Options::parse(argc,argv);
88 // Filename, should be at position 1
89 if (argc == 1) {
90 help();
91 exit(1);
92 }
93 filename = argv[1];
94 argc--;
95 }
96 /// Return true if the strategy must be printed
97 bool printStrategy(void) const {
98 return _printStrategy.value();
99 }
100 /// Print help message
101 virtual void help(void) {
102 Options::help();
103 std::cerr << "\t(string) " << std::endl
104 << "\t\tqdimacs file to parse (.cnf)" << std::endl;
105 }
106};
107
108/**
109 * \brief %Example: CNF QSAT solver
110 *
111 * QSAT finds models of Quantified Boolean variables such
112 * that a set of clauses is satisfied or shows that
113 * no such model exists.
114 *
115 * This example parses a Q-Dimacs CNF file in which
116 * the constraints are specified. For each line of
117 * the file a clause propagator is posted.
118 *
119 * Format of Q-Dimacs CNF files:
120 *
121 * A dimacs file starts with comments (each line
122 * starts with c). The number of variables and the
123 * number of clauses is defined by the line
124 *
125 * p cnf \<variables\> \<clauses\>
126 *
127 * Then come the quantifiers of the binder. Each lines
128 * starts with a 'a' for universal quantifier or a 'e'
129 * for existential quantifier. The following number until
130 * zero correspond to the id of the variables that take this
131 * quantifier. All variable of the matrix which does not appear
132 * here are considered as the outermost existential variables
133 * of the problem.
134 *
135 * a \<variable list\>
136 * e \<variable list\>
137 *
138 * Each of the subsequent lines specifies a clause.
139 * A positive literal is denoted by a positive
140 * integer, a negative literal is denoted by the
141 * corresponding negative integer. Each line is
142 * terminated by 0.
143 *
144 * c sample CNF file
145 * p cnf 3 2
146 * 3 -1 0
147 * 1 2 -1 0
148 *
149 * \ingroup Example
150 */
151class QDimacs : public Script, public QSpaceInfo {
152private:
153 /// The Boolean variables
154 typedef std::vector< BoolVarArray > QBoolVarArray;
155 QBoolVarArray qx;
156public:
157 /// The actual problem
158 QDimacs(const QDimacsOptions& opt) : Script(opt), QSpaceInfo() {
159 if (!opt.printStrategy()) strategyMethod(0); // disable build and print strategy
160 parseQDIMACS(opt.filename.c_str(),opt._qConstraint.value());
161 }
162
163 /// Constructor for cloning
164 QDimacs(bool share, QDimacs& s) : Script(share,s), QSpaceInfo(*this,share,s), qx(s.qx) {
165 for (unsigned int i=0; i<qx.size(); i++)
166 qx[i].update(*this,share,s.qx[i]);
167 }
168
169 /// Perform copying during cloning
170 virtual Space*
171 copy(bool share) {
172 return new QDimacs(share,*this);
173 }
174
175
176 /// Post constraints according to QDIMACS file \a f
177 void parseQDIMACS(const char* f, bool usedQuantifiedConstraint) {
178 BoolVarArray x;
179 std::vector<int> x_rk;
180 std::vector<Gecode::TQuantifier> x_quant;
181 int variables = 0;
182 int clauses = 0;
183 std::ifstream dimacs(f);
184 if (!dimacs) {
185 std::cerr << "error: file '" << f << "' not found" << std::endl;
186 exit(1);
187 }
188 std::cout << "Solving problem from QDIMACS file '" << f << "'"
189 << std::endl;
190 std::string line;
191 int c = 0;
192 while (dimacs.good()) {
193 std::getline(dimacs,line);
194 // Comments (ignore them)
195 if (line[0] == 'c' || line == "") {
196 }
197 // Line has format "p cnf <variables> <clauses>"
198 else if (variables == 0 && clauses == 0 &&
199 line[0] == 'p' && line[1] == ' ' &&
200 line[2] == 'c' && line[3] == 'n' &&
201 line[4] == 'f' && line[5] == ' ') {
202 int i = 6;
203 while (line[i] >= '0' && line[i] <= '9') {
204 variables = 10*variables + line[i] - '0';
205 i++;
206 }
207 i++;
208 while (line[i] >= '0' && line[i] <= '9') {
209 clauses = 10*clauses + line[i] - '0';
210 i++;
211 }
212 x = BoolVarArray(*this, variables, 0, 1);
213 x_rk.resize(variables,Int::Limits::max);
214 x_quant.resize(variables,EXISTS);
215 std::cout << "(" << variables << " variables, "
216 << clauses << " clauses)" << std::endl << std::endl;
217 }
218 // Line has format "a <variables>" or "e <variables>" or "r <variables>"
219 else if ( (line[0] == 'a' && line[1] == ' ') ||
220 (line[0] == 'e' && line[1] == ' ') ||
221 (line[0] == 'r' && line[1] == ' ') ) {
222 if (line[0] == 'r') {
223 std::cerr << "format error in dimacs file, \"r\" quantifier not recognized for now" << std::endl;
224 std::cerr << "context: '" << line << "'" << std::endl;
225 std::exit(EXIT_FAILURE);
226 }
227 BoolVarArgs tmp;
228 Gecode::TQuantifier quant = (line[0]=='e')?EXISTS:FORALL;
229 std::vector<int> values;
230 int i = 2;
231 while (line[i] != 0) {
232 if (line[i] == ' ') {
233 i++;
234 continue;
235 }
236 int value = 0;
237 while (line[i] >= '0' && line[i] <= '9') {
238 value = 10 * value + line[i] - '0';
239 i++;
240 }
241 if (value != 0) {
242 values.push_back(value);
243 tmp << x[value-1];
244 x_rk[value-1] = qx.size();
245 x_quant[value-1] = quant;
246 if (quant == FORALL) setForAll(*this,x[value-1]);
247 i++;
248 }
249 }
250
251 std::cout << "( " << values.size() << " ";
252 std::cout << ((quant==EXISTS)?"existential":"universal");
253 std::cout << "variables )"<< std::endl;
254 qx.push_back( BoolVarArray(*this,tmp) );
255 }
256 // Parse regular clause
257 else if (variables > 0 &&
258 ((line[0] >= '0' && line[0] <= '9') || line[0] == '-' || line[0] == ' ')) {
259 c++;
260 std::vector<int> pos;
261 std::vector<int> neg;
262 int i = 0;
263 while (line[i] != 0) {
264 if (line[i] == ' ') {
265 i++;
266 continue;
267 }
268 bool positive = true;
269 if (line[i] == '-') {
270 positive = false;
271 i++;
272 }
273 int value = 0;
274 while (line[i] >= '0' && line[i] <= '9') {
275 value = 10 * value + line[i] - '0';
276 i++;
277 }
278 if (value != 0) {
279 if (positive)
280 pos.push_back(value-1);
281 else
282 neg.push_back(value-1);
283 i++;
284 }
285 }
286
287 // Create positive BoolVarArgs
288 BoolVarArgs positives(pos.size());
289 QBoolVarArgs qpositives(pos.size());
290 for (int i=pos.size(); i--;) {
291 positives[i] = x[pos[i]];
292 qpositives[i] = QBoolVar(x_quant[pos[i]],x[pos[i]],x_rk[pos[i]]);
293 }
294
295 BoolVarArgs negatives(neg.size());
296 QBoolVarArgs qnegatives(neg.size());
297 for (int i=neg.size(); i--;) {
298 negatives[i] = x[neg[i]];
299 qnegatives[i] = QBoolVar(x_quant[neg[i]],x[neg[i]],x_rk[neg[i]]);
300 }
301
302 // Post propagators
303 if (usedQuantifiedConstraint)
304 qclause(*this, BOT_OR, qpositives, qnegatives, 1);
305 else
306 clause(*this, BOT_OR, positives, negatives, 1);
307 }
308 else {
309 std::cerr << "format error in dimacs file" << std::endl;
310 std::cerr << "context: '" << line << "'" << std::endl;
311 std::exit(EXIT_FAILURE);
312 }
313 }
314 dimacs.close();
315 if (clauses != c) {
316 std::cerr << "error: number of specified clauses seems to be wrong."
317 << std::endl;
318 std::exit(EXIT_FAILURE);
319 }
320
321 for (unsigned int i=0; i<qx.size(); i++)
322 branch(*this, qx[i], INT_VAR_NONE(), INT_VAL_MIN());
323
324 // FIN DESCRIPTION PB
325 }
326};
327
328
329/** \brief Main-function
330 */
331int main(int argc, char* argv[]) {
332
333 QDimacsOptions opt("QDIMACS",true);
334 opt.parse(argc,argv);
335
336 // Check whether all arguments are successfully parsed
337 if (argc > 1) {
338 std::cerr << "Could not parse all arguments." << std::endl;
339 opt.help();
340 std::exit(EXIT_FAILURE);
341 }
342
343 // Run SAT solver
344 Script::run<QDimacs,DFS,QDimacsOptions>(opt);
345 return 0;
346}
347
348// STATISTICS: example-any