Skip to content
GitLab
Commit 4979f95f authored by Kučera Petr RNDr. Ph.D.'s avatar Kučera Petr RNDr. Ph.D.
Browse files

progress report in cnfprime

parent 815f3387
Hide whitespace changes
Inline Side-by-side
bin/cnfprime.cpp
View file @ 4979f95f
......@@ -31,6 +31,7 @@ struct config_t : public SUBool::PrgConfigBase
std::string input_file{};
std::string output_file{};
bool unitprop{false};
unsigned progress_step{0};
virtual void InnerDump(unsigned level) const override;
};
......@@ -47,7 +48,10 @@ parse_arguments(int argc, char *argv[])
"Use only unit propagation instead of SAT. It means "
"that the result is not necessarily prime, but it is prime with "
"respect to 1-provability (although not fully as only one round of "
"prime subimplicate finding is performed");
"prime subimplicate finding is performed")("progress-step",
po::value(&conf.progress_step)->default_value(0),
"If positive, then report progress after this many clauses. Has no "
"effect with option -u.");
opts.Add(desc);
if (!opts.Parse(argc, argv, conf))
{
......@@ -62,6 +66,7 @@ config_t::InnerDump(unsigned level) const
SUBool::logs.DumpValue("\t", level, "input_file", input_file);
SUBool::logs.DumpValue("\t", level, "output_file", output_file);
SUBool::logs.DumpValue("\t", level, "unitprop", unitprop);
SUBool::logs.DumpValue("\t", level, "progress_step", progress_step);
}
SUBool::CNF
......@@ -73,7 +78,7 @@ process(const config_t &conf, SUBool::CNF input)
}
else
{
return SUBool::prime_cnf(input);
return SUBool::prime_cnf(input, conf.progress_step);
}
}
......
lib/cnfutil.cpp
View file @ 4979f95f
......@@ -16,15 +16,14 @@
namespace SUBool
{
// Assumes that the CNF is satisfiable.
std::vector<Literal> masked_clause_assump(const Clause &clause,
const std::vector<bool> &mask);
std::vector<Literal> masked_clause_assump(
const Clause &clause, const std::vector<bool> &mask);
Clause masked_clause(const Clause &clause, const std::vector<bool> &mask);
std::optional<Clause> solve_with_learning(
const CNF &prime, const CNF &cnf, unsigned cnf_start_index, CNF *learned,
const Clause *clause, const std::vector<Literal> &assump);
std::unordered_set<Literal>
intersect_lits_with_assign(std::unordered_set<Literal> lits,
const PartialAssignment &alpha);
std::optional<Clause> solve_with_learning(const CNF &prime, const CNF &cnf,
unsigned cnf_start_index, CNF *learned, const Clause *clause,
const std::vector<Literal> &assump);
std::unordered_set<Literal> intersect_lits_with_assign(
std::unordered_set<Literal> lits, const PartialAssignment &alpha);
}; // namespace SUBool
......@@ -49,8 +48,8 @@ SUBool::masked_cnf(CNF cnf, const std::vector<bool> &mask)
}
std::vector<SUBool::Literal>
SUBool::masked_clause_assump(const Clause &clause,
const std::vector<bool> &mask)
SUBool::masked_clause_assump(
const Clause &clause, const std::vector<bool> &mask)
{
std::vector<Literal> assump;
for (unsigned j = 0; j < clause.Size(); ++j)
......@@ -116,7 +115,7 @@ SUBool::is_implicate(const SolverInterface &solver, const Clause &clause)
std::optional<SUBool::Clause>
SUBool::prime_subimplicate(const CNF &cnf, const Clause &clause,
unsigned ignore_var, bool promised_sat)
unsigned ignore_var, bool promised_sat)
{
IncSolverWrapper solver(cnf);
return prime_subimplicate(solver.Solver(), clause, ignore_var, promised_sat);
......@@ -124,11 +123,11 @@ SUBool::prime_subimplicate(const CNF &cnf, const Clause &clause,
std::optional<SUBool::Clause>
SUBool::prime_subimplicate(const SolverInterface &solver, const Clause &clause,
unsigned ignore_var, bool promised_sat)
unsigned ignore_var, bool promised_sat)
{
std::vector<Literal> assump;
std::transform(clause.begin(), clause.end(), std::back_inserter(assump),
literal_negate);
literal_negate);
auto r = solver.Solve(assump);
if (r)
{
......@@ -146,12 +145,13 @@ SUBool::prime_subimplicate(const SolverInterface &solver, const Clause &clause,
}
assump.clear();
std::for_each(subclause.begin(), subclause.end(),
[&assump, &l](const auto &lit) {
if (lit != l)
{
assump.push_back(lit.Negation());
}
});
[&assump, &l](const auto &lit)
{
if (lit != l)
{
assump.push_back(lit.Negation());
}
});
std::shuffle(assump.begin(), assump.end(), sub_rand);
if (!solver.Solve(assump))
{
......@@ -160,9 +160,9 @@ SUBool::prime_subimplicate(const SolverInterface &solver, const Clause &clause,
if (subclause.Size() + 1 < old_size)
{
std::vector<Literal> intersect;
std::set_intersection(
to_check.begin(), to_check.end(), subclause.Literals().begin(),
subclause.Literals().end(), std::back_inserter(intersect));
std::set_intersection(to_check.begin(), to_check.end(),
subclause.Literals().begin(), subclause.Literals().end(),
std::back_inserter(intersect));
to_check = std::move(intersect);
}
}
......@@ -172,9 +172,8 @@ SUBool::prime_subimplicate(const SolverInterface &solver, const Clause &clause,
std::optional<SUBool::Clause>
SUBool::solve_with_learning(const CNF &prime, const CNF &cnf,
unsigned cnf_start_index, CNF *learned,
const Clause *clause,
const std::vector<Literal> &assump)
unsigned cnf_start_index, CNF *learned, const Clause *clause,
const std::vector<Literal> &assump)
{
SimpSolverWrapper wrap;
auto &g = wrap.Solver();
......@@ -208,12 +207,25 @@ SUBool::solve_with_learning(const CNF &prime, const CNF &cnf,
}
SUBool::CNF
SUBool::prime_cnf(const SolverInterface &solver, const CNF &cnf)
SUBool::prime_cnf(
const SolverInterface &solver, const CNF &cnf, size_t progress_step)
{
CNF prime;
bool promised_sat = false;
size_t cnt = 0;
for (const auto &clause : cnf)
{
if (progress_step > 0)
{
++cnt;
if (cnt % progress_step == 0)
{
logs.TLog(3) << 100.0
* (static_cast<double>(cnt)
/ static_cast<double>(cnf.Size()))
<< "%" << std::endl;
}
}
if (prime.SubsumedByAny(clause))
{
continue;
......@@ -226,6 +238,10 @@ SUBool::prime_cnf(const SolverInterface &solver, const CNF &cnf)
promised_sat = true;
prime.PushBack(*p);
}
if (progress_step > 0)
{
logs.TLog(3) << "100%" << std::endl;
}
return prime;
}
......
lib/cnfutil.h
View file @ 4979f95f
......@@ -35,15 +35,13 @@ namespace SUBool
bool is_implicate(const SolverInterface &solver, const Clause &clause);
// promised_sat = cnf is satisfiable.
std::optional<Clause> prime_subimplicate(const CNF &cnf,
const Clause &clause,
unsigned ignore_var = 0,
bool promised_sat = false);
const Clause &clause, unsigned ignore_var = 0,
bool promised_sat = false);
// Solver must be incremental and initialized with a CNF already
std::optional<Clause> prime_subimplicate(const SolverInterface &solver,
const Clause &clause,
unsigned ignore_var = 0,
bool promised_sat = false);
const Clause &clause, unsigned ignore_var = 0,
bool promised_sat = false);
// Clauses at index i for which pred(i) is satisfied are ignored
template <class IgnorePred>
......@@ -51,17 +49,20 @@ namespace SUBool
// solver must be incremental and initialized with a CNF which implies @p cnf
template <class IgnorePred>
CNF prime_cnf_with_ignore(const SolverInterface &solver, const CNF &cnf,
IgnorePred pred);
CNF prime_cnf_with_ignore(
const SolverInterface &solver, const CNF &cnf, IgnorePred pred);
// solver must be incremental and initialized with a CNF which implies @p cnf
CNF prime_cnf(const SolverInterface &solver, const CNF &cnf);
// progress_step determines the number of clauses after which the progress is
// reported. If 0, then progress is not reported.
CNF prime_cnf(
const SolverInterface &solver, const CNF &cnf, size_t progress_step = 0);
inline CNF
prime_cnf(const CNF &cnf)
prime_cnf(const CNF &cnf, size_t progress_step = 0)
{
IncSolverWrapper solver(cnf);
return prime_cnf(solver.Solver(), cnf);
return prime_cnf(solver.Solver(), cnf, progress_step);
}
CNF masked_cnf(SUBool::CNF cnf, const std::vector<bool> &mask);
......@@ -80,8 +81,8 @@ SUBool::prime_cnf_with_ignore(const CNF &cnf, Pred pred)
template <class Pred>
SUBool::CNF
SUBool::prime_cnf_with_ignore(const SolverInterface &solver, const CNF &cnf,
Pred pred)
SUBool::prime_cnf_with_ignore(
const SolverInterface &solver, const CNF &cnf, Pred pred)
{
if (!solver.Solve())
{
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment