57 void parse(
int& argc,
char* argv[]) {
71 std::cerr <<
"\t(string) " << std::endl
72 <<
"\t\tdimacs file to parse (.cnf)" << std::endl;
125 x.update(*
this, s.x);
131 return new Sat(*
this);
137 os <<
"solution:\n" << x << std::endl;
144 std::ifstream dimacs(f);
146 std::cerr <<
"error: file '" << f <<
"' not found" << std::endl;
149 std::cout <<
"Solving problem from DIMACS file '" << f <<
"'"
153 while (dimacs.good()) {
154 std::getline(dimacs,line);
156 if (line[0] ==
'c' || line ==
"") {
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] ==
' ') {
164 while (line[i] >=
'0' && line[i] <=
'9') {
165 variables = 10*variables + line[i] -
'0';
169 while (line[i] >=
'0' && line[i] <=
'9') {
170 clauses = 10*clauses + line[i] -
'0';
173 std::cout <<
"(" << variables <<
" variables, "
174 << clauses <<
" clauses)" << std::endl << std::endl;
179 else if (variables > 0 &&
180 ((line[0] >=
'0' && line[0] <=
'9') || line[0] ==
'-' || line[0] ==
' ')) {
182 std::vector<int> pos;
183 std::vector<int>
neg;
185 while (line[i] != 0) {
186 if (line[i] ==
' ') {
190 bool positive =
true;
191 if (line[i] ==
'-') {
196 while (line[i] >=
'0' && line[i] <=
'9') {
197 value = 10 * value + line[i] -
'0';
202 pos.push_back(value-1);
204 neg.push_back(value-1);
211 for (
int i=pos.size(); i--;)
212 positives[i] = x[pos[i]];
215 for (
int i=
neg.size(); i--;)
216 negatives[i] = x[
neg[i]];
222 std::cerr <<
"format error in dimacs file" << std::endl;
223 std::cerr <<
"context: '" << line <<
"'" << std::endl;
224 std::exit(EXIT_FAILURE);
229 std::cerr <<
"error: number of specified clauses seems to be wrong."
231 std::exit(EXIT_FAILURE);
240int main(
int argc,
char* argv[]) {
247 std::cerr <<
"Could not parse all arguments." << std::endl;
249 std::exit(EXIT_FAILURE);
virtual void help(void)
Print help text.
void parse(int &argc, char *argv[])
Parse options from arguments argv (number is argc)
Passing Boolean variables.
static void run(const Options &opt, Script *s=NULL)
Options(const char *s)
Initialize options for script with name s.
Options for SAT problems.
void parse(int &argc, char *argv[])
Parse options from arguments argv (number is argc)
virtual void help(void)
Print help message.
std::string filename
Name of the DIMACS file to parse.
SatOptions(const char *s)
Initialize options with file name s.
virtual Space * copy(void)
Perform copying during cloning.
Sat(const SatOptions &opt)
The actual problem.
void parseDIMACS(const char *f)
Post constraints according to DIMACS file f.
virtual void print(std::ostream &os) const
Print solution.
Sat(Sat &s)
Constructor for cloning.
void parse(int argc, char *argv[])
Parse commandline arguments.
Driver::ScriptBase< Driver::IgnoreStepOption< Space > > Script
Base-class for scripts.
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.
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...
Gecode toplevel namespace
BoolValBranch BOOL_VAL_MIN(void)
Select smallest value.
IntRelType neg(IntRelType irt)
Return negated relation type of irt.
BoolVarBranch BOOL_VAR_AFC_MAX(double d=1.0, BranchTbl tbl=nullptr)
Select variable with largest accumulated failure count with decay factor d.
int main(int argc, char *argv[])