Skip to content

Commit

Permalink
Modifying the parser to accept the new format of WCNF files. Small fi…
Browse files Browse the repository at this point in the history 
…xes to the topK mode.
  • Loading branch information
@marekpiotrow
marekpiotrow committed Dec 23, 2020
1 parent aef43f0 commit 3deae50
Show file tree
Hide file tree
Showing 2 changed files with 53 additions and 17 deletions.
10 changes: 5 additions & 5 deletions MsSolver.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -488,9 +488,10 @@ void MsSolver::maxsat_solve(solve_Command cmd)
int used_cpu = cpuTime();
first_time=true; limitTime(used_cpu + (opt_cpu_lim - used_cpu)/4);
}
lbool status;
while (1) {
if (use_base_assump) for (int i = 0; i < base_assump.size(); i++) assump_ps.push(base_assump[i]);
lbool status =
status =
base_assump.size() == 1 && base_assump[0] == assump_lit ? l_True :
base_assump.size() == 1 && base_assump[0] == ~assump_lit ? l_False :
sat_solver.solveLimited(assump_ps);
Expand Down Expand Up @@ -578,6 +579,7 @@ void MsSolver::maxsat_solve(solve_Command cmd)
else {
best_goalvalue = Int_MAX;
if (soft_unsat.size() > 0) sat_solver.addClause(soft_unsat);
else { status = l_False; break; }
for (int i = 0; i < soft_cls.size(); i++)
if (soft_unsat[i] == soft_cls[i].snd->last() && soft_cls[i].snd->size() > 1 &&
top_impl_gen.at(var(soft_unsat[i]))) {
Expand Down Expand Up @@ -649,10 +651,7 @@ void MsSolver::maxsat_solve(solve_Command cmd)
convertPbs(false);
}
} else { // UNSAT returned
if (assump_ps.size() == 0 && assump_lit == lit_Undef) {
if (opt_output_top > 0) printf("v \n");
break;
}
if (assump_ps.size() == 0 && assump_lit == lit_Undef) break;
{
Minisat::vec<Lit> core_mus;
if (opt_core_minimization) {
Expand Down Expand Up @@ -871,6 +870,7 @@ void MsSolver::maxsat_solve(solve_Command cmd)
}
} // END OF LOOP

if (status == l_False && opt_output_top > 0) printf("v\n");
if (goal_gcd != 1) {
if (best_goalvalue != Int_MAX) best_goalvalue *= goal_gcd;
if (LB_goalvalue != Int_MIN) LB_goalvalue *= goal_gcd;
Expand Down
60 changes: 48 additions & 12 deletions PbParser.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -330,7 +330,8 @@ static bool parse_wcnfs(B& in, S& solver, bool wcnf_format, Int hard_bound)
{
vec<Lit> ps, gps; vec<Int> gCs; vec<char> tmp;
int gvars = 0;
Int one = 1, weight;
Int one(1), weight(0);
int n_vars = 0, n_constrs = 0;

#ifdef MAXPRE
extern bool opt_use_maxpre;
Expand All @@ -340,51 +341,85 @@ static bool parse_wcnfs(B& in, S& solver, bool wcnf_format, Int hard_bound)
extern maxPreprocessor::PreprocessorInterface *maxpre_ptr;
std::vector<std::vector<int> > clauses;
std::vector<uint64_t> weights;
Int weight_sum(0);
#endif

tmp.clear(); tmp.growTo(15,0);
while (*in != EOF){
weight = (wcnf_format ? parseInt(in) : 1);
skipWhitespace(in);
if (*in == 'h') ++in, weight = hard_bound;
else
weight = (wcnf_format ? parseInt(in) : Int(1));
#ifdef MAXPRE
if (opt_use_maxpre) clauses.push_back(std::vector<int>());
#endif
while (1) {
bool negated = parseLit(in,tmp);
if (tmp.size() == 2 && tmp[0] == '0') break;
int v = atoi(&tmp[0]);
#ifdef MAXPRE
int v = atoi(tmp);
if (opt_use_maxpre) clauses.back().push_back(negated ? -v : v), ps.push(mkLit(v, negated));
else
#endif
{
if (solver.declared_n_vars < 0) {
vec<char> t(15,0);
while (n_vars < v) { sprintf(&t[0], "%d", ++n_vars); solver.getVar(t); }
}
ps.push(mkLit(solver.getVar(tmp), negated));
}
}
skipEndOfLine(in);
#ifdef MAXPRE
if (opt_use_maxpre) {
weights.push_back(tolong(weight));
if (weight < hard_bound) solver.storeSoftClause(ps, tolong(weight));
if (weight <= 0) { clauses.pop_back(); ps.clear(); continue; }
weights.push_back(weight >= hard_bound ? 0 : tolong(weight));
if (weight < hard_bound) {
solver.storeSoftClause(ps, tolong(weight));
weight_sum += weight;
}
} else
#endif
if (weight >= hard_bound) {
if (weight <= 0) { ps.clear(); continue; }
else if (weight >= hard_bound) {
if (!solver.addClause(ps)) return false;
} else {
gvars++;
if (ps.size() == 1) {
if (!opt_maxsat_msu) gps.push(~ps.last()), gCs.push(weight);
} else {
sprintf(&tmp[0],"#%d",gvars);
ps.push(mkLit(solver.getVar(tmp), true));
ps.push(lit_Undef);
if (!opt_maxsat_msu) gps.push(ps.last()), gCs.push(weight);
}
}
#ifdef BIG_WEIGHTS
solver.storeSoftClause(ps, weight);
#else
solver.storeSoftClause(ps, tolong(weight));
#endif
}
if (solver.declared_n_constrs < 0 && ps.size() > 0) n_constrs++;
ps.clear();
}
if (!opt_use_maxpre) {
if (solver.declared_n_vars < 0 && n_vars > 0) solver.declared_n_vars = n_vars;
if (solver.declared_n_constrs < 0 && n_constrs > 0) solver.declared_n_constrs = n_constrs;
gvars = solver.soft_cls.size();
tmp.clear(); tmp.growTo(16,0);
for (int i = 0; i < gvars; i++)
if (solver.soft_cls[i].snd->last() == lit_Undef) {
sprintf(&tmp[0],"#%d",i + 1);
Lit p = mkLit(solver.getVar(tmp), true);
solver.soft_cls[i].snd->last() = p;
if (!opt_maxsat_msu) gps[i] = p;
}
}
#ifdef MAXPRE
if (opt_use_maxpre) {
reportf("Using MaxPre - an MaxSAT preprocessor by Tuukka Korhonen (2017) with techniques: %s\n",
opt_maxpre_str);
if (++weight_sum < hard_bound) hard_bound = weight_sum;
uint64_t topWeight = tolong(hard_bound);
for (auto &w : weights)
if (w == 0 || w > topWeight) w = topWeight;
maxpre_ptr = new maxPreprocessor::PreprocessorInterface(clauses, weights, topWeight);
if (opt_maxpre_skip >= 10) maxpre_ptr->setSkipTechnique(opt_maxpre_skip);
if (opt_maxpre_time > 0) maxpre_ptr->preprocess(std::string(opt_maxpre_str), 0, opt_maxpre_time);
Expand All @@ -395,6 +430,7 @@ static bool parse_wcnfs(B& in, S& solver, bool wcnf_format, Int hard_bound)
std::vector<int> labels;
maxpre_ptr->getInstance(clauses, weights, labels);
assert(clauses.size() == weights.size());
tmp.clear(); tmp.growTo(15,0);
for (unsigned maxvar = 1, i = 0 ; i < clauses.size(); i++) {
ps.clear();
for (unsigned j = 0; j < clauses[i].size(); j++) {
Expand All @@ -418,7 +454,7 @@ static bool parse_wcnfs(B& in, S& solver, bool wcnf_format, Int hard_bound)
}
#endif
if (gvars == 0 && !opt_maxsat_msu) {
tmp.clear(); tmp.growTo(15,0);
tmp.clear(); tmp.growTo(10,0);
sprintf(&tmp[0],"#%d",1);
gps.push(mkLit(solver.getVar(tmp)));
gCs.push(one);
Expand Down Expand Up @@ -464,7 +500,7 @@ void parse_PB_file(cchar* filename, PbSolver& solver, bool old_format, bool abor
template<class B, class S>
static bool parse_WCNF(B& in, S& solver, bool abort_on_error)
{
Int hard_bound = Int_MAX;
Int hard_bound = WEIGHT_MAX;
bool wcnf_format = true;

try{
Expand Down

0 comments on commit 3deae50

Please sign in to comment.