Commit 2b5f7274 authored by Kučera Petr RNDr. Ph.D.'s avatar Kučera Petr RNDr. Ph.D.
Browse files

UnitPropagatorM fixes and tests

parent 807ea354
......@@ -8,6 +8,7 @@
*/
#include <cxxopts.hpp>
#include "normalform.h"
#include "prgutil.h"
const std::string prg_name = "cnfdiff";
......
......@@ -13,7 +13,8 @@
#include <sstream>
#include "logstream.h"
#include "normalform.h"
#include "sbexception.h"
#include "util.h"
namespace SUBool
{
......@@ -137,12 +138,6 @@ namespace SUBool
std::string author_year_info();
void print_version(const std::string &prg_name, const std::string &prg_desc);
constexpr const char *
bool_to_string(bool a)
{
return (a ? "true" : "false");
}
template <class T>
void
dump_value(const std::string &line_prefix, unsigned level,
......
......@@ -5,10 +5,11 @@
/**@file unitprop2.h
* Linear time unit propagation (with CNF managed by the propagator).
*/
#include <sstream>
#include "unitprop2.h"
#include "sbexception.h"
#include <sstream>
#include "unitprop2.h"
#include "util.h"
SUBool::UnitPropagatorM::UnitPropagatorM(const CNF &cnf) : UnitPropagatorM()
{
......@@ -63,6 +64,7 @@ SUBool::UnitPropagatorM::AddUnitClause(Clause clause)
const auto &lit = clause[0];
if (mUnitClauses.find(lit.Negation()) != mUnitClauses.end())
{
mContradictory = true;
return false;
}
mUnitClauses.insert(lit);
......@@ -110,7 +112,7 @@ SUBool::UnitPropagatorM::RemoveClause(iterator i_clause)
mClauses.erase(i_clause);
}
void
SUBool::UnitPropagatorM::const_iterator_list::iterator
SUBool::UnitPropagatorM::UpdateWatch(const Literal &lit,
const_iterator_list::iterator it) const
{
......@@ -118,6 +120,7 @@ SUBool::UnitPropagatorM::UpdateWatch(const Literal &lit,
auto &w1 = i_clause->w1;
auto &w2 = i_clause->w2;
const Clause &clause = i_clause->clause;
std::cout << "updating watch for " << *i_clause << std::endl;
bool watch_updated = false;
if (clause.Size() > 2)
{
......@@ -145,33 +148,42 @@ SUBool::UnitPropagatorM::UpdateWatch(const Literal &lit,
}
}
}
if (!watch_updated)
{
++it;
}
if (clause[w1.index].Value(mValues) == PartialValue::FALSE)
{
std::swap(w1, w2);
}
if (!watch_updated)
{
std::cout << "Watch not updated" << std::endl;
return std::next(it);
}
std::cout << "Updated watch " << *i_clause << std::endl;
return it;
}
SUBool::UnitPropagatorM::CLAUSE_STATE
SUBool::UnitPropagatorM::ClauseStatus(const_iterator i_clause) const
{
std::cout << "Checking status of clause " << *i_clause << std::endl;
std::cout << "with values: " << mValues << std::endl;
PartialValue v1 = i_clause->FirstWatchedLiteral().Value(mValues);
PartialValue v2 = i_clause->SecondWatchedLiteral().Value(mValues);
if (v1 == PartialValue::TRUE || v2 == PartialValue::TRUE)
{
std::cout << "SATISFIED" << std::endl;
return SATISFIED;
}
if (v1 == PartialValue::UNDEF && v2 == PartialValue::UNDEF)
{
std::cout << "OTHER" << std::endl;
return OTHER;
}
if (v1 == PartialValue::UNDEF || v2 == PartialValue::UNDEF)
{
std::cout << "UNIT" << std::endl;
return UNIT;
}
std::cout << "UNSATISFIED" << std::endl;
return UNSATISFIED;
}
......@@ -182,14 +194,17 @@ SUBool::UnitPropagatorM::UpdateWatches(const Literal &lit) const
auto it = mWatchedClauses[neg_index].begin();
while (it != mWatchedClauses[neg_index].end())
{
UpdateWatch(lit, it);
switch (ClauseStatus(*it))
auto &i_clause = *it;
it = UpdateWatch(lit, it);
switch (ClauseStatus(i_clause))
{
case UNSATISFIED:
return false;
case UNIT:
{
mLiteralQueue.push((*it)->FirstWatchedLiteral());
std::cout << "Adding " << i_clause->FirstWatchedLiteral()
<< " to queue" << std::endl;
mLiteralQueue.push(i_clause->FirstWatchedLiteral());
break;
}
default:
......@@ -202,6 +217,7 @@ SUBool::UnitPropagatorM::UpdateWatches(const Literal &lit) const
bool
SUBool::UnitPropagatorM::AddLiteralValue(const Literal &lit) const
{
std::cout << "Adding literal value " << lit << std::endl;
switch (lit.Value(mValues))
{
case PartialValue::FALSE:
......@@ -209,8 +225,12 @@ SUBool::UnitPropagatorM::AddLiteralValue(const Literal &lit) const
case PartialValue::TRUE:
return true;
case PartialValue::UNDEF:
{
mValues[lit.Variable()] = lit.Value(PartialValue::TRUE);
return UpdateWatches(lit);
auto ret = UpdateWatches(lit);
std::cout << "returning " << bool_to_string(ret) << std::endl;
return ret;
}
default:
throw InvariantFailedException("UnitPropagator::AddLiteralValue",
"Unknown literal value");
......@@ -231,12 +251,15 @@ SUBool::UnitPropagatorM::PropInit() const
bool
SUBool::UnitPropagatorM::PropagateQueue() const
{
bool no_conflict = false;
bool no_conflict = true;
while (!mLiteralQueue.empty() && no_conflict)
{
no_conflict = AddLiteralValue(mLiteralQueue.front());
auto lit = mLiteralQueue.front();
std::cout << "queue literal " << lit << std::endl;
mLiteralQueue.pop();
no_conflict = AddLiteralValue(lit);
}
std::cout << "returning " << bool_to_string(no_conflict) << std::endl;
return no_conflict;
}
......@@ -251,54 +274,28 @@ SUBool::UnitPropagatorM::InnerPropagate(
PropInit();
if (!PropagateQueue())
{
// could be cached, but rarely happens, so maybe not worth it
mContradictory = true;
return false;
}
for (const auto &lit : assump)
{
if (!AddLiteralValue(lit) || !PropagateQueue())
std::cout << "Assumption literal: " << lit << std::endl;
if (lit.Variable() <= MaxVariable()
&& (!AddLiteralValue(lit) || !PropagateQueue()))
{
std::cout << "false" << std::endl;
return false;
}
}
std::cout << "true" << std::endl;
return true;
}
#if 0
SUBool::PartialAssignment beta(MaxVariable(), PartialValue::UNDEF);
if (mWatchedClauses.size() < 2 * MaxVariable())
{
mWatchedClauses.resize(2 * MaxVariable());
}
std::queue<Literal> lq;
PropInit(assump, lq);
while (!lq.empty())
{
if (lq.front().Variable() <= MaxVariable())
{
int conflict = AddLiteralValue(lq.front(), lq, beta);
if (conflict >= 0)
{
return conflict;
}
}
lq.pop();
}
if (conseq != nullptr)
{
*conseq = std::move(beta);
if (assump.Size() > conseq->Size())
{
auto s = conseq->Size();
conseq->Resize(assump.Size(), PartialValue::UNDEF);
for (unsigned var = s + 1; var <= assump.Size(); ++var)
{
(*conseq)[var] = assump[var];
}
}
}
return -1;
std::ostream &
SUBool::operator<<(std::ostream &out,
const SUBool::UnitPropagatorM::ClauseInfo &ci)
{
out << ci.clause << " (" << ci.FirstWatchedLiteral() << ", "
<< ci.SecondWatchedLiteral() << ")";
return out;
}
#endif
......@@ -5,8 +5,8 @@
/**@file unitprop2.h
* Linear time unit propagation (with CNF managed by the propagator).
*/
#ifndef __UNITPROP_H
#define __UNITPROP_H
#ifndef __UNITPROP2_H
#define __UNITPROP2_H
#include <list>
#include <queue>
......@@ -20,6 +20,7 @@ namespace SUBool
{
class UnitPropagatorM
{
public:
struct ClauseInfo;
using clause_list = std::list<ClauseInfo>;
using iterator = clause_list::iterator;
......@@ -66,7 +67,7 @@ namespace SUBool
clause_list mClauses;
mutable std::vector<const_iterator_list> mWatchedClauses;
std::unordered_set<Literal> mUnitClauses;
bool mContradictory; // cannot be unset once set to true
mutable bool mContradictory; // cannot be unset once set to true
unsigned mMaxVariable;
mutable PartialAssignment mValues;
mutable std::queue<Literal> mLiteralQueue;
......@@ -84,8 +85,8 @@ namespace SUBool
};
bool UpdateWatches(const Literal &lit) const;
void UpdateWatch(const Literal &lit,
const_iterator_list::iterator it) const;
const_iterator_list::iterator
UpdateWatch(const Literal &lit, const_iterator_list::iterator it) const;
CLAUSE_STATE ClauseStatus(const_iterator i_clause) const;
bool AddUnitClause(Clause clause);
......@@ -138,6 +139,11 @@ namespace SUBool
return InnerPropagate(assump);
}
bool
Contradictory() const
{
return mContradictory;
}
unsigned
MaxVariable() const
{
......@@ -156,6 +162,9 @@ namespace SUBool
bool AddClause(Clause clause);
void RemoveClause(iterator i_clause);
};
std::ostream &operator<<(std::ostream &out,
const UnitPropagatorM::ClauseInfo &ci);
} // namespace SUBool
#endif
......@@ -95,6 +95,13 @@ namespace SUBool
}
return os;
}
constexpr const char *
bool_to_string(bool a)
{
return (a ? "true" : "false");
}
} // namespace SUBool
// Implementation
......
......@@ -16,6 +16,7 @@ su_add_test_exec(horn false)
su_add_test_exec(schoning false)
su_add_test_exec(assign false)
su_add_test_exec(unitprop false)
su_add_test_exec(unitprop2 false)
su_add_test_exec(resolve false)
su_add_test_exec(glucose true)
su_add_test_exec(cnfcompress false)
......
......@@ -17,9 +17,10 @@ namespace SUBool
bool TestUnitPropCNF() const;
bool TestAmoProduct10() const;
bool TestStdIn() const;
public:
bool RunTests() const;
public:
bool RunTests() const;
};
};
}; // namespace SUBool
#endif
/*
* Project SUBool
* Petr Kucera, 2016
*/
/**@file test_unitprop2.cpp
* Contains tests of UnitPropagatorM (reimplemented.
*/
#include <chrono>
#include <sstream>
#include "random_utils.h"
#include "test_unitprop2.h"
#include "unitprop.h"
#include "unitprop2.h"
#include "util.h"
const char *dimacs_simple = "c\n"
"c start with comments\n"
"c\n"
"c\n"
"p cnf 5 3\n"
"1 -5 4 0\n"
"-1 5 3 4 0\n"
"-3 -4 0";
const char *dimacs_quinn = "c quinn.cnf\n"
"c\n"
"p cnf 16 18\n"
" 1 2 0\n"
" -2 -4 0\n"
" 3 4 0\n"
" -4 -5 0\n"
" 5 -6 0\n"
" 6 -7 0\n"
" 6 7 0\n"
" 7 -16 0\n"
" 8 -9 0\n"
" -8 -14 0\n"
" 9 10 0\n"
" 9 -10 0\n"
"-10 -11 0\n"
" 10 12 0\n"
" 11 12 0\n"
" 13 14 0\n"
" 14 -15 0\n"
" 15 16 0";
const char *dimacs_horn = "c\n"
"c A horn formula\n"
"c\n"
"p cnf 7 8\n"
"2 0\n"
"-4 0\n"
"5 -7 -2 0\n"
"-1 3 -4 0\n"
"-5 -4 -2 1 0\n"
"3 -1 -2 0\n"
"5 -2 0\n"
"1 -2 -3 -4 0";
const char *amo_product_10 = "c AMO Product\n"
"p cnf 16 24\n"
"-2 11 0\n"
"-1 11 0\n"
"-1 -2 0\n"
"-3 12 0\n"
"-11 12 0\n"
"-3 -11 0\n"
"-4 13 0\n"
"-12 13 0\n"
"-4 -12 0\n"
"-5 14 0\n"
"-13 14 0\n"
"-5 -13 0\n"
"-6 15 0\n"
"-14 15 0\n"
"-6 -14 0\n"
"-7 16 0\n"
"-15 16 0\n"
"-7 -15 0\n"
"-9 -10 0\n"
"-8 -10 0\n"
"-8 -9 0\n"
"-10 -16 0\n"
"-9 -16 0\n"
"-8 -16 0\n";
const char *unitprop_cnf = "c\n"
"p cnf 6 5\n"
"1 -2 0\n"
"1 -3 0\n"
"2 3 -5 0\n"
"2 3 -4 0\n"
"1 2 3 4 5 6 0\n";
bool
SUBool::TestUnitPropM::TestDimacsHorn() const
{
std::cout << "Testing unit propagation on Horn CNF" << std::endl;
std::stringstream ss;
ss << dimacs_horn;
CNF cnf;
ss >> cnf;
std::cout << "Input: " << std::endl;
std::cout << dimacs_horn << std::endl;
std::cout << "Trying the empty assignment" << std::endl;
PartialAssignment alpha(cnf.MaxVariable());
UnitPropagatorM up(cnf);
auto beta = up.Propagate(alpha);
std::cout << "Consequences: " << beta << std::endl;
return true;
}
bool
SUBool::TestUnitPropM::TestAmoProduct10() const
{
std::cout << "Testing unit propagation on AMO Product with n=10"
<< std::endl;
std::stringstream ss;
ss << amo_product_10;
CNF cnf;
ss >> cnf;
std::cout << "Input: " << std::endl;
std::cout << amo_product_10 << std::endl;
UnitPropagatorM up(cnf);
std::cout << "Trying assignments setting one variable to 1" << std::endl;
for (int i = 1; i <= 10; ++i)
{
PartialAssignment alpha(cnf.MaxVariable());
alpha[i] = PartialValue::TRUE;
auto beta = up.Propagate(alpha);
std::cout << "--" << std::endl;
std::cout << "Assumptions : " << alpha << std::endl;
std::cout << "Consequences: " << beta << std::endl;
PartialAssignment gamma(cnf.MaxVariable(), PartialValue::FALSE);
if (!beta)
{
std::cout << "[FAILED]" << std::endl;
return false;
}
gamma[i] = PartialValue::TRUE;
for (int j = 1; j <= 10; ++j)
{
if ((*beta)[j] != gamma[j])
{
std::cout << "[FAILED]" << std::endl;
return false;
}
}
std::cout << "[PASSED]" << std::endl;
}
std::cout << "Trying assignments setting two variables to 1" << std::endl;
for (int i = 1; i <= 10; ++i)
{
for (int j = 1; j <= 10; ++j)
{
if (j == i)
{
continue;
}
PartialAssignment alpha(cnf.MaxVariable());
alpha[i] = PartialValue::TRUE;
alpha[j] = PartialValue::TRUE;
std::cout << "--" << std::endl;
auto beta = up.Propagate(alpha);
std::cout << "Result: " << beta;
if (beta)
{
std::cout << " [FAILED]" << std::endl;
return false;
}
std::cout << " [PASSED]" << std::endl;
}
}
return true;
}
bool
SUBool::TestUnitPropM::TestUnitPropCNF() const
{
std::cout << "Testing unit propagation on CNF" << std::endl;
std::stringstream ss;
ss << unitprop_cnf;
CNF cnf;
ss >> cnf;
std::cout << "Input: " << std::endl;
std::cout << unitprop_cnf << std::endl;
std::cout << "Trying the assignment with assumptions -1" << std::endl;
PartialAssignment alpha(cnf.MaxVariable());
alpha[1] = PartialValue::FALSE;
// alpha[6] = PartialValue::FALSE;
UnitPropagatorM up(cnf);
auto beta = up.Propagate(alpha);
std::cout << "Consequences: " << beta << std::endl;
if (!beta)
{
std::cout << "[FAILED]" << std::endl;
return false;
}
PartialAssignment gamma(cnf.MaxVariable(), PartialValue::FALSE);
gamma[cnf.MaxVariable()] = PartialValue::TRUE;
std::cout << "Gamma: " << gamma << std::endl;
for (unsigned k = 1; k <= cnf.MaxVariable(); ++k)
{
if ((*beta)[k] != gamma[k])
{
std::cout << (*beta)[k] << "!=" << gamma[k] << " k: " << k
<< std::endl;
std::cout << "[FAILED]" << std::endl;
return false;
}
}
std::cout << "[PASSED]" << std::endl;
return true;
}
bool
SUBool::TestUnitPropM::TestSingleRandomCNF(const CNF &cnf,
const unsigned assump_rounds,
const unsigned assump_size) const
{
UnitPropagator up(&cnf);
UnitPropagatorM up_m(cnf);
for (unsigned round = 0; round < assump_rounds; ++round)
{
auto assump_lits =
random_literal_vector_with_size(assump_size, cnf.MaxVariable());
PartialAssignment alpha(cnf.MaxVariable(), assump_lits);
PartialAssignment clos(0);
auto confl = up.Propagate(alpha, &clos);
auto clos_m = up_m.Propagate(assump_lits);
if ((clos_m && confl >= 0) || (!clos_m && confl < 0))
{
std::cout << "[FAILED] Different results on random CNF" << std::endl;
std::cout << "confl: " << confl << std::endl;
std::cout << "clos_m: " << clos_m << std::endl;
std::cout << "CNF" << std::endl;
std::cout << cnf << std::endl;
std::cout << "c assumptions" << std::endl;
for (const auto &lit : assump_lits)
{
std::cout << lit << " 0" << std::endl;
}
std::cout << "c assumption pa: " << alpha << std::endl;
return false;
}
if (clos_m && *clos_m != clos)
{
std::cout << "[FAILED] Different closures on random CNF" << std::endl;
return false;
}
}
return true;
}
bool
SUBool::TestUnitPropM::TestRandomCNF(const unsigned rounds,
const unsigned n_clauses,
const unsigned n_vars,
const unsigned assump_rounds,
const unsigned assump_size) const
{
std::cout << "Testing propagation on random formulas" << std::endl;
for (unsigned round = 0; round < rounds; ++round)
{
auto cnf = random_cnf(n_clauses, n_vars);
if (!TestSingleRandomCNF(cnf, assump_rounds, assump_size))
{
std::cout << "[FAILED] round " << round << std::endl;
return false;
}
}
std::cout << "[ALL OK]" << std::endl;