47 using namespace Gecode;
61 void parse(
int& argc,
char* argv[]) {
75 std::cerr <<
"\t(string) " << std::endl
76 <<
"\t\tdimacs file to parse (.cnf)" << std::endl;
128 x.update(*
this, share, s.x);
134 return new Sat(share,*
this);
140 os <<
"solution:\n" <<
x << std::endl;
147 std::ifstream dimacs(f);
149 std::cerr <<
"error: file '" << f <<
"' not found" << std::endl;
152 std::cout <<
"Solving problem from DIMACS file '" << f <<
"'"
156 while (dimacs.good()) {
157 std::getline(dimacs,line);
159 if (line[0] ==
'c' || line ==
"") {
162 else if (variables == 0 && clauses == 0 &&
163 line[0] ==
'p' && line[1] ==
' ' &&
164 line[2] ==
'c' && line[3] ==
'n' &&
165 line[4] ==
'f' && line[5] ==
' ') {
167 while (line[i] >=
'0' && line[i] <=
'9') {
168 variables = 10*variables + line[
i] -
'0';
172 while (line[i] >=
'0' && line[i] <=
'9') {
173 clauses = 10*clauses + line[
i] -
'0';
176 std::cout <<
"(" << variables <<
" variables, "
177 << clauses <<
" clauses)" << std::endl << std::endl;
182 else if (variables > 0 &&
183 ((line[0] >=
'0' && line[0] <=
'9') || line[0] ==
'-' || line[0] ==
' ')) {
185 std::vector<int>
pos;
186 std::vector<int>
neg;
188 while (line[i] != 0) {
189 if (line[i] ==
' ') {
194 if (line[i] ==
'-') {
199 while (line[i] >=
'0' && line[i] <=
'9') {
200 value = 10 * value + line[
i] -
'0';
205 pos.push_back(value-1);
207 neg.push_back(value-1);
214 for (
int i=pos.size(); i--;)
215 positives[i] =
x[pos[i]];
218 for (
int i=neg.size(); i--;)
219 negatives[i] =
x[neg[i]];
225 std::cerr <<
"format error in dimacs file" << std::endl;
226 std::cerr <<
"context: '" << line <<
"'" << std::endl;
227 std::exit(EXIT_FAILURE);
232 std::cerr <<
"error: number of specified clauses seems to be wrong."
234 std::exit(EXIT_FAILURE);
243 int main(
int argc,
char* argv[]) {
250 std::cerr <<
"Could not parse all arguments." << std::endl;
252 std::exit(EXIT_FAILURE);
256 Script::run<Sat,DFS,SatOptions>(
opt);