Go to the documentation of this file.
61 void parse(
int& argc,
char* argv[]) {
75 std::cerr <<
"\t(string) " << std::endl
76 <<
"\t\tdimacs file to parse (.cnf)" << std::endl;
123 parseDIMACS(
opt.filename.c_str());
135 return new Sat(share,*
this);
141 os <<
"solution:\n" <<
x << std::endl;
148 std::ifstream dimacs(
f);
150 std::cerr <<
"error: file '" <<
f <<
"' not found" << std::endl;
153 std::cout <<
"Solving problem from DIMACS file '" <<
f <<
"'"
157 while (dimacs.good()) {
158 std::getline(dimacs,line);
160 if (line[0] ==
'c' || line ==
"") {
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] ==
' ') {
168 while (line[
i] >=
'0' && line[
i] <=
'9') {
169 variables = 10*variables + line[
i] -
'0';
173 while (line[
i] >=
'0' && line[
i] <=
'9') {
174 clauses = 10*clauses + line[
i] -
'0';
177 std::cout <<
"(" << variables <<
" variables, "
178 << clauses <<
" clauses)" << std::endl << std::endl;
183 else if (variables > 0 &&
184 ((line[0] >=
'0' && line[0] <=
'9') || line[0] ==
'-' || line[0] ==
' ')) {
186 std::vector<int>
pos;
187 std::vector<int>
neg;
189 while (line[
i] != 0) {
190 if (line[
i] ==
' ') {
195 if (line[
i] ==
'-') {
200 while (line[
i] >=
'0' && line[
i] <=
'9') {
201 value = 10 * value + line[
i] -
'0';
206 pos.push_back(value-1);
208 neg.push_back(value-1);
215 for (
int i=
pos.size();
i--;)
219 for (
int i=
neg.size();
i--;)
226 std::cerr <<
"format error in dimacs file" << std::endl;
227 std::cerr <<
"context: '" << line <<
"'" << std::endl;
228 std::exit(EXIT_FAILURE);
233 std::cerr <<
"error: number of specified clauses seems to be wrong."
235 std::exit(EXIT_FAILURE);
244 int main(
int argc,
char* argv[]) {
251 std::cerr <<
"Could not parse all arguments." << std::endl;
253 std::exit(EXIT_FAILURE);
257 Script::run<Sat,DFS,SatOptions>(
opt);
Post propagator for SetVar x
virtual Space * copy(bool share)
Perform copying during cloning.
Sat(bool share, Sat &s)
Constructor for cloning.
Gecode::IntArgs i(4, 1, 2, 3, 4)
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.
void update(Space &home, bool share, VarImpVar< VarImp > &y)
Update this variable to be a clone of variable y.
Options for SAT problems.
Gecode toplevel namespace
virtual void help(void)
Print help message.
virtual void print(std::ostream &os) const
Print solution.
void parse(int &argc, char *argv[])
Parse options from arguments argv (number is argc)
Passing Boolean variables.
Parametric base-class for scripts.
void parse(int &argc, char *argv[])
Parse options from arguments argv (number is argc)
void parseDIMACS(const char *f)
Post constraints according to DIMACS file f.
BoolValBranch BOOL_VAL_MIN(void)
Select smallest value.
void positive(int n, const char *l)
Check whether n is in range and strictly positive, otherwise throw out of limits with information l.
BoolVarBranch BOOL_VAR_AFC_MAX(double d, BranchTbl tbl)
Select variable with largest accumulated failure count with decay factor d.
Sat(const SatOptions &opt)
The actual problem.
IntRelType neg(IntRelType irt)
Return negated relation type of irt.
virtual void help(void)
Print help text.
SatOptions(const char *s)
Initialize options with file name s.
std::string filename
Name of the DIMACS file to parse.
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...
Post propagator for f(x \diamond_{\mathit{op}} y) \sim_r z \f$ void rel(Home home
Gecode::FloatVal c(-8, 8)
int main(int argc, char *argv[])
bool pos(const View &x)
Test whether x is postive.