This repository has been archived on 2023-08-20. You can view files and clone it, but cannot push or open issues or pull requests.
yap-6.3/packages/bee/cryptominisat-2.5.1/Solver/Subsumer.cpp
Vitor Santos Costa 16015bd8e6 bee
2019-04-22 12:15:21 +01:00

2222 lines
73 KiB
C++
Executable File

/**************************************************************************************************
Originally From: Solver.C -- (C) Niklas Een, Niklas Sorensson, 2004
Substantially modified by: Mate Soos (2010)
**************************************************************************************************/
#include "Solver.h"
#include "Subsumer.h"
#include "ClauseCleaner.h"
#include "time_mem.h"
#include "assert.h"
#include <iomanip>
#include <cmath>
#include <algorithm>
#include "VarReplacer.h"
#include "XorFinder.h"
#ifdef _MSC_VER
#define __builtin_prefetch(a,b,c)
#endif //_MSC_VER
//#define VERBOSE_DEBUG
#ifdef VERBOSE_DEBUG
#define BIT_MORE_VERBOSITY
#endif
//#define BIT_MORE_VERBOSITY
//#define HYPER_DEBUG
//#define HYPER_DEBUG2
//#define TOUCH_LESS
#ifdef VERBOSE_DEBUG
using std::cout;
using std::endl;
#endif //VERBOSE_DEBUG
Subsumer::Subsumer(Solver& s):
solver(s)
, totalTime(0.0)
, numElimed(0)
, numCalls(0)
{
};
Subsumer::~Subsumer()
{
}
void Subsumer::extendModel(Solver& solver2)
{
assert(checkElimedUnassigned());
vec<Lit> tmp;
typedef map<Var, vector<Clause*> > elimType;
for (elimType::iterator it = elimedOutVar.begin(), end = elimedOutVar.end(); it != end; it++) {
#ifndef NDEBUG
Var var = it->first;
#ifdef VERBOSE_DEBUG
std::cout << "Reinserting elimed var: " << var+1 << std::endl;
#endif
assert(!solver.decision_var[var]);
assert(solver.assigns[var] == l_Undef);
assert(!solver.order_heap.inHeap(var));
#endif
for (vector<Clause*>::iterator it2 = it->second.begin(), end2 = it->second.end(); it2 != end2; it2++) {
Clause& c = **it2;
tmp.clear();
tmp.growTo(c.size());
std::copy(c.getData(), c.getDataEnd(), tmp.getData());
#ifdef VERBOSE_DEBUG
std::cout << "Reinserting Clause: ";
c.plainPrint();
#endif
solver2.addClause(tmp);
assert(solver2.ok);
}
}
}
const bool Subsumer::unEliminate(const Var var)
{
assert(var_elimed[var]);
vec<Lit> tmp;
typedef map<Var, vector<Clause*> > elimType;
elimType::iterator it = elimedOutVar.find(var);
//it MUST have been decision var, otherwise we would
//never have removed it
solver.setDecisionVar(var, true);
var_elimed[var] = false;
numElimed--;
//If the variable was removed because of
//pure literal removal (by blocked clause
//elimination, there are no clauses to re-insert
if (it == elimedOutVar.end()) return solver.ok;
FILE* backup_libraryCNFfile = solver.libraryCNFFile;
solver.libraryCNFFile = NULL;
for (vector<Clause*>::iterator it2 = it->second.begin(), end2 = it->second.end(); it2 != end2; it2++) {
solver.addClause(**it2);
clauseFree(*it2);
}
solver.libraryCNFFile = backup_libraryCNFfile;
elimedOutVar.erase(it);
return solver.ok;
}
bool selfSubset(uint32_t A, uint32_t B)
{
uint32_t B_tmp = B | ((B & 0xAAAAAAAALL) >> 1) | ((B & 0x55555555LL) << 1);
if ((A & ~B_tmp) == 0){
uint32_t C = A & ~B;
return (C & (C-1)) == 0;
}else
return false;
}
// Assumes 'seen' is cleared (will leave it cleared)
bool selfSubset(Clause& A, Clause& B, vec<char>& seen)
{
for (uint32_t i = 0; i < B.size(); i++)
seen[B[i].toInt()] = 1;
bool flip = false;
for (uint32_t i = 0; i < A.size(); i++) {
if (!seen[A[i].toInt()]) {
if (flip == true || !seen[(~A[i]).toInt()]) {
for (uint32_t i = 0; i < B.size(); i++) seen[B[i].toInt()] = 0;
return false;
}
flip = true;
}
}
for (uint32_t i = 0; i < B.size(); i++)
seen[B[i].toInt()] = 0;
return flip;
}
template <>
inline uint32_t Subsumer::subsume0(Clause& ps, uint32_t abs)
{
ps.subsume0Finished();
ps.unsetVarChanged();
#ifdef VERBOSE_DEBUG
cout << "subsume0 orig clause: ";
ps.plainPrint();
#endif
return subsume0Orig(ps, abs);
}
template <class T>
inline uint32_t Subsumer::subsume0(T& ps, uint32_t abs)
{
#ifdef VERBOSE_DEBUG
cout << "subsume0 orig vec: ";
ps[0].print(); std::cout << " ";
ps[1].printFull();
#endif
return subsume0Orig(ps, abs);
}
// Will put NULL in 'cs' if clause removed.
template<class T>
uint32_t Subsumer::subsume0Orig(const T& ps, uint32_t abs)
{
uint32_t retIndex = std::numeric_limits<uint32_t>::max();
vec<ClauseSimp> subs;
findSubsumed(ps, abs, subs);
for (uint32_t i = 0; i < subs.size(); i++){
clauses_subsumed++;
#ifdef VERBOSE_DEBUG
cout << "-> subsume0 removing:";
subs[i].clause->plainPrint();
#endif
Clause* tmp = subs[i].clause;
retIndex = subs[i].index;
unlinkClause(subs[i]);
clauseFree(tmp);
}
return retIndex;
}
void Subsumer::subsume0BIN(const Lit lit1, const vec<char>& lits)
{
vec<ClauseSimp> subs;
vec<ClauseSimp> subs2;
vec<Lit> subs2Lit;
vec<ClauseSimp>& cs = occur[lit1.toInt()];
for (ClauseSimp *it = cs.getData(), *end = it + cs.size(); it != end; it++){
if (it+1 != end)
__builtin_prefetch((it+1)->clause, 0, 1);
if (it->clause == NULL) continue;
Clause& c = *it->clause;
bool removed = false;
for (uint32_t i = 0; i < c.size(); i++) {
if (lits[c[i].toInt()]) {
subs.push(*it);
removed = true;
break;
}
}
if (!removed) {
for (uint32_t i = 0; i < c.size(); i++) {
if (lits[(~c[i]).toInt()]) {
subs2.push(*it);
subs2Lit.push(c[i]);
break;
}
}
}
}
for (uint32_t i = 0; i < subs.size(); i++){
clauses_subsumed++;
#ifdef VERBOSE_DEBUG
cout << "-> subsume0 removing:";
subs[i].clause->plainPrint();
#endif
Clause* tmp = subs[i].clause;
unlinkClause(subs[i]);
clauseFree(tmp);
}
if (subs2.size() == 0) return;
registerIteration(subs2);
for (uint32_t j = 0; j < subs2.size(); j++){
if (subs2[j].clause == NULL) continue;
ClauseSimp c = subs2[j];
Clause& cl = *c.clause;
#ifdef VERBOSE_DEBUG
cout << "-> Strenghtening clause :";
cl.plainPrint();
#endif
unlinkClause(c);
literals_removed++;
cl.strengthen(subs2Lit[j]);
Lit *a, *b, *end;
for (a = b = cl.getData(), end = a + cl.size(); a != end; a++) {
lbool val = solver.value(*a);
if (val == l_Undef)
*b++ = *a;
if (val == l_True) {
#ifdef VERBOSE_DEBUG
std::cout << "--> Clause was satisfied." << std::endl;
#endif
clauseFree(&cl);
goto endS;
}
}
cl.shrink(a-b);
cl.setStrenghtened();
#ifdef VERBOSE_DEBUG
cout << "--> Strenghtened clause:";
cl.plainPrint();
#endif
if (cl.size() == 0) {
solver.ok = false;
unregisterIteration(subs2);
clauseFree(&cl);
return;
}
if (cl.size() > 2) {
cl.calcAbstraction();
linkInAlreadyClause(c);
clauses[c.index] = c;
solver.attachClause(cl);
updateClause(c);
} else if (cl.size() == 2) {
cl.calcAbstraction();
solver.attachClause(cl);
solver.becameBinary++;
addBinaryClauses.push(&cl);
//updateClause(c);
} else {
assert(cl.size() == 1);
solver.uncheckedEnqueue(cl[0]);
solver.ok = (solver.propagate() == NULL);
if (!solver.ok) {
unregisterIteration(subs2);
return;
}
#ifdef VERBOSE_DEBUG
cout << "--> Found that var " << cl[0].var()+1 << " must be " << std::boolalpha << !cl[0].sign() << endl;
#endif
clauseFree(&cl);
}
endS:;
}
unregisterIteration(subs2);
}
void Subsumer::unlinkClause(ClauseSimp c, Var elim)
{
Clause& cl = *c.clause;
if (elim != var_Undef) {
assert(!cl.learnt());
#ifdef VERBOSE_DEBUG
std::cout << "Eliminating clause: "; c.clause->plainPrint();
std::cout << "On variable: " << elim+1 << std::endl;
#endif //VERBOSE_DEBUG
elimedOutVar[elim].push_back(c.clause);
}
for (uint32_t i = 0; i < cl.size(); i++) {
maybeRemove(occur[cl[i].toInt()], &cl);
#ifndef TOUCH_LESS
touch(cl[i]);
#endif
}
solver.detachClause(cl);
// Remove from iterator vectors/sets:
for (uint32_t i = 0; i < iter_vecs.size(); i++) {
vec<ClauseSimp>& cs = *iter_vecs[i];
for (uint32_t j = 0; j < cs.size(); j++)
if (cs[j].clause == &cl)
cs[j].clause = NULL;
}
for (uint32_t i = 0; i < iter_sets.size(); i++) {
CSet& cs = *iter_sets[i];
cs.exclude(c);
}
// Remove clause from clause touched set:
cl_touched.exclude(c);
cl_added.exclude(c);
clauses[c.index].clause = NULL;
}
void Subsumer::unlinkModifiedClause(vec<Lit>& origClause, ClauseSimp c)
{
for (uint32_t i = 0; i < origClause.size(); i++) {
maybeRemove(occur[origClause[i].toInt()], c.clause);
#ifndef TOUCH_LESS
touch(origClause[i]);
#endif
}
solver.detachModifiedClause(origClause[0], origClause[1], origClause.size(), c.clause);
// Remove from iterator vectors/sets:
for (uint32_t i = 0; i < iter_vecs.size(); i++){
vec<ClauseSimp>& cs = *iter_vecs[i];
for (uint32_t j = 0; j < cs.size(); j++)
if (cs[j].clause == c.clause)
cs[j].clause = NULL;
}
for (uint32_t i = 0; i < iter_sets.size(); i++){
CSet& cs = *iter_sets[i];
cs.exclude(c);
}
// Remove clause from clause touched set:
cl_touched.exclude(c);
cl_added.exclude(c);
clauses[c.index].clause = NULL;
}
void Subsumer::unlinkModifiedClauseNoDetachNoNULL(vec<Lit>& origClause, ClauseSimp c)
{
for (uint32_t i = 0; i < origClause.size(); i++) {
maybeRemove(occur[origClause[i].toInt()], c.clause);
#ifndef TOUCH_LESS
touch(origClause[i]);
#endif
}
// Remove from iterator vectors/sets:
for (uint32_t i = 0; i < iter_vecs.size(); i++){
vec<ClauseSimp>& cs = *iter_vecs[i];
for (uint32_t j = 0; j < cs.size(); j++)
if (cs[j].clause == c.clause)
cs[j].clause = NULL;
}
for (uint32_t i = 0; i < iter_sets.size(); i++){
CSet& cs = *iter_sets[i];
cs.exclude(c);
}
// Remove clause from clause touched set:
cl_touched.exclude(c);
cl_added.exclude(c);
}
void Subsumer::subsume1(ClauseSimp& ps)
{
vec<ClauseSimp> Q;
vec<ClauseSimp> subs;
vec<Lit> qs;
uint32_t q;
ps.clause->unsetStrenghtened();
registerIteration(Q);
registerIteration(subs);
Q.push(ps);
q = 0;
while (q < Q.size()){
if (Q[q].clause == NULL) { q++; continue; }
#ifdef VERBOSE_DEBUG
cout << "subsume1 with clause:";
Q[q].clause->plainPrint();
#endif
qs.clear();
for (uint32_t i = 0; i < Q[q].clause->size(); i++)
qs.push((*Q[q].clause)[i]);
for (uint32_t i = 0; i < qs.size(); i++){
qs[i] = ~qs[i];
uint32_t abst = calcAbstraction(qs);
findSubsumed(qs, abst, subs);
for (uint32_t j = 0; j < subs.size(); j++){
/*#ifndef NDEBUG
if (&counter != NULL && counter == -1){
dump(*subs[j].clause);
qs[i] = ~qs[i];
dump(qs);
printf(L_LIT"\n", L_lit(qs[i]));
exit(0);
}
#endif*/
if (subs[j].clause == NULL) continue;
ClauseSimp c = subs[j];
Clause& cl = *c.clause;
#ifdef VERBOSE_DEBUG
cout << "-> Strenghtening clause :";
cl.plainPrint();
#endif
unlinkClause(c);
literals_removed++;
cl.strengthen(qs[i]);
Lit *a, *b, *end;
for (a = b = cl.getData(), end = a + cl.size(); a != end; a++) {
lbool val = solver.value(*a);
if (val == l_Undef)
*b++ = *a;
if (val == l_True) {
#ifdef VERBOSE_DEBUG
std::cout << "--> Clause was satisfied." << std::endl;
#endif
clauseFree(&cl);
goto endS;
}
}
cl.shrink(a-b);
cl.setStrenghtened();
#ifdef VERBOSE_DEBUG
cout << "--> Strenghtened clause:";
cl.plainPrint();
#endif
if (cl.size() == 0) {
solver.ok = false;
unregisterIteration(Q);
unregisterIteration(subs);
clauseFree(&cl);
return;
}
if (cl.size() > 1) {
cl.calcAbstraction();
linkInAlreadyClause(c);
clauses[c.index] = c;
solver.attachClause(cl);
if (cl.size() == 2) solver.becameBinary++;
updateClause(c);
Q.push(c);
} else {
assert(cl.size() == 1);
solver.uncheckedEnqueue(cl[0]);
solver.ok = (solver.propagate() == NULL);
if (!solver.ok) {
unregisterIteration(Q);
unregisterIteration(subs);
return;
}
#ifdef VERBOSE_DEBUG
cout << "--> Found that var " << cl[0].var()+1 << " must be " << std::boolalpha << !cl[0].sign() << endl;
#endif
clauseFree(&cl);
}
endS:;
}
qs[i] = ~qs[i];
subs.clear();
}
q++;
}
unregisterIteration(Q);
unregisterIteration(subs);
}
template<class T>
void Subsumer::subsume1Partial(const T& ps)
{
assert(solver.decisionLevel() == 0);
registerIteration(subsume1PartialSubs);
#ifdef VERBOSE_DEBUG
cout << "-> Strenghtening using clause :";
ps[0].print(); std::cout << " ";
ps[1].printFull();
#endif
assert(ps.size() == 2);
subsume1PartialQs.clear();
for (uint8_t i = 0; i < 2; i++)
subsume1PartialQs.push(ps[i]);
for (uint8_t i = 0; i < 2; i++){
subsume1PartialQs[i] = ~subsume1PartialQs[i];
uint32_t abst = calcAbstraction(subsume1PartialQs);
findSubsumed(subsume1PartialQs, abst, subsume1PartialSubs);
for (uint32_t j = 0; j < subsume1PartialSubs.size(); j++){
if (subsume1PartialSubs[j].clause == NULL) continue;
ClauseSimp c = subsume1PartialSubs[j];
Clause& cl = *c.clause;
#ifdef VERBOSE_DEBUG
cout << "-> Strenghtening clause :";
cl.plainPrint();
#endif
unlinkClause(subsume1PartialSubs[j]);
literals_removed++;
cl.strengthen(subsume1PartialQs[i]);
Lit *a, *b, *end;
for (a = b = cl.getData(), end = a + cl.size(); a != end; a++) {
lbool val = solver.value(*a);
if (val == l_Undef)
*b++ = *a;
if (val == l_True) {
#ifdef VERBOSE_DEBUG
std::cout << "--> Clause was satisfied." << std::endl;
#endif
clauseFree(&cl);
goto endS;
}
}
cl.shrink(a-b);
cl.setStrenghtened();
#ifdef VERBOSE_DEBUG
cout << "--> Strenghtened clause:";
cl.plainPrint();
#endif
if (cl.size() == 0) {
solver.ok = false;
unregisterIteration(subsume1PartialSubs);
clauseFree(&cl);
return;
}
if (cl.size() > 2) {
cl.calcAbstraction();
linkInAlreadyClause(c);
clauses[c.index] = c;
solver.attachClause(cl);
updateClause(c);
} else if (cl.size() == 2) {
cl.calcAbstraction();
solver.attachClause(cl);
solver.becameBinary++;
addBinaryClauses.push(&cl);
//updateClause(c);
} else {
assert(cl.size() == 1);
solver.uncheckedEnqueue(cl[0]);
solver.ok = (solver.propagate() == NULL);
if (!solver.ok) {
unregisterIteration(subsume1PartialSubs);
return;
}
#ifdef VERBOSE_DEBUG
cout << "--> Found that var " << cl[0].var()+1 << " must be " << std::boolalpha << !cl[0].sign() << endl;
#endif
clauseFree(&cl);
}
endS:;
}
subsume1PartialQs[i] = ~subsume1PartialQs[i];
subsume1PartialSubs.clear();
}
unregisterIteration(subsume1PartialSubs);
}
void Subsumer::updateClause(ClauseSimp c)
{
if (!c.clause->learnt()) subsume0(*c.clause, c.clause->getAbst());
cl_touched.add(c);
}
void Subsumer::almost_all_database()
{
#ifdef BIT_MORE_VERBOSITY
std::cout << "c Larger database" << std::endl;
#endif
// Optimized variant when virtually whole database is involved:
cl_added .clear();
cl_touched.clear();
for (uint32_t i = 0; i < clauses.size(); i++) {
if (numMaxSubsume1 == 0) break;
if (clauses[i].clause != NULL) {
subsume1(clauses[i]);
numMaxSubsume1--;
if (!solver.ok) return;
}
}
assert(solver.ok);
solver.ok = (solver.propagate() == NULL);
if (!solver.ok) {
std::cout << "c (contradiction during subsumption)" << std::endl;
return;
}
solver.clauseCleaner->cleanClausesBewareNULL(clauses, ClauseCleaner::simpClauses, *this);
#ifdef VERBOSE_DEBUG
cout << "subsume1 part 1 finished" << endl;
#endif
CSet s1;
registerIteration(s1);
while (cl_touched.size() > 0 && numMaxSubsume1 > 0){
#ifdef VERBOSE_DEBUG
std::cout << "c cl_touched was > 0, new iteration" << std::endl;
#endif
for (CSet::iterator it = cl_touched.begin(), end = cl_touched.end(); it != end; ++it) {
if (it->clause != NULL)
s1.add(*it);
}
cl_touched.clear();
for (CSet::iterator it = s1.begin(), end = s1.end(); it != end; ++it) {
if (numMaxSubsume1 == 0) break;
if (it->clause != NULL) {
subsume1(*it);
numMaxSubsume1--;
if (!solver.ok) return;
}
}
s1.clear();
if (!solver.ok) return;
solver.ok = (solver.propagate() == NULL);
if (!solver.ok) {
printf("c (contradiction during subsumption)\n");
unregisterIteration(s1);
return;
}
solver.clauseCleaner->cleanClausesBewareNULL(clauses, ClauseCleaner::simpClauses, *this);
}
unregisterIteration(s1);
}
void Subsumer::smaller_database()
{
#ifdef BIT_MORE_VERBOSITY
std::cout << "c Smaller database" << std::endl;
#endif
// Set used in 1-subs:
// (1) clauses containing a negated literal of an added clause.
// (2) all added or strengthened ("touched") clauses.
//
// Set used in 0-subs:
// (1) clauses containing a (non-negated) literal of an added clause, including the added clause itself.
// (2) all strenghtened clauses -- REMOVED!! We turned on eager backward subsumption which supersedes this.
#ifdef BIT_MORE_VERBOSITY
printf(" PREPARING\n");
#endif
CSet s0, s1; // 's0' is used for 0-subsumption, 's1' for 1-subsumption
vec<char> ol_seen(solver.nVars()*2, 0);
for (CSet::iterator it = cl_added.begin(), end = cl_added.end(); it != end; ++it) {
if (it->clause == NULL) continue;
ClauseSimp& c = *it;
Clause& cl = *it->clause;
s1.add(c);
for (uint32_t j = 0; j < cl.size(); j++){
if (ol_seen[cl[j].toInt()]) continue;
ol_seen[cl[j].toInt()] = 1;
vec<ClauseSimp>& n_occs = occur[(~cl[j]).toInt()];
for (uint32_t k = 0; k < n_occs.size(); k++)
if (n_occs[k].clause != c.clause && n_occs[k].clause->size() <= cl.size() && selfSubset(n_occs[k].clause->getAbst(), c.clause->getAbst()) && selfSubset(*n_occs[k].clause, cl, seen_tmp))
s1.add(n_occs[k]);
vec<ClauseSimp>& p_occs = occur[cl[j].toInt()];
for (uint32_t k = 0; k < p_occs.size(); k++)
if (subsetAbst(p_occs[k].clause->getAbst(), c.clause->getAbst()))
s0.add(p_occs[k]);
}
}
cl_added.clear();
registerIteration(s0);
registerIteration(s1);
#ifdef BIT_MORE_VERBOSITY
printf("c FIXED-POINT\n");
#endif
// Fixed-point for 1-subsumption:
while (s1.size() > 0 || cl_touched.size() > 0){
for (CSet::iterator it = cl_touched.begin(), end = cl_touched.end(); it != end; ++it) {
if (it->clause != NULL) {
s1.add(*it);
s0.add(*it);
}
}
cl_touched.clear();
assert(solver.qhead == solver.trail.size());
#ifdef BIT_MORE_VERBOSITY
printf("c s1.size()=%d cl_touched.size()=%d\n", s1.size(), cl_touched.size());
#endif
for (CSet::iterator it = s1.begin(), end = s1.end(); it != end; ++it) {
if (numMaxSubsume1 == 0) break;
if (it->clause != NULL) {
subsume1(*it);
numMaxSubsume1--;
if (!solver.ok) return;
}
}
s1.clear();
if (!solver.ok) return;
solver.ok = (solver.propagate() == NULL);
if (!solver.ok){
printf("c (contradiction during subsumption)\n");
unregisterIteration(s1);
unregisterIteration(s0);
return;
}
solver.clauseCleaner->cleanClausesBewareNULL(clauses, ClauseCleaner::simpClauses, *this);
}
unregisterIteration(s1);
// Iteration pass for 0-subsumption:
for (CSet::iterator it = s0.begin(), end = s0.end(); it != end; ++it) {
if (it->clause != NULL)
subsume0(*it->clause, it->clause->getAbst());
}
s0.clear();
unregisterIteration(s0);
}
ClauseSimp Subsumer::linkInClause(Clause& cl)
{
ClauseSimp c(&cl, clauseID++);
clauses.push(c);
for (uint32_t i = 0; i < cl.size(); i++) {
occur[cl[i].toInt()].push(c);
touch(cl[i].var());
}
cl_added.add(c);
return c;
}
void Subsumer::linkInAlreadyClause(ClauseSimp& c)
{
Clause& cl = *c.clause;
for (uint32_t i = 0; i < cl.size(); i++) {
occur[cl[i].toInt()].push(c);
touch(cl[i].var());
}
}
template<bool UseCL>
void Subsumer::addFromSolver(vec<Clause*>& cs, bool alsoLearnt)
{
Clause **i = cs.getData();
Clause **j = i;
for (Clause **end = i + cs.size(); i != end; i++) {
if (i+1 != end)
__builtin_prefetch(*(i+1), 1, 1);
if (!alsoLearnt && (*i)->learnt()) {
*j++ = *i;
(*i)->setUnsorted();
continue;
}
if (!UseCL && (*i)->size() == 2) {
//don't add binary clauses in this case
*j++ = *i;
(*i)->setUnsorted();
continue;
}
ClauseSimp c(*i, clauseID++);
clauses.push(c);
Clause& cl = *c.clause;
for (uint32_t i = 0; i < cl.size(); i++) {
occur[cl[i].toInt()].push(c);
touch(cl[i].var());
}
if (UseCL) {
if (fullSubsume || cl.getVarChanged()) cl_added.add(c);
else if (cl.getStrenghtened()) cl_touched.add(c);
}
if (cl.getVarChanged() || cl.getStrenghtened())
cl.calcAbstraction();
}
cs.shrink(i-j);
}
void Subsumer::addBackToSolver()
{
#ifdef HYPER_DEBUG2
uint32_t binaryLearntAdded = 0;
#endif
for (uint32_t i = 0; i < clauses.size(); i++) {
if (clauses[i].clause != NULL) {
assert(clauses[i].clause->size() > 1);
if (clauses[i].clause->size() == 2) {
#ifdef HYPER_DEBUG2
if (clauses[i].clause->learnt())
binaryLearntAdded++;
#endif
solver.binaryClauses.push(clauses[i].clause);
} else {
if (clauses[i].clause->learnt())
solver.learnts.push(clauses[i].clause);
else
solver.clauses.push(clauses[i].clause);
}
}
}
#ifdef HYPER_DEBUG2
std::cout << "Binary learnt added:" << binaryLearntAdded << std::endl;
#endif
}
void Subsumer::removeWrong(vec<Clause*>& cs)
{
Clause **i = cs.getData();
Clause **j = i;
for (Clause **end = i + cs.size(); i != end; i++) {
Clause& c = **i;
if (!c.learnt()) {
*j++ = *i;
continue;
}
bool remove = false;
for (Lit *l = c.getData(), *end2 = l+c.size(); l != end2; l++) {
if (var_elimed[l->var()]) {
remove = true;
solver.detachClause(c);
clauseFree(&c);
break;
}
}
if (!remove)
*j++ = *i;
}
cs.shrink(i-j);
}
void Subsumer::fillCannotEliminate()
{
std::fill(cannot_eliminate.getData(), cannot_eliminate.getDataEnd(), false);
for (uint32_t i = 0; i < solver.xorclauses.size(); i++) {
const XorClause& c = *solver.xorclauses[i];
for (uint32_t i2 = 0; i2 < c.size(); i2++)
cannot_eliminate[c[i2].var()] = true;
}
const vec<Clause*>& tmp = solver.varReplacer->getClauses();
for (uint32_t i = 0; i < tmp.size(); i++) {
const Clause& c = *tmp[i];
for (uint32_t i2 = 0; i2 < c.size(); i2++)
cannot_eliminate[c[i2].var()] = true;
}
for (uint32_t i = 0; i < solver.assumptions.size(); i++)
cannot_eliminate[solver.assumptions[i].var()] = true;
#ifdef VERBOSE_DEBUG
uint32_t tmpNum = 0;
for (uint32_t i = 0; i < cannot_eliminate.size(); i++)
if (cannot_eliminate[i])
tmpNum++;
std::cout << "Cannot eliminate num:" << tmpNum << std::endl;
#endif
}
void Subsumer::subsume0LearntSet(vec<Clause*>& cs)
{
Clause** a = cs.getData();
Clause** b = a;
for (Clause** end = a + cs.size(); a != end; a++) {
if (numMaxSubsume0 > 0 && !(*a)->subsume0IsFinished()) {
numMaxSubsume0--;
uint32_t index = subsume0(**a, calcAbstraction(**a));
if (index != std::numeric_limits<uint32_t>::max()) {
(*a)->makeNonLearnt();
//solver.nbBin--;
clauses[index].clause = *a;
linkInAlreadyClause(clauses[index]);
solver.learnts_literals -= (*a)->size();
solver.clauses_literals += (*a)->size();
cl_added.add(clauses[index]);
continue;
}
if (numMaxSubsume1 > 0 &&
(((*a)->size() == 2 && clauses.size() < 3500000) ||
((*a)->size() <= 3 && clauses.size() < 300000) ||
((*a)->size() <= 4 && clauses.size() < 60000))) {
ClauseSimp c(*a, clauseID++);
//(*a)->calcAbstraction();
//clauses.push(c);
subsume1(c);
numMaxSubsume1--;
if (!solver.ok) {
for (; a != end; a++)
*b++ = *a;
cs.shrink(a-b);
return;
}
//assert(clauses[c.index].clause != NULL);
//clauses.pop();
clauseID--;
}
}
*b++ = *a;
}
cs.shrink(a-b);
}
const bool Subsumer::treatLearnts()
{
subsume0LearntSet(solver.learnts);
if (!solver.ok) return false;
subsume0LearntSet(solver.binaryClauses);
if (!solver.ok) return false;
solver.ok = (solver.propagate() == NULL);
if (!solver.ok){
printf("c (contradiction during subsumption)\n");
return false;
}
solver.clauseCleaner->cleanClausesBewareNULL(clauses, ClauseCleaner::simpClauses, *this);
return true;
}
const bool Subsumer::subsumeWithBinaries(const bool startUp)
{
clearAll();
clauseID = 0;
fullSubsume = true;
addBinaryClauses.clear();
//Clearing stats
subsNonExistentumFailed = 0;
clauses_subsumed = 0;
literals_removed = 0;
double myTime = cpuTime();
uint32_t origTrailSize = solver.trail.size();
clauses.reserve(solver.clauses.size());
solver.clauseCleaner->cleanClauses(solver.clauses, ClauseCleaner::clauses);
addFromSolver<false>(solver.clauses);
#ifdef DEBUG_BINARIES
for (uint32_t i = 0; i < clauses.size(); i++) {
assert(clauses[i].clause->size() != 2);
}
#endif //DEBUG_BINARIES
for (uint32_t i = 0; i < solver.binaryClauses.size(); i++) {
if (startUp || !solver.binaryClauses[i]->learnt()) {
Clause& c = *solver.binaryClauses[i];
subsume0(c, c.getAbst());
}
}
for (uint32_t i = 0; i < solver.binaryClauses.size(); i++) {
Clause& c = *solver.binaryClauses[i];
subsume1Partial(c);
if (!solver.ok) return false;
}
if (solver.verbosity >= 1) {
std::cout << "c subs with bin: " << std::setw(8) << clauses_subsumed
<< " lits-rem: " << std::setw(9) << literals_removed
<< " v-fix: " << std::setw(4) <<solver.trail.size() - origTrailSize
<< " time: " << std::setprecision(2) << std::setw(5) << cpuTime() - myTime << " s"
<< std::setw(17) << " |" << std::endl;
}
if (!subsWNonExistBinsFull(startUp)) return false;
#ifdef DEBUG_BINARIES
for (uint32_t i = 0; i < clauses.size(); i++) {
assert(clauses[i].clause == NULL || clauses[i].clause->size() != 2);
}
#endif //DEBUG_BINARIES
addBackToSolver();
for (uint32_t i = 0; i < addBinaryClauses.size(); i++) {
solver.binaryClauses.push(addBinaryClauses[i]);
}
addBinaryClauses.clear();
if (solver.verbosity >= 1) {
std::cout << "c Subs w/ non-existent bins: " << std::setw(6) << subsNonExistentNum
<< " l-rem: " << std::setw(6) << subsNonExistentLitsRemoved
<< " v-fix: " << std::setw(5) << subsNonExistentumFailed
<< " done: " << std::setw(6) << doneNum
<< " time: " << std::fixed << std::setprecision(2) << std::setw(5) << subsNonExistentTime << " s"
<< std::setw(2) << " |" << std::endl;
}
totalTime += cpuTime() - myTime;
solver.order_heap.filter(Solver::VarFilter(solver));
return true;
}
#define MAX_BINARY_PROP 40000000
const bool Subsumer::subsWNonExistBinsFull(const bool startUp)
{
uint32_t oldClausesSubusmed = clauses_subsumed;
uint32_t oldLitsRemoved = literals_removed;
double myTime = cpuTime();
uint64_t oldProps = solver.propagations;
uint32_t oldTrailSize = solver.trail.size();
uint64_t maxProp = MAX_BINARY_PROP;
if (!startUp) maxProp /= 3;
ps2.clear();
ps2.growTo(2);
toVisitAll.growTo(solver.nVars()*2, false);
doneNum = 0;
uint32_t startFrom = solver.mtrand.randInt(solver.order_heap.size());
for (uint32_t i = 0; i < solver.order_heap.size(); i++) {
Var var = solver.order_heap[(i+startFrom)%solver.order_heap.size()];
if (solver.propagations - oldProps > maxProp) break;
if (solver.assigns[var] != l_Undef || !solver.decision_var[var]) continue;
doneNum++;
Lit lit(var, true);
if (!subsWNonExistBins(lit, startUp)) {
if (!solver.ok) return false;
solver.cancelUntil(0);
solver.uncheckedEnqueue(~lit);
solver.ok = (solver.propagate() == NULL);
if (!solver.ok) return false;
continue;
}
//in the meantime it could have got assigned
if (solver.assigns[var] != l_Undef) continue;
lit = ~lit;
if (!subsWNonExistBins(lit, startUp)) {
if (!solver.ok) return false;
solver.cancelUntil(0);
solver.uncheckedEnqueue(~lit);
solver.ok = (solver.propagate() == NULL);
if (!solver.ok) return false;
continue;
}
}
subsNonExistentNum = clauses_subsumed - oldClausesSubusmed;
subsNonExistentTime = cpuTime() - myTime;
subsNonExistentumFailed = solver.trail.size() - oldTrailSize;
subsNonExistentLitsRemoved = literals_removed - oldLitsRemoved;
return true;
}
const bool Subsumer::subsWNonExistBins(const Lit& lit, const bool startUp)
{
#ifdef VERBOSE_DEBUG
std::cout << "subsWNonExistBins called with lit "; lit.print();
std::cout << " startUp: " << startUp << std::endl;
#endif //VERBOSE_DEBUG
toVisit.clear();
solver.newDecisionLevel();
solver.uncheckedEnqueueLight(lit);
bool failed;
if (startUp) {
failed = (solver.propagateBin() != NULL);
} else {
failed = (solver.propagateBinNoLearnts() != NULL);
}
if (failed) return false;
assert(solver.decisionLevel() > 0);
for (int c = solver.trail.size()-1; c > (int)solver.trail_lim[0]; c--) {
Lit x = solver.trail[c];
toVisit.push(x);
toVisitAll[x.toInt()] = true;
}
solver.cancelUntil(0);
if (toVisit.size() <= 1) {
ps2[0] = ~lit;
for (Lit *l = toVisit.getData(), *end = toVisit.getDataEnd(); l != end; l++) {
ps2[1] = *l;
assert(ps2[0] != ps2[1]);
#ifdef VERBOSE_DEBUG
std::cout << "Non-existent bin. lit1: "; ps2[0].print();
std::cout << " lit2: "; ps2[1].print(); std::cout << std::endl;
#endif //VERBOSE_DEBUG
subsume0(ps2, calcAbstraction(ps2));
subsume1Partial(ps2);
}
} else {
subsume0BIN(~lit, toVisitAll);
}
for (uint32_t i = 0; i < toVisit.size(); i++)
toVisitAll[toVisit[i].toInt()] = false;
return solver.ok;
}
void Subsumer::clearAll()
{
touched_list.clear();
touched.clear();
touched.growTo(solver.nVars(), false);
for (Var var = 0; var < solver.nVars(); var++) {
if (solver.decision_var[var] && solver.assigns[var] == l_Undef) touch(var);
occur[2*var].clear();
occur[2*var+1].clear();
}
clauses.clear();
cl_added.clear();
cl_touched.clear();
}
const bool Subsumer::simplifyBySubsumption()
{
if (solver.nClauses() > 20000000) return true;
double myTime = cpuTime();
uint32_t origTrailSize = solver.trail.size();
clauses_subsumed = 0;
literals_removed = 0;
numblockedClauseRemoved = 0;
numCalls++;
clauseID = 0;
numVarsElimed = 0;
blockTime = 0.0;
clearAll();
//if (solver.xorclauses.size() < 30000 && solver.clauses.size() < MAX_CLAUSENUM_XORFIND/10) addAllXorAsNorm();
solver.testAllClauseAttach();
if (solver.performReplace && !solver.varReplacer->performReplace(true))
return false;
fillCannotEliminate();
solver.testAllClauseAttach();
clauses.reserve(solver.clauses.size() + solver.binaryClauses.size());
cl_added.reserve(solver.clauses.size() + solver.binaryClauses.size());
cl_touched.reserve(solver.clauses.size() + solver.binaryClauses.size());
if (clauses.size() < 200000)
fullSubsume = true;
else
fullSubsume = false;
solver.clauseCleaner->cleanClauses(solver.clauses, ClauseCleaner::clauses);
addFromSolver<true>(solver.clauses);
solver.clauseCleaner->removeSatisfied(solver.binaryClauses, ClauseCleaner::binaryClauses);
addFromSolver<true>(solver.binaryClauses);
//Limits
if (clauses.size() > 3500000) {
numMaxSubsume0 = 900000 * (1+numCalls/2);
numMaxElim = (uint32_t)((double)solver.order_heap.size() / 5.0 * (0.8+(double)(numCalls)/4.0));
numMaxSubsume1 = 100000 * (1+numCalls/2);
numMaxBlockToVisit = (int64_t)(30000.0 * (0.8+(double)(numCalls)/3.0));
}
if (clauses.size() <= 3500000 && clauses.size() > 1500000) {
numMaxSubsume0 = 2000000 * (1+numCalls/2);
numMaxElim = (uint32_t)((double)solver.order_heap.size() / 2.0 * (0.8+(double)(numCalls)/4.0));
numMaxSubsume1 = 300000 * (1+numCalls/2);
numMaxBlockToVisit = (int64_t)(50000.0 * (0.8+(double)(numCalls)/3.0));
}
if (clauses.size() <= 1500000) {
numMaxSubsume0 = 4000000 * (1+numCalls/2);
numMaxElim = (uint32_t)((double)solver.order_heap.size() / 2.0 * (0.8+(double)(numCalls)/2.0));
numMaxSubsume1 = 400000 * (1+numCalls/2);
numMaxBlockToVisit = (int64_t)(80000.0 * (0.8+(double)(numCalls)/3.0));
}
if (numCalls == 1) numMaxSubsume1 = 0;
if (!solver.doSubsume1) numMaxSubsume1 = 0;
if (solver.order_heap.size() > 200000)
numMaxBlockVars = (uint32_t)((double)solver.order_heap.size() / 3.5 * (0.8+(double)(numCalls)/4.0));
else
numMaxBlockVars = (uint32_t)((double)solver.order_heap.size() / 1.5 * (0.8+(double)(numCalls)/4.0));
//For debugging
//numMaxBlockToVisit = std::numeric_limits<int64_t>::max();
//numMaxElim = std::numeric_limits<uint32_t>::max();
//numMaxSubsume0 = std::numeric_limits<uint32_t>::max();
//numMaxSubsume1 = std::numeric_limits<uint32_t>::max();
//numMaxBlockVars = std::numeric_limits<uint32_t>::max();
#ifdef BIT_MORE_VERBOSITY
std::cout << "c num clauses:" << clauses.size() << std::endl;
std::cout << "c time to link in:" << cpuTime()-myTime << std::endl;
#endif
for (uint32_t i = 0; i < clauses.size(); i++) {
if (numMaxSubsume0 == 0) break;
if (clauses[i].clause != NULL &&
(fullSubsume
|| !clauses[i].clause->subsume0IsFinished())
) {
subsume0(*clauses[i].clause, clauses[i].clause->getAbst());
numMaxSubsume0--;
}
}
origNClauses = clauses.size();
uint32_t origNLearnts = solver.learnts.size();
if (!treatLearnts()) return false;
#ifdef BIT_MORE_VERBOSITY
std::cout << "c time until pre-subsume0 clauses and subsume1 2-learnts:" << cpuTime()-myTime << std::endl;
#endif
if (!solver.ok) return false;
#ifdef VERBOSE_DEBUG
std::cout << "c pre-subsumed:" << clauses_subsumed << std::endl;
std::cout << "c cl_added:" << cl_added.size() << std::endl;
std::cout << "c cl_touched:" << cl_touched.size() << std::endl;
std::cout << "c clauses:" << clauses.size() << std::endl;
std::cout << "c origNClauses:" << origNClauses << std::endl;
#endif
if (clauses.size() > 10000000) goto endSimplifyBySubsumption;
if (solver.doBlockedClause && numCalls % 3 == 1) blockedClauseRemoval();
do{
#ifdef BIT_MORE_VERBOSITY
std::cout << "c time before the start of almost_all/smaller: " << cpuTime() - myTime << std::endl;
#endif
if (numMaxSubsume0 > 0) {
if (cl_added.size() > origNClauses / 2) {
almost_all_database();
if (!solver.ok) return false;
} else {
smaller_database();
if (!solver.ok) return false;
}
}
cl_added.clear();
assert(cl_added.size() == 0);
assert(solver.ok);
solver.ok = (solver.propagate() == NULL);
if (!solver.ok) {
printf("c (contradiction during subsumption)\n");
return false;
}
solver.clauseCleaner->cleanClausesBewareNULL(clauses, ClauseCleaner::simpClauses, *this);
#ifdef BIT_MORE_VERBOSITY
std::cout << "c time until the end of almost_all/smaller: " << cpuTime() - myTime << std::endl;
#endif
if (!solver.doVarElim) break;
#ifdef BIT_MORE_VERBOSITY
printf("c VARIABLE ELIMINIATION\n");
std::cout << "c toucheds list size:" << touched_list.size() << std::endl;
#endif
vec<Var> init_order;
orderVarsForElim(init_order); // (will untouch all variables)
for (bool first = true; numMaxElim > 0; first = false){
uint32_t vars_elimed = 0;
vec<Var> order;
if (first) {
//init_order.copyTo(order);
for (uint32_t i = 0; i < init_order.size(); i++) {
const Var var = init_order[i];
if (!cannot_eliminate[var] && solver.decision_var[var])
order.push(var);
}
} else {
for (uint32_t i = 0; i < touched_list.size(); i++) {
const Var var = touched_list[i];
if (!cannot_eliminate[var] && solver.decision_var[var])
order.push(var);
touched[var] = false;
}
touched_list.clear();
}
#ifdef VERBOSE_DEBUG
std::cout << "Order size:" << order.size() << std::endl;
#endif
assert(solver.qhead == solver.trail.size());
for (uint32_t i = 0; i < order.size() && numMaxElim > 0; i++, numMaxElim--) {
if (maybeEliminate(order[i])) {
if (!solver.ok) {
printf("c (contradiction during subsumption)\n");
return false;
}
vars_elimed++;
}
}
assert(solver.qhead == solver.trail.size());
if (vars_elimed == 0) break;
numVarsElimed += vars_elimed;
#ifdef BIT_MORE_VERBOSITY
printf("c #var-elim: %d\n", vars_elimed);
std::cout << "c time until the end of varelim: " << cpuTime() - myTime << std::endl;
#endif
}
}while (cl_added.size() > 100 && numMaxElim > 0);
endSimplifyBySubsumption:
if (!solver.ok) return false;
solver.ok = (solver.propagate() == NULL);
if (!solver.ok) {
printf("c (contradiction during subsumption)\n");
return false;
}
#ifndef NDEBUG
verifyIntegrity();
#endif
//vector<char> var_merged = merge();
removeWrong(solver.learnts);
removeWrong(solver.binaryClauses);
removeAssignedVarsFromEliminated();
/*solver.clauseCleaner->cleanClausesBewareNULL(clauses, ClauseCleaner::simpClauses, *this);
addFromSolver(solver.learnts, true);
addFromSolver(solver.binaryClauses, true);
if (solver.doHyperBinRes && clauses.size() < 1000000 && numCalls > 1 && !hyperBinRes())
return false;*/
solver.order_heap.filter(Solver::VarFilter(solver));
addBackToSolver();
solver.nbCompensateSubsumer += origNLearnts-solver.learnts.size();
if (solver.verbosity >= 1) {
std::cout << "c | lits-rem: " << std::setw(9) << literals_removed
<< " cl-subs: " << std::setw(8) << clauses_subsumed
<< " v-elim: " << std::setw(6) << numVarsElimed
<< " v-fix: " << std::setw(4) <<solver.trail.size() - origTrailSize
<< " time: " << std::setprecision(2) << std::setw(5) << (cpuTime() - myTime) << " s"
//<< " blkClRem: " << std::setw(5) << numblockedClauseRemoved
<< " |" << std::endl;
if (numblockedClauseRemoved > 0 || blockTime > 0.0) {
std::cout
<< "c | Blocked clauses removed: " << std::setw(8) << numblockedClauseRemoved
<< " Time: " << std::fixed << std::setprecision(2) << std::setw(4) << blockTime << " s"
<< " |" << std::endl;
}
}
totalTime += cpuTime() - myTime;
solver.testAllClauseAttach();
return true;
}
void Subsumer::removeAssignedVarsFromEliminated()
{
for (Var var = 0; var < var_elimed.size(); var++) {
if (var_elimed[var] && solver.assigns[var] != l_Undef) {
var_elimed[var] = false;
solver.setDecisionVar(var, true);
numElimed--;
map<Var, vector<Clause*> >::iterator it = elimedOutVar.find(var);
if (it != elimedOutVar.end()) {
//TODO memory loss here
elimedOutVar.erase(it);
}
}
}
}
template<class T>
void Subsumer::findSubsumed(const T& ps, uint32_t abs, vec<ClauseSimp>& out_subsumed)
{
#ifdef VERBOSE_DEBUG
cout << "findSubsumed: ";
for (uint32_t i = 0; i < ps.size(); i++) {
if (ps[i].sign()) printf("-");
printf("%d ", ps[i].var() + 1);
}
printf("0\n");
#endif
uint32_t min_i = 0;
for (uint32_t i = 1; i < ps.size(); i++){
if (occur[ps[i].toInt()].size() < occur[ps[min_i].toInt()].size())
min_i = i;
}
vec<ClauseSimp>& cs = occur[ps[min_i].toInt()];
for (ClauseSimp *it = cs.getData(), *end = it + cs.size(); it != end; it++){
if (it+1 != end)
__builtin_prefetch((it+1)->clause, 1, 1);
if (it->clause != (Clause*)&ps && subsetAbst(abs, it->clause->getAbst()) && ps.size() <= it->clause->size() && subset(ps, *it->clause)) {
out_subsumed.push(*it);
#ifdef VERBOSE_DEBUG
cout << "subsumed: ";
it->clause->plainPrint();
#endif
}
}
}
void inline Subsumer::MigrateToPsNs(vec<ClauseSimp>& poss, vec<ClauseSimp>& negs, vec<ClauseSimp>& ps, vec<ClauseSimp>& ns, const Var x)
{
poss.moveTo(ps);
negs.moveTo(ns);
for (uint32_t i = 0; i < ps.size(); i++)
unlinkClause(ps[i], x);
for (uint32_t i = 0; i < ns.size(); i++)
unlinkClause(ns[i], x);
}
void inline Subsumer::DeallocPsNs(vec<ClauseSimp>& ps, vec<ClauseSimp>& ns)
{
for (uint32_t i = 0; i < ps.size(); i++) {
//clauses[ps[i].index].clause = NULL;
//clauseFree(ps[i].clause);
}
for (uint32_t i = 0; i < ns.size(); i++) {
//clauses[ns[i].index].clause = NULL;
//clauseFree(ns[i].clause);
}
}
// Returns TRUE if variable was eliminated.
bool Subsumer::maybeEliminate(const Var x)
{
assert(solver.qhead == solver.trail.size());
assert(!var_elimed[x]);
assert(!cannot_eliminate[x]);
assert(solver.decision_var[x]);
if (solver.value(x) != l_Undef) return false;
if (occur[Lit(x, false).toInt()].size() == 0 && occur[Lit(x, true).toInt()].size() == 0)
return false;
vec<ClauseSimp>& poss = occur[Lit(x, false).toInt()];
vec<ClauseSimp>& negs = occur[Lit(x, true).toInt()];
// Heuristic CUT OFF:
if (poss.size() >= 10 && negs.size() >= 10)
return false;
// Count clauses/literals before elimination:
int before_clauses = poss.size() + negs.size();
uint32_t before_literals = 0;
for (uint32_t i = 0; i < poss.size(); i++) before_literals += poss[i].clause->size();
for (uint32_t i = 0; i < negs.size(); i++) before_literals += negs[i].clause->size();
// Heuristic CUT OFF2:
if ((poss.size() >= 3 && negs.size() >= 3 && before_literals > 300)
&& clauses.size() > 1500000)
return false;
if ((poss.size() >= 5 && negs.size() >= 5 && before_literals > 400)
&& clauses.size() <= 1500000 && clauses.size() > 200000)
return false;
if ((poss.size() >= 8 && negs.size() >= 8 && before_literals > 700)
&& clauses.size() <= 200000)
return false;
// Count clauses/literals after elimination:
int after_clauses = 0;
vec<Lit> dummy;
for (uint32_t i = 0; i < poss.size(); i++) for (uint32_t j = 0; j < negs.size(); j++){
// Merge clauses. If 'y' and '~y' exist, clause will not be created.
dummy.clear();
bool ok = merge(*poss[i].clause, *negs[j].clause, Lit(x, false), Lit(x, true), dummy);
if (ok){
after_clauses++;
if (after_clauses > before_clauses) goto Abort;
}
}
Abort:;
//Eliminate:
if (after_clauses <= before_clauses) {
vec<ClauseSimp> ps, ns;
MigrateToPsNs(poss, negs, ps, ns, x);
for (uint32_t i = 0; i < ps.size(); i++) for (uint32_t j = 0; j < ns.size(); j++){
dummy.clear();
bool ok = merge(*ps[i].clause, *ns[j].clause, Lit(x, false), Lit(x, true), dummy);
if (ok){
uint32_t group_num = 0;
#ifdef STATS_NEEDED
group_num = solver.learnt_clause_group++;
if (solver.dynamic_behaviour_analysis) {
string name = solver.logger.get_group_name(ps[i].clause->getGroup()) + " " + solver.logger.get_group_name(ns[j].clause->getGroup());
solver.logger.set_group_name(group_num, name);
}
#endif
Clause* cl = solver.addClauseInt(dummy, group_num);
if (cl != NULL) {
ClauseSimp c = linkInClause(*cl);
subsume0(*cl, cl->getAbst());
}
if (!solver.ok) return true;
}
}
DeallocPsNs(ps, ns);
goto Eliminated;
}
return false;
Eliminated:
assert(occur[Lit(x, false).toInt()].size() + occur[Lit(x, true).toInt()].size() == 0);
var_elimed[x] = true;
numElimed++;
solver.setDecisionVar(x, false);
return true;
}
// Returns FALSE if clause is always satisfied ('out_clause' should not be used). 'seen' is assumed to be cleared.
bool Subsumer::merge(const Clause& ps, const Clause& qs, const Lit without_p, const Lit without_q, vec<Lit>& out_clause)
{
for (uint32_t i = 0; i < ps.size(); i++){
if (ps[i] != without_p){
seen_tmp[ps[i].toInt()] = 1;
out_clause.push(ps[i]);
}
}
for (uint32_t i = 0; i < qs.size(); i++){
if (qs[i] != without_q){
if (seen_tmp[(~qs[i]).toInt()]){
for (uint32_t i = 0; i < ps.size(); i++)
seen_tmp[ps[i].toInt()] = 0;
return false;
}
if (!seen_tmp[qs[i].toInt()])
out_clause.push(qs[i]);
}
}
for (uint32_t i = 0; i < ps.size(); i++)
seen_tmp[ps[i].toInt()] = 0;
return true;
}
struct myComp {
bool operator () (const pair<int, Var>& x, const pair<int, Var>& y) {
return x.first < y.first ||
(!(y.first < x.first) && x.second < y.second);
}
};
// Side-effect: Will untouch all variables.
void Subsumer::orderVarsForElim(vec<Var>& order)
{
order.clear();
vec<pair<int, Var> > cost_var;
for (uint32_t i = 0; i < touched_list.size(); i++){
Var x = touched_list[i];
touched[x] = 0;
cost_var.push(std::make_pair( occur[Lit(x, false).toInt()].size() * occur[Lit(x, true).toInt()].size() , x ));
}
touched_list.clear();
std::sort(cost_var.getData(), cost_var.getData()+cost_var.size(), myComp());
for (uint32_t x = 0; x < cost_var.size(); x++) {
if (cost_var[x].first != 0)
order.push(cost_var[x].second);
}
}
const bool Subsumer::hyperUtility(vec<ClauseSimp>& iter, const Lit lit, BitArray& inside, vec<Clause*>& addToClauses)
{
for (ClauseSimp *it = iter.getData(), *end = it + iter.size() ; it != end; it++) {
if (it->clause == NULL) continue;
uint32_t notIn = 0;
Lit notInLit = lit_Undef;
Clause& cl = *it->clause;
for (uint32_t i = 0; i < cl.size(); i++) {
if (cl[i].var() == lit.var() || cl.size() == 2) {
goto next;
}
if (!inside[cl[i].toInt()]) {
notIn++;
if (notIn > 1) goto next;
notInLit = cl[i];
}
}
if (notIn == 0) {
vec<Lit> lits(1);
lits[0] = lit;
solver.addClauseInt(lits, cl.getGroup());
if (!solver.ok) return false;
}
if (notIn == 1 && !inside[(~notInLit).toInt()]) {
vec<Lit> cs(2);
cs[0] = lit;
cs[1] = notInLit;
//uint32_t index = subsume0(cs, calcAbstraction(cs));
/*if (index != std::numeric_limits<uint32_t>::max()) {
Clause *cl3 = Clause_new(cs, cl.getGroup());
ClauseSimp c(cl3, index);
addToClauses.push(c);
inside.setBit((~notInLit).toInt());
#ifdef HYPER_DEBUG
std::cout << "HyperBinRes adding clause: ";
cl3->plainPrint();
#endif
} else {*/
Clause *cl3 = Clause_new(cs, cl.getGroup());
addToClauses.push(cl3);
inside.setBit((~notInLit).toInt());
//}
}
next:;
}
return true;
}
const bool Subsumer::hyperBinRes()
{
double myTime = cpuTime();
BitArray inside;
inside.resize(solver.nVars()*2, 0);
uint32_t hyperBinAdded = 0;
uint32_t oldTrailSize = solver.trail.size();
vec<Clause*> addToClauses;
vec<Lit> addedToInside;
uint64_t totalClausesChecked = 0;
vec<Var> varsToCheck;
if (clauses.size() > 500000 || solver.order_heap.size() > 50000) {
Heap<Solver::VarOrderLt> tmp(solver.order_heap);
uint32_t thisTopX = std::min(tmp.size(), 5000U);
for (uint32_t i = 0; i != thisTopX; i++)
varsToCheck.push(tmp.removeMin());
} else {
for (Var i = 0; i < solver.nVars(); i++)
varsToCheck.push(i);
}
for (uint32_t test = 0; test < 2*varsToCheck.size(); test++) if (solver.assigns[test/2] == l_Undef && solver.decision_var[test/2]) {
if (totalClausesChecked > 1000000)
break;
inside.setZero();
addToClauses.clear();
addedToInside.clear();
Lit lit(varsToCheck[test/2], test&1);
#ifdef HYPER_DEBUG
std::cout << "Resolving with literal:" << (lit.sign() ? "-" : "") << lit.var()+1 << std::endl;
#endif
//fill inside with binary clauses' literals that this lit is in
//addedToInside now contains the list
vec<ClauseSimp>& set = occur[lit.toInt()];
totalClausesChecked += occur.size();
for (ClauseSimp *it = set.getData(), *end = it + set.size() ; it != end; it++) {
if (it->clause == NULL) continue;
Clause& cl2 = *it->clause;
if (cl2.size() > 2) continue;
assert(cl2[0] == lit || cl2[1] == lit);
if (cl2[0] == lit) {
if (!inside[(~cl2[1]).toInt()]) {
inside.setBit((~cl2[1]).toInt());
addedToInside.push(~cl2[1]);
}
} else {
if (!inside[(~cl2[0]).toInt()]) {
inside.setBit((~cl2[0]).toInt());
addedToInside.push(~cl2[0]);
}
}
}
uint32_t sum = 0;
for (uint32_t add = 0; add < addedToInside.size(); add++) {
sum += occur[addedToInside[add].toInt()].size();
}
if (sum < clauses.size()) {
totalClausesChecked += sum;
for (uint32_t add = 0; add < addedToInside.size(); add++) {
vec<ClauseSimp>& iter = occur[addedToInside[add].toInt()];
if (!hyperUtility(iter, lit, inside, addToClauses))
return false;
}
} else {
totalClausesChecked += clauses.size();
if (!hyperUtility(clauses, lit, inside, addToClauses))
return false;
}
hyperBinAdded += addToClauses.size();
for (uint32_t i = 0; i < addToClauses.size(); i++) {
Clause *c = solver.addClauseInt(*addToClauses[i], addToClauses[i]->getGroup());
clauseFree(addToClauses[i]);
if (c != NULL) {
ClauseSimp cc = linkInClause(*c);
subsume1(cc);
}
if (!solver.ok) return false;
}
}
if (solver.verbosity >= 1) {
std::cout << "c | Hyper-binary res binary added: " << std::setw(5) << hyperBinAdded
<< " unitaries: " << std::setw(5) << solver.trail.size() - oldTrailSize
<< " time: " << std::setprecision(2) << std::setw(5)<< cpuTime() - myTime << " s"
<< " |" << std::endl;
}
return true;
}
class varDataStruct
{
public:
varDataStruct() :
numPosClauses (0)
, numNegClauses (0)
, sumPosClauseSize (0)
, sumNegClauseSize (0)
, posHash(0)
, negHash(0)
{}
const bool operator < (const varDataStruct& other) const
{
if (numPosClauses < other.numPosClauses) return true;
if (numPosClauses > other.numPosClauses) return false;
if (numNegClauses < other.numNegClauses) return true;
if (numNegClauses > other.numNegClauses) return false;
if (sumPosClauseSize < other.sumPosClauseSize) return true;
if (sumPosClauseSize > other.sumPosClauseSize) return false;
if (sumNegClauseSize < other.sumNegClauseSize) return true;
if (sumNegClauseSize > other.sumNegClauseSize) return false;
if (posHash < other.posHash) return true;
if (posHash > other.posHash) return false;
if (negHash < other.negHash) return true;
if (negHash > other.negHash) return false;
return false;
}
const bool operator == (const varDataStruct& other) const
{
if (numPosClauses == other.numPosClauses &&
numNegClauses == other.numNegClauses &&
sumPosClauseSize == other.sumPosClauseSize &&
sumNegClauseSize == other.sumNegClauseSize &&
posHash == other.posHash &&
negHash == other.negHash)
return true;
return false;
}
void reversePolarity()
{
std::swap(numPosClauses, numNegClauses);
std::swap(sumPosClauseSize, sumNegClauseSize);
std::swap(posHash, negHash);
}
uint32_t numPosClauses;
uint32_t numNegClauses;
uint32_t sumPosClauseSize;
uint32_t sumNegClauseSize;
int posHash;
int negHash;
};
void Subsumer::verifyIntegrity()
{
vector<uint> occurNum(solver.nVars()*2, 0);
for (uint32_t i = 0; i < clauses.size(); i++) {
if (clauses[i].clause == NULL) continue;
Clause& c = *clauses[i].clause;
for (uint32_t i2 = 0; i2 < c.size(); i2++)
occurNum[c[i2].toInt()]++;
}
for (uint32_t i = 0; i < occurNum.size(); i++) {
assert(occurNum[i] == occur[i].size());
}
}
const bool Subsumer::allTautology(const vec<Lit>& ps, const Lit lit)
{
#ifdef VERBOSE_DEBUG
cout << "allTautology: ";
for (uint32_t i = 0; i < ps.size(); i++) {
if (ps[i].sign()) printf("-");
printf("%d ", ps[i].var() + 1);
}
printf("0\n");
#endif
vec<ClauseSimp>& cs = occur[lit.toInt()];
if (cs.size() == 0) return true;
for (const Lit *l = ps.getData(), *end = ps.getDataEnd(); l != end; l++) {
seen_tmp[l->toInt()] = true;
}
bool allIsTautology = true;
for (ClauseSimp *it = cs.getData(), *end = cs.getDataEnd(); it != end; it++){
if (it+1 != end)
__builtin_prefetch((it+1)->clause, 1, 1);
Clause& c = *it->clause;
for (Lit *l = c.getData(), *end2 = l + c.size(); l != end2; l++) {
if (*l != lit && seen_tmp[(~(*l)).toInt()]) {
goto next;
}
}
allIsTautology = false;
break;
next:;
}
for (const Lit *l = ps.getData(), *end = ps.getDataEnd(); l != end; l++) {
seen_tmp[l->toInt()] = false;
}
return allIsTautology;
}
void Subsumer::blockedClauseRemoval()
{
if (numMaxBlockToVisit < 0) return;
if (solver.order_heap.size() < 1) return;
double myTime = cpuTime();
vec<ClauseSimp> toRemove;
touchedBlockedVars = priority_queue<VarOcc, vector<VarOcc>, MyComp>();
touchedBlockedVarsBool.clear();
touchedBlockedVarsBool.growTo(solver.nVars(), false);
for (uint32_t i = 0; i < solver.order_heap.size() && i < numMaxBlockVars; i++) {
touchBlockedVar(solver.order_heap[solver.mtrand.randInt(solver.order_heap.size()-1)]);
}
while (touchedBlockedVars.size() > 100 && numMaxBlockToVisit > 0) {
VarOcc vo = touchedBlockedVars.top();
touchedBlockedVars.pop();
if (solver.assigns[vo.var] != l_Undef || !solver.decision_var[vo.var] || cannot_eliminate[vo.var])
continue;
touchedBlockedVarsBool[vo.var] = false;
Lit lit = Lit(vo.var, false);
Lit negLit = Lit(vo.var, true);
numMaxBlockToVisit -= (int64_t)occur[lit.toInt()].size();
numMaxBlockToVisit -= (int64_t)occur[negLit.toInt()].size();
//if (!tryOneSetting(lit, negLit)) {
tryOneSetting(negLit, lit);
// }
}
blockTime += cpuTime() - myTime;
#ifdef BIT_MORE_VERBOSITY
std::cout << "c Total fime for block until now: " << blockTime << std::endl;
#endif
}
const bool Subsumer::tryOneSetting(const Lit lit, const Lit negLit)
{
uint32_t toRemove = 0;
bool returnVal = false;
vec<Lit> cl;
for(ClauseSimp *it = occur[lit.toInt()].getData(), *end = occur[lit.toInt()].getDataEnd(); it != end; it++) {
cl.clear();
cl.growTo(it->clause->size()-1);
for (uint32_t i = 0, i2 = 0; i < it->clause->size(); i++) {
if ((*it->clause)[i] != lit) {
cl[i2] = (*it->clause)[i];
i2++;
}
}
if (allTautology(cl, negLit)) {
toRemove++;
} else {
break;
}
}
if (toRemove == occur[lit.toInt()].size()) {
var_elimed[lit.var()] = true;
solver.setDecisionVar(lit.var(), false);
vec<ClauseSimp> toRemove(occur[lit.toInt()]);
for (ClauseSimp *it = toRemove.getData(), *end = toRemove.getDataEnd(); it != end; it++) {
#ifdef VERBOSE_DEBUG
std::cout << "Next varelim because of block clause elim" << std::endl;
#endif //VERBOSE_DEBUG
unlinkClause(*it, lit.var());
numblockedClauseRemoved++;
}
vec<ClauseSimp> toRemove2(occur[negLit.toInt()]);
for (ClauseSimp *it = toRemove2.getData(), *end = toRemove2.getDataEnd(); it != end; it++) {
#ifdef VERBOSE_DEBUG
std::cout << "Next varelim because of block clause elim" << std::endl;
#endif //VERBOSE_DEBUG
unlinkClause(*it, lit.var());
numblockedClauseRemoved++;
}
returnVal = true;
}
return returnVal;
}
const bool Subsumer::checkElimedUnassigned() const
{
for (uint32_t i = 0; i < var_elimed.size(); i++) {
if (var_elimed[i]) {
assert(solver.assigns[i] == l_Undef);
if (solver.assigns[i] != l_Undef) return false;
}
}
return true;
}
/*
int hash32shift(int key)
{
key = ~key + (key << 15); // key = (key << 15) - key - 1;
key = key ^ (key >> 12);
key = key + (key << 2);
key = key ^ (key >> 4);
key = key * 2057; // key = (key + (key << 3)) + (key << 11);
key = key ^ (key >> 16);
return key;
}
vector<char> Subsumer::merge()
{
vector<char> var_merged(solver.nVars(), false);
double myTime = cpuTime();
vector<varDataStruct> varData(solver.nVars());
for (Var var = 0; var < solver.nVars(); var++) if (solver.decision_var[var] && solver.assigns[var] == l_Undef && !cannot_eliminate[var]) {
varDataStruct thisVar;
vec<ClauseSimp>& toCountPos = occur[Lit(var, false).toInt()];
thisVar.numPosClauses = toCountPos.size();
for (uint32_t i2 = 0; i2 < toCountPos.size(); i2++) {
thisVar.sumPosClauseSize += toCountPos[i2].clause->size();
for (Lit *l = toCountPos[i2].clause->getData(), *end = l + toCountPos[i2].clause->size(); l != end; l++) {
if (l->var() != var) thisVar.posHash ^= hash32shift(l->toInt());
}
}
vec<ClauseSimp>& toCountNeg = occur[Lit(var, true).toInt()];
thisVar.numNegClauses = toCountNeg.size();
for (uint32_t i2 = 0; i2 < toCountNeg.size(); i2++) {
thisVar.sumNegClauseSize += toCountNeg[i2].clause->size();
for (Lit *l = toCountNeg[i2].clause->getData(), *end = l + toCountNeg[i2].clause->size(); l != end; l++) {
if (l->var() != var) thisVar.negHash ^= hash32shift(l->toInt());
}
}
varData[var] = thisVar;
}
map<varDataStruct, vector<Var> > dataToVar;
for (Var var = 0; var < solver.nVars(); var++) if (solver.decision_var[var] && solver.assigns[var] == l_Undef) {
dataToVar[varData[var]].push_back(var);
assert(dataToVar[varData[var]].size() > 0);
}
for (map<varDataStruct, vector<Var> >::iterator it = dataToVar.begin(); it != dataToVar.end(); it++) {
//std::cout << "size: " << it->second.size() << std::endl;
for (uint i = 0; i < it->second.size()-1; i++) {
assert(it->second.size() > i+1);
assert(varData[it->second[i]] == varData[it->second[i+1]]);
}
}
uint64_t checked = 0;
uint64_t replaced = 0;
for (Var var = 0; var < solver.nVars(); var++) if (solver.decision_var[var] && solver.assigns[var] == l_Undef && !cannot_eliminate[var]) {
varDataStruct tmp = varData[var];
assert(dataToVar[tmp].size() > 0);
if (dataToVar[tmp].size() > 0) {
map<varDataStruct, vector<Var> >::iterator it = dataToVar.find(tmp);
for (uint i = 0; i < it->second.size(); i++) if (it->second[i] != var) {
checked ++;
if (checkIfSame(Lit(var, false), Lit(it->second[i], false)) &&
(checkIfSame(Lit(var, true), Lit(it->second[i], true))))
{
vec<Lit> ps(2);
ps[0] = Lit(var, false);
ps[1] = Lit(it->second[i], false);
solver.varReplacer->replace(ps, true, 0);
replaced++;
goto next;
}
}
}
tmp.reversePolarity();
if (dataToVar[tmp].size() > 0) {
map<varDataStruct, vector<Var> >::iterator it = dataToVar.find(tmp);
for (uint i = 0; i < it->second.size(); i++) if (it->second[i] != var) {
checked ++;
if (checkIfSame(Lit(var, true), Lit(it->second[i], false)) &&
(checkIfSame(Lit(var, false), Lit(it->second[i], true))))
{
vec<Lit> ps(2);
ps[0] = Lit(var, false);
ps[1] = Lit(it->second[i], false);
solver.varReplacer->replace(ps, false, 0);
replaced++;
goto next;
}
}
}
next:;
}
std::cout << "c | Merging vars in same clauses. checked: " << std::setw(5) << checked << " replaced: " << std::setw(5) << replaced << " time: " << std::setprecision(2) << std::setw(5) << cpuTime()-myTime << std::endl;
return var_merged;
}*/
/*const bool Subsumer::checkIfSame(const Lit lit1, const Lit lit2)
{
assert(lit1.var() != lit2.var());
#ifdef VERBOSE_DEBUG
std::cout << "checking : " << lit1.var()+1 << " , " << lit2.var()+1 << std::endl;
#endif
vec<ClauseSimp>& occSet1 = occur[lit1.toInt()];
vec<ClauseSimp>& occSet2 = occur[lit2.toInt()];
vec<Lit> tmp;
for (ClauseSimp *it = occSet1.getData(), *end = it + occSet1.size(); it != end; it++) {
bool found = false;
tmp.clear();
uint32_t clauseSize = it->clause->size();
for (Lit *l = it->clause->getData(), *end2 = l + it->clause->size(); l != end2; l++) {
if (l->var() != lit1.var()) {
tmp.push(*l);
seen_tmp[l->toInt()] = true;
}
}
#ifdef VERBOSE_DEBUG
std::cout << "orig: ";
it->clause->plainPrint();
#endif
for (ClauseSimp *it2 = occSet2.getData(), *end2 = it2 + occSet2.size(); (it2 != end2 && !found); it2++) {
if (it2->clause->size() != clauseSize) continue;
for (Lit *l = it2->clause->getData(), *end3 = l + tmp.size(); l != end3; l++) if (l->var() != lit1.var()) {
if (!seen_tmp[l->toInt()]) goto next;
}
found = true;
#ifdef VERBOSE_DEBUG
std::cout << "OK: ";
it2->clause->plainPrint();
#endif
next:;
}
for (Lit *l = tmp.getData(), *end2 = l + tmp.size(); l != end2; l++) {
seen_tmp[l->toInt()] = false;
}
if (!found) return false;
}
#ifdef VERBOSE_DEBUG
std::cout << "OK" << std::endl;
#endif
return true;
}*/
/*void Subsumer::pureLiteralRemoval()
{
for (Var var = 0; var < solver.nVars(); var++) if (solver.decision_var[var] && solver.assigns[var] == l_Undef && !cannot_eliminate[var] && !var_elimed[var] && !solver.varReplacer->varHasBeenReplaced(var)) {
uint32_t numPosClauses = occur[Lit(var, false).toInt()].size();
uint32_t numNegClauses = occur[Lit(var, true).toInt()].size();
if (numNegClauses > 0 && numPosClauses > 0) continue;
if (numNegClauses == 0 && numPosClauses == 0) {
if (solver.decision_var[var]) madeVarNonDecision.push(var);
solver.setDecisionVar(var, false);
pureLitRemoved[var] = true;
pureLitsRemovedNum++;
continue;
}
if (numPosClauses == 0 && numNegClauses > 0) {
if (solver.decision_var[var]) madeVarNonDecision.push(var);
solver.setDecisionVar(var, false);
pureLitRemoved[var] = true;
assignVar.push(Lit(var, true));
vec<ClauseSimp> occ(occur[Lit(var, true).toInt()]);
for (ClauseSimp *it = occ.getData(), *end = occ.getDataEnd(); it != end; it++) {
unlinkClause(*it);
pureLitClauseRemoved.push(it->clause);
}
pureLitsRemovedNum++;
continue;
}
if (numNegClauses == 0 && numPosClauses > 0) {
if (solver.decision_var[var]) madeVarNonDecision.push(var);
solver.setDecisionVar(var, false);
pureLitRemoved[var] = true;
assignVar.push(Lit(var, false));
vec<ClauseSimp> occ(occur[Lit(var, false).toInt()]);
for (ClauseSimp *it = occ.getData(), *end = occ.getDataEnd(); it != end; it++) {
unlinkClause(*it);
pureLitClauseRemoved.push(it->clause);
}
pureLitsRemovedNum++;
continue;
}
}
}*/
/*void Subsumer::undoPureLitRemoval()
{
assert(solver.ok);
for (uint32_t i = 0; i < madeVarNonDecision.size(); i++) {
assert(!solver.decision_var[madeVarNonDecision[i]]);
assert(solver.assigns[madeVarNonDecision[i]] == l_Undef);
solver.setDecisionVar(madeVarNonDecision[i], true);
pureLitRemoved[madeVarNonDecision[i]] = false;
}
madeVarNonDecision.clear();
for (Lit *l = assignVar.getData(), *end = assignVar.getDataEnd(); l != end; l++) {
solver.uncheckedEnqueue(*l);
solver.ok = (solver.propagate() == NULL);
assert(solver.ok);
}
assignVar.clear();
}
void Subsumer::reAddPureLitClauses()
{
for (Clause **it = pureLitClauseRemoved.getData(), **end = pureLitClauseRemoved.getDataEnd(); it != end; it++) {
solver.addClause(**it, (*it)->getGroup());
clauseFree(*it);
assert(solver.ok);
}
pureLitClauseRemoved.clear();
}*/