Generated on Thu Jan 16 2025 00:00:00 for Gecode by doxygen 1.14.0
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
43using namespace Gecode;
44
49class SatOptions : public Options {
50public:
52 std::string filename;
54 SatOptions(const char* s)
55 : Options(s) {}
56
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
69 virtual void help(void) {
71 std::cerr << "\t(string) " << std::endl
72 << "\t\tdimacs file to parse (.cnf)" << std::endl;
73 }
74};
75
111class Sat : public Script {
112private:
114 BoolVarArray x;
115public:
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
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
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
254 return 0;
255}
256
257// STATISTICS: example-any
virtual void help(void)
Print help text.
Definition options.cpp:494
void parse(int &argc, char *argv[])
Parse options from arguments argv (number is argc)
Definition options.cpp:548
Passing Boolean variables.
Definition int.hh:721
Boolean variable array.
Definition int.hh:820
static void run(const Options &opt, Script *s=NULL)
Options(const char *s)
Initialize options for script with name s.
Definition options.cpp:576
Computation spaces.
Definition core.hpp:1744
Options for SAT problems.
Definition sat.cpp:49
void parse(int &argc, char *argv[])
Parse options from arguments argv (number is argc)
Definition sat.cpp:57
virtual void help(void)
Print help message.
Definition sat.cpp:69
std::string filename
Name of the DIMACS file to parse.
Definition sat.cpp:52
SatOptions(const char *s)
Initialize options with file name s.
Definition sat.cpp:54
virtual Space * copy(void)
Perform copying during cloning.
Definition sat.cpp:130
Sat(const SatOptions &opt)
The actual problem.
Definition sat.cpp:117
void parseDIMACS(const char *f)
Post constraints according to DIMACS file f.
Definition sat.cpp:141
virtual void print(std::ostream &os) const
Print solution.
Definition sat.cpp:136
Sat(Sat &s)
Constructor for cloning.
Definition sat.cpp:124
void parse(int argc, char *argv[])
Parse commandline arguments.
Definition test.cpp:120
Driver::ScriptBase< Driver::IgnoreStepOption< Space > > Script
Base-class for scripts.
Definition driver.hh:801
void branch(Home home, const FloatVarArgs &x, FloatVarBranch vars, FloatValBranch vals, FloatBranchFilter bf=nullptr, FloatVarValPrint vvp=nullptr)
Branch over x with variable selection vars and value selection vals.
Definition branch.cpp:39
void clause(Home home, BoolOpType o, const BoolVarArgs &x, const BoolVarArgs &y, BoolVar z, IntPropLevel ipl=IPL_DEF)
Post domain consistent propagator for Boolean clause with positive variables x and negative variables...
Definition bool.cpp:955
@ BOT_OR
Disjunction.
Definition int.hh:967
Gecode toplevel namespace
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
BoolVarBranch BOOL_VAR_AFC_MAX(double d=1.0, BranchTbl tbl=nullptr)
Select variable with largest accumulated failure count with decay factor d.
Definition var.hpp:404
Options opt
The options.
Definition test.cpp:97
int main(int argc, char *argv[])
Definition test.cpp:208