Fixing minor last things

This commit is contained in:
Mate Soos 2022-03-21 18:26:25 +01:00
parent a7a6475f6f
commit a13b5332c2
3 changed files with 8 additions and 3 deletions

View File

@ -76,6 +76,10 @@ bool CDCL::solve_loop(const uint32_t max_conflicts, CDCL::Model& model, int& sol
if (conflictClause) if (conflictClause)
{ {
conflicts++; conflicts++;
m_sumConflicts++;
if (m_sumConflicts % 1000 == 999) {
cout << "c confl: " << m_sumConflicts << std::endl;
}
if (currentDecisionLevel() == 0) if (currentDecisionLevel() == 0)
{ {
// cout << "Unsatisfiable" << endl; // cout << "Unsatisfiable" << endl;
@ -96,8 +100,8 @@ bool CDCL::solve_loop(const uint32_t max_conflicts, CDCL::Model& model, int& sol
{ {
if (auto variable = nextDecisionVariable()) if (auto variable = nextDecisionVariable())
{ {
cout << "Level " << currentDecisionLevel() << " - "; // cout << "c Level " << currentDecisionLevel() << " - ";
cout << ((m_assignments.size() * 100) / m_variables.size()) << "% of variables assigned." << endl; // cout << ((m_assignments.size() * 100) / m_variables.size()) << "% of variables assigned." << endl;
m_decisionPoints.emplace_back(m_assignmentTrail.size()); m_decisionPoints.emplace_back(m_assignmentTrail.size());
// cout << "Deciding on " << m_variables.at(*variable) << " @" << currentDecisionLevel() << endl; // cout << "Deciding on " << m_variables.at(*variable) << " @" << currentDecisionLevel() << endl;

View File

@ -122,6 +122,7 @@ private:
std::map<size_t, size_t> m_levelForVariable; std::map<size_t, size_t> m_levelForVariable;
/// TODO wolud be good to not have to copy the clauses /// TODO wolud be good to not have to copy the clauses
std::map<Literal, Clause const*> m_reason; std::map<Literal, Clause const*> m_reason;
uint64_t m_sumConflicts = 0;
// Var activity // Var activity
Heap<VarOrderLt> order; Heap<VarOrderLt> order;

View File

@ -177,7 +177,7 @@ int main(int argc, char** argv)
last_line_break = ss.str().size(); last_line_break = ss.str().size();
ss << "v"; ss << "v";
} }
ss << " " << (m.second ? "" : "-") << m.first; ss << " " << (m.second ? "" : "-") << m.first+1;
} }
cout << ss.str() << " 0" << endl; cout << ss.str() << " 0" << endl;
cout << "s SATISFIABLE" << endl; cout << "s SATISFIABLE" << endl;