/***************************************************************************
CryptoMiniSat -- Copyright (c) 2009 Mate Soos
This program is free software: you can redistribute it and/or modify
it under the terms of the GNU General Public License as published by
the Free Software Foundation, either version 3 of the License, or
(at your option) any later version.
This program is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
GNU General Public License for more details.
You should have received a copy of the GNU General Public License
along with this program. If not, see .
****************************************************************************/
#include
#include "UselessBinRemover.h"
#include "VarReplacer.h"
#include "ClauseCleaner.h"
#include "time_mem.h"
//#define VERBOSE_DEBUG
using namespace CMSat;
UselessBinRemover::UselessBinRemover(Solver& _solver) :
solver(_solver)
{
}
/**
@brief Time limiting
*/
#define MAX_REMOVE_BIN_FULL_PROPS 20000000
/**
@brief We measure time in (bogo)propagations and "extra" time, time not accountable in (bogo)props
*/
#define EXTRATIME_DIVIDER 3
/**
@brief Removes useless binary non-learnt clauses. See definiton of class for details
We pick variables starting randomly at a place and going on until we stop:
we limit ourselves in time using (bogo)propagations and "extratime"
*/
bool UselessBinRemover::removeUslessBinFull()
{
double myTime = cpuTime();
toDeleteSet.clear();
toDeleteSet.growTo(solver.nVars()*2, 0);
uint32_t origHeapSize = solver.order_heap.size();
uint64_t origProps = solver.propagations;
bool fixed = false;
uint32_t extraTime = 0;
uint32_t numBinsBefore = solver.numBins;
solver.sortWatched(); //VERY important
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 - origProps + extraTime > MAX_REMOVE_BIN_FULL_PROPS) break;
if (solver.assigns[var] != l_Undef || !solver.decision_var[var]) continue;
Lit lit(var, true);
if (!removeUselessBinaries(lit)) {
fixed = true;
solver.cancelUntilLight();
solver.uncheckedEnqueue(~lit);
solver.ok = (solver.propagate().isNULL());
if (!solver.ok) return false;
continue;
}
lit = ~lit;
if (!removeUselessBinaries(lit)) {
fixed = true;
solver.cancelUntilLight();
solver.uncheckedEnqueue(~lit);
solver.ok = (solver.propagate().isNULL());
if (!solver.ok) return false;
continue;
}
}
if (fixed) solver.order_heap.filter(Solver::VarFilter(solver));
if (solver.conf.verbosity >= 1) {
std::cout
<< "c Removed useless bin:" << std::setw(8) << (numBinsBefore - solver.numBins)
<< " fixed: " << std::setw(5) << (origHeapSize - solver.order_heap.size())
<< " props: " << std::fixed << std::setprecision(2) << std::setw(6) << (double)(solver.propagations - origProps)/1000000.0 << "M"
<< " time: " << std::fixed << std::setprecision(2) << std::setw(5) << cpuTime() - myTime << " s"
<< std::endl;
}
return true;
}
/**
@brief Removes useless binaries of the graph portion that starts with lit
We try binary-space propagation on lit. Then, we check that we cannot reach any
of its one-hop neighboours from any of its other one-hope neighbours. If we can,
we remove the one-hop neighbour from the neightbours (i.e. remove the binary
clause). Example:
\li a->b, a->c, b->c
\li In claues: (-a V b), (-a V c), (-b V c)
One-hop neighbours of a: b, c. But c can be reached through b! So, we remove
a->c, the one-hop neighbour that is useless.
*/
bool UselessBinRemover::removeUselessBinaries(const Lit lit)
{
solver.newDecisionLevel();
solver.uncheckedEnqueueLight(lit);
//Propagate only one hop
failed = !solver.propagateBinOneLevel();
if (failed) return false;
bool ret = true;
oneHopAway.clear();
assert(solver.decisionLevel() > 0);
int c;
if (solver.trail.size()-solver.trail_lim[0] == 0) {
solver.cancelUntilLight();
goto end;
}
//Fill oneHopAway and toDeleteSet with lits that are 1 hop away
extraTime += (solver.trail.size() - solver.trail_lim[0]) / EXTRATIME_DIVIDER;
for (c = solver.trail.size()-1; c > (int)solver.trail_lim[0]; c--) {
Lit x = solver.trail[c];
toDeleteSet[x.toInt()] = true;
oneHopAway.push(x);
solver.assigns[x.var()] = l_Undef;
}
solver.assigns[solver.trail[c].var()] = l_Undef;
solver.qhead = solver.trail_lim[0];
solver.trail.shrink_(solver.trail.size() - solver.trail_lim[0]);
solver.trail_lim.clear();
//solver.cancelUntil(0);
wrong.clear();
//We now try to reach the one-hop-away nodes from other one-hop-away
//nodes, but this time we propagate all the way
for(uint32_t i = 0; i < oneHopAway.size(); i++) {
//no need to visit it if it already queued for removal
//basically, we check if it's in 'wrong'
if (toDeleteSet[oneHopAway[i].toInt()]) {
if (!fillBinImpliesMinusLast(lit, oneHopAway[i], wrong)) {
ret = false;
goto end;
}
}
}
for (uint32_t i = 0; i < wrong.size(); i++) {
removeBin(~lit, wrong[i]);
}
end:
for(uint32_t i = 0; i < oneHopAway.size(); i++) {
toDeleteSet[oneHopAway[i].toInt()] = false;
}
return ret;
}
/**
@brief Removes a binary clause (lit1 V lit2)
The binary clause might be in twice, three times, etc. Take care to remove
all instances of it.
*/
void UselessBinRemover::removeBin(const Lit lit1, const Lit lit2)
{
#ifdef VERBOSE_DEBUG
std::cout << "Removing useless bin: " << lit1 << " " << lit2 << std::endl;
#endif //VERBOSE_DEBUG
std::pair removed1 = removeWBinAll(solver.watches[(~lit1).toInt()], lit2);
std::pair removed2 = removeWBinAll(solver.watches[(~lit2).toInt()], lit1);
assert(removed1 == removed2);
assert((removed1.first + removed2.first) % 2 == 0);
assert((removed1.second + removed2.second) % 2 == 0);
solver.learnts_literals -= (removed1.first + removed2.first);
solver.clauses_literals -= (removed1.second + removed2.second);
solver.numBins -= (removed1.first + removed2.first + removed1.second + removed2.second)/2;
}
/**
@brief Propagates all the way lit, but doesn't propagate origLit
Removes adds to "wrong" the set of one-hop lits that can be reached from
lit AND are one-hop away from origLit. These later need to be removed
*/
bool UselessBinRemover::fillBinImpliesMinusLast(const Lit origLit, const Lit lit, vec& wrong)
{
solver.newDecisionLevel();
solver.uncheckedEnqueueLight(lit);
//if it's a cycle, it doesn't work, so don't propagate origLit
failed = !solver.propagateBinExcept(origLit);
if (failed) return false;
assert(solver.decisionLevel() > 0);
int c;
extraTime += (solver.trail.size() - solver.trail_lim[0]) / EXTRATIME_DIVIDER;
for (c = solver.trail.size()-1; c > (int)solver.trail_lim[0]; c--) {
Lit x = solver.trail[c];
if (toDeleteSet[x.toInt()]) {
wrong.push(x);
toDeleteSet[x.toInt()] = false;
};
solver.assigns[x.var()] = l_Undef;
}
solver.assigns[solver.trail[c].var()] = l_Undef;
solver.qhead = solver.trail_lim[0];
solver.trail.shrink_(solver.trail.size() - solver.trail_lim[0]);
solver.trail_lim.clear();
//solver.cancelUntil(0);
return true;
}