22 for(std::map<literalt, unsigned>::const_iterator it=
pb_constraintmap.begin();
24 d_sum += ((*it).second);
28 out <<
"# PBType: E" <<
"\n";
29 out <<
"# PBGoal: " <<
goal <<
"\n";
33 out <<
"# PBType: SE" <<
"\n";
34 out <<
"# PBGoal: " << d_sum <<
"\n";
35 out <<
"# PBObj : MIN" <<
"\n";
39 out <<
"# PBType: GE" <<
"\n";
40 out <<
"# PBGoal: " << 0 <<
"\n";
41 out <<
"# PBObj : MAX" <<
"\n";
48 int dimacs_lit=lit_entry.first.dimacs();
49 out <<
"v" << dimacs_lit <<
" c" << lit_entry.second <<
"\n";
64 if(command.substr(command.length(), 1)!=
"/")
83 command +=
" -f temp.cnf";
90 command +=
" -S 1000 -D 1 -H -I -a";
95 command +=
" -S 1000 -D 1 -I -a";
100 command +=
" -S 1000 -D 1 -a";
106 command +=
" -a > temp.out";
108 int res=system(command.c_str());
111 std::ifstream
file(
"temp.out");
114 bool satisfied=
false;
118 error() <<
"Unable to read SAT results!" <<
eom;
124 while(file && !file.eof ())
126 std::getline(file, line);
127 if(strstr(line.c_str(),
128 "Variable Assignments Satisfying CNF Formula:")!=
nullptr)
146 else if(strstr(line.c_str(),
"SAT... SUM")!=
nullptr)
149 sscanf(line.c_str(),
"%*s %*s %*s %d", &
opt_sum);
151 else if(strstr(line.c_str(),
"SAT - All implied")!=
nullptr)
156 "%*s %*s %*s %*s %*s %*s %*s %*s %*s %*s %*s %d",
159 else if(strstr(line.c_str(),
"SAT... Solution")!=
nullptr)
162 sscanf(line.c_str(),
"%*s %*s %*s %d", &
opt_sum);
164 else if(strstr(line.c_str(),
"Optimal Soln")!=
nullptr)
167 if(strstr(line.c_str(),
"time out")!=
nullptr)
169 status() <<
"WARNING: TIMED OUT. SOLUTION MAY BE INCORRECT." 173 sscanf(line.c_str(),
"%*s %*s %*s %d", &
opt_sum);
182 std::ofstream
file(
"temp.cnf");
186 std::ofstream pbfile(
"temp.cnf.pb");
203 "PBS checker: system is UNSATISFIABLE" <<
eom;
208 "PBS checker: system is SATISFIABLE";
222 int dimacs_lit=a.
dimacs();
226 bool neg=(dimacs_lit < 0);
228 dimacs_lit=-dimacs_lit;
230 std::set<int>::const_iterator f=
assigned.find(dimacs_lit);
virtual tvt l_get(literalt a) const
virtual resultt prop_solve()
static mstreamt & eom(mstreamt &m)
virtual void write_dimacs_pb(std::ostream &out)
virtual void write_dimacs_cnf(std::ostream &out)
std::map< literalt, unsigned > pb_constraintmap
virtual size_t no_variables() const override