QA_SAT/qubo_lab
2
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

added minisat code base

Browse Source
This commit is contained in:
Tom
2019-02-08 23:07:45 +01:00
parent 0a0fbcc46d
commit 4f9ae6c67d
31 changed files with 5063 additions and 8 deletions
Download Patch File Download Diff File Expand all files Collapse all files

211
minisat/simp/Main.cc Normal file
View File

@@ -0,0 +1,211 @@
/*****************************************************************************************[Main.cc]
Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson
Copyright (c) 2007, Niklas Sorensson
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
associated documentation files (the "Software"), to deal in the Software without restriction,
including without limitation the rights to use, copy, modify, merge, publish, distribute,
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all copies or
substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/
#include <errno.h>
#include <signal.h>
#include <zlib.h>
#include <sys/resource.h>
#include "utils/System.h"
#include "utils/ParseUtils.h"
#include "utils/Options.h"
#include "core/Dimacs.h"
#include "simp/SimpSolver.h"
using namespace Minisat;
//=================================================================================================
void printStats(Solver& solver)
{
double cpu_time = cpuTime();
double mem_used = memUsedPeak();
printf("restarts : %"PRIu64"\n", solver.starts);
printf("conflicts : %-12"PRIu64" (%.0f /sec)\n", solver.conflicts , solver.conflicts /cpu_time);
printf("decisions : %-12"PRIu64" (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions /cpu_time);
printf("propagations : %-12"PRIu64" (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time);
printf("conflict literals : %-12"PRIu64" (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals);
if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used);
printf("CPU time : %g s\n", cpu_time);
}
static Solver* solver;
// Terminate by notifying the solver and back out gracefully. This is mainly to have a test-case
// for this feature of the Solver as it may take longer than an immediate call to '_exit()'.
static void SIGINT_interrupt(int signum) { solver->interrupt(); }
// Note that '_exit()' rather than 'exit()' has to be used. The reason is that 'exit()' calls
// destructors and may cause deadlocks if a malloc/free function happens to be running (these
// functions are guarded by locks for multithreaded use).
static void SIGINT_exit(int signum) {
printf("\n"); printf("*** INTERRUPTED ***\n");
if (solver->verbosity > 0){
printStats(*solver);
printf("\n"); printf("*** INTERRUPTED ***\n"); }
_exit(1); }
//=================================================================================================
// Main:
int main(int argc, char** argv)
{
try {
setUsageHelp("USAGE: %s [options] <input-file> <result-output-file>\n\n where input may be either in plain or gzipped DIMACS.\n");
// printf("This is MiniSat 2.0 beta\n");
#if defined(__linux__)
fpu_control_t oldcw, newcw;
_FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw);
printf("WARNING: for repeatability, setting FPU to use double precision\n");
#endif
// Extra options:
//
IntOption verb ("MAIN", "verb", "Verbosity level (0=silent, 1=some, 2=more).", 1, IntRange(0, 2));
BoolOption pre ("MAIN", "pre", "Completely turn on/off any preprocessing.", true);
StringOption dimacs ("MAIN", "dimacs", "If given, stop after preprocessing and write the result to this file.");
IntOption cpu_lim("MAIN", "cpu-lim","Limit on CPU time allowed in seconds.\n", INT32_MAX, IntRange(0, INT32_MAX));
IntOption mem_lim("MAIN", "mem-lim","Limit on memory usage in megabytes.\n", INT32_MAX, IntRange(0, INT32_MAX));
parseOptions(argc, argv, true);
SimpSolver S;
double initial_time = cpuTime();
if (!pre) S.eliminate(true);
S.verbosity = verb;
solver = &S;
// Use signal handlers that forcibly quit until the solver will be able to respond to
// interrupts:
signal(SIGINT, SIGINT_exit);
signal(SIGXCPU,SIGINT_exit);
// Set limit on CPU-time:
if (cpu_lim != INT32_MAX){
rlimit rl;
getrlimit(RLIMIT_CPU, &rl);
if (rl.rlim_max == RLIM_INFINITY || (rlim_t)cpu_lim < rl.rlim_max){
rl.rlim_cur = cpu_lim;
if (setrlimit(RLIMIT_CPU, &rl) == -1)
printf("WARNING! Could not set resource limit: CPU-time.\n");
} }
// Set limit on virtual memory:
if (mem_lim != INT32_MAX){
rlim_t new_mem_lim = (rlim_t)mem_lim * 1024*1024;
rlimit rl;
getrlimit(RLIMIT_AS, &rl);
if (rl.rlim_max == RLIM_INFINITY || new_mem_lim < rl.rlim_max){
rl.rlim_cur = new_mem_lim;
if (setrlimit(RLIMIT_AS, &rl) == -1)
printf("WARNING! Could not set resource limit: Virtual memory.\n");
} }
if (argc == 1)
printf("Reading from standard input... Use '--help' for help.\n");
gzFile in = (argc == 1) ? gzdopen(0, "rb") : gzopen(argv[1], "rb");
if (in == NULL)
printf("ERROR! Could not open file: %s\n", argc == 1 ? "<stdin>" : argv[1]), exit(1);
if (S.verbosity > 0){
printf("============================[ Problem Statistics ]=============================\n");
printf("| |\n"); }
parse_DIMACS(in, S);
gzclose(in);
FILE* res = (argc >= 3) ? fopen(argv[2], "wb") : NULL;
if (S.verbosity > 0){
printf("| Number of variables: %12d |\n", S.nVars());
printf("| Number of clauses: %12d |\n", S.nClauses()); }
double parsed_time = cpuTime();
if (S.verbosity > 0)
printf("| Parse time: %12.2f s |\n", parsed_time - initial_time);
// Change to signal-handlers that will only notify the solver and allow it to terminate
// voluntarily:
signal(SIGINT, SIGINT_interrupt);
signal(SIGXCPU,SIGINT_interrupt);
S.eliminate(true);
double simplified_time = cpuTime();
if (S.verbosity > 0){
printf("| Simplification time: %12.2f s |\n", simplified_time - parsed_time);
printf("| |\n"); }
if (!S.okay()){
if (res != NULL) fprintf(res, "UNSAT\n"), fclose(res);
if (S.verbosity > 0){
printf("===============================================================================\n");
printf("Solved by simplification\n");
printStats(S);
printf("\n"); }
printf("UNSATISFIABLE\n");
exit(20);
}
if (dimacs){
if (S.verbosity > 0)
printf("==============================[ Writing DIMACS ]===============================\n");
S.toDimacs((const char*)dimacs);
if (S.verbosity > 0)
printStats(S);
exit(0);
}
vec<Lit> dummy;
lbool ret = S.solveLimited(dummy);
if (S.verbosity > 0){
printStats(S);
printf("\n"); }
printf(ret == l_True ? "SATISFIABLE\n" : ret == l_False ? "UNSATISFIABLE\n" : "INDETERMINATE\n");
if (res != NULL){
if (ret == l_True){
fprintf(res, "SAT\n");
for (int i = 0; i < S.nVars(); i++)
if (S.model[i] != l_Undef)
fprintf(res, "%s%s%d", (i==0)?"":" ", (S.model[i]==l_True)?"":"-", i+1);
fprintf(res, " 0\n");
}else if (ret == l_False)
fprintf(res, "UNSAT\n");
else
fprintf(res, "INDET\n");
fclose(res);
}
#ifdef NDEBUG
exit(ret == l_True ? 10 : ret == l_False ? 20 : 0); // (faster than "return", which will invoke the destructor for 'Solver')
#else
return (ret == l_True ? 10 : ret == l_False ? 20 : 0);
#endif
} catch (OutOfMemoryException&){
printf("===============================================================================\n");
printf("INDETERMINATE\n");
exit(0);
}
}

4
minisat/simp/Makefile Normal file
View File

@@ -0,0 +1,4 @@
EXEC = minisat
DEPDIR = mtl utils core
include $(MROOT)/mtl/template.mk

717
minisat/simp/SimpSolver.cc Normal file
View File

@@ -0,0 +1,717 @@
/***********************************************************************************[SimpSolver.cc]
Copyright (c) 2006, Niklas Een, Niklas Sorensson
Copyright (c) 2007-2010, Niklas Sorensson
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
associated documentation files (the "Software"), to deal in the Software without restriction,
including without limitation the rights to use, copy, modify, merge, publish, distribute,
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all copies or
substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/
#include "mtl/Sort.h"
#include "simp/SimpSolver.h"
#include "utils/System.h"
using namespace Minisat;
//=================================================================================================
// Options:
static const char* _cat = "SIMP";
static BoolOption opt_use_asymm (_cat, "asymm", "Shrink clauses by asymmetric branching.", false);
static BoolOption opt_use_rcheck (_cat, "rcheck", "Check if a clause is already implied. (costly)", false);
static BoolOption opt_use_elim (_cat, "elim", "Perform variable elimination.", true);
static IntOption opt_grow (_cat, "grow", "Allow a variable elimination step to grow by a number of clauses.", 0);
static IntOption opt_clause_lim (_cat, "cl-lim", "Variables are not eliminated if it produces a resolvent with a length above this limit. -1 means no limit", 20, IntRange(-1, INT32_MAX));
static IntOption opt_subsumption_lim (_cat, "sub-lim", "Do not check if subsumption against a clause larger than this. -1 means no limit.", 1000, IntRange(-1, INT32_MAX));
static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of wasted memory allowed before a garbage collection is triggered during simplification.", 0.5, DoubleRange(0, false, HUGE_VAL, false));
//=================================================================================================
// Constructor/Destructor:
SimpSolver::SimpSolver() :
grow (opt_grow)
, clause_lim (opt_clause_lim)
, subsumption_lim (opt_subsumption_lim)
, simp_garbage_frac (opt_simp_garbage_frac)
, use_asymm (opt_use_asymm)
, use_rcheck (opt_use_rcheck)
, use_elim (opt_use_elim)
, merges (0)
, asymm_lits (0)
, eliminated_vars (0)
, elimorder (1)
, use_simplification (true)
, occurs (ClauseDeleted(ca))
, elim_heap (ElimLt(n_occ))
, bwdsub_assigns (0)
, n_touched (0)
{
vec<Lit> dummy(1,lit_Undef);
ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below.
bwdsub_tmpunit = ca.alloc(dummy);
remove_satisfied = false;
}
SimpSolver::~SimpSolver()
{
}
Var SimpSolver::newVar(bool sign, bool dvar) {
Var v = Solver::newVar(sign, dvar);
frozen .push((char)false);
eliminated.push((char)false);
if (use_simplification){
n_occ .push(0);
n_occ .push(0);
occurs .init(v);
touched .push(0);
elim_heap .insert(v);
}
return v; }
lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
{
vec<Var> extra_frozen;
lbool result = l_True;
do_simp &= use_simplification;
if (do_simp){
// Assumptions must be temporarily frozen to run variable elimination:
for (int i = 0; i < assumptions.size(); i++){
Var v = var(assumptions[i]);
// If an assumption has been eliminated, remember it.
assert(!isEliminated(v));
if (!frozen[v]){
// Freeze and store.
setFrozen(v, true);
extra_frozen.push(v);
} }
result = lbool(eliminate(turn_off_simp));
}
if (result == l_True)
result = Solver::solve_();
else if (verbosity >= 1)
printf("===============================================================================\n");
if (result == l_True)
extendModel();
if (do_simp)
// Unfreeze the assumptions that were frozen:
for (int i = 0; i < extra_frozen.size(); i++)
setFrozen(extra_frozen[i], false);
return result;
}
bool SimpSolver::addClause_(vec<Lit>& ps)
{
#ifndef NDEBUG
for (int i = 0; i < ps.size(); i++)
assert(!isEliminated(var(ps[i])));
#endif
int nclauses = clauses.size();
if (use_rcheck && implied(ps))
return true;
if (!Solver::addClause_(ps))
return false;
if (use_simplification && clauses.size() == nclauses + 1){
CRef cr = clauses.last();
const Clause& c = ca[cr];
// NOTE: the clause is added to the queue immediately and then
// again during 'gatherTouchedClauses()'. If nothing happens
// in between, it will only be checked once. Otherwise, it may
// be checked twice unnecessarily. This is an unfortunate
// consequence of how backward subsumption is used to mimic
// forward subsumption.
subsumption_queue.insert(cr);
for (int i = 0; i < c.size(); i++){
occurs[var(c[i])].push(cr);
n_occ[toInt(c[i])]++;
touched[var(c[i])] = 1;
n_touched++;
if (elim_heap.inHeap(var(c[i])))
elim_heap.increase(var(c[i]));
}
}
return true;
}
void SimpSolver::removeClause(CRef cr)
{
const Clause& c = ca[cr];
if (use_simplification)
for (int i = 0; i < c.size(); i++){
n_occ[toInt(c[i])]--;
updateElimHeap(var(c[i]));
occurs.smudge(var(c[i]));
}
Solver::removeClause(cr);
}
bool SimpSolver::strengthenClause(CRef cr, Lit l)
{
Clause& c = ca[cr];
assert(decisionLevel() == 0);
assert(use_simplification);
// FIX: this is too inefficient but would be nice to have (properly implemented)
// if (!find(subsumption_queue, &c))
subsumption_queue.insert(cr);
if (c.size() == 2){
removeClause(cr);
c.strengthen(l);
}else{
detachClause(cr, true);
c.strengthen(l);
attachClause(cr);
remove(occurs[var(l)], cr);
n_occ[toInt(l)]--;
updateElimHeap(var(l));
}
return c.size() == 1 ? enqueue(c[0]) && propagate() == CRef_Undef : true;
}
// Returns FALSE if clause is always satisfied ('out_clause' should not be used).
bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause)
{
merges++;
out_clause.clear();
bool ps_smallest = _ps.size() < _qs.size();
const Clause& ps = ps_smallest ? _qs : _ps;
const Clause& qs = ps_smallest ? _ps : _qs;
for (int i = 0; i < qs.size(); i++){
if (var(qs[i]) != v){
for (int j = 0; j < ps.size(); j++)
if (var(ps[j]) == var(qs[i]))
if (ps[j] == ~qs[i])
return false;
else
goto next;
out_clause.push(qs[i]);
}
next:;
}
for (int i = 0; i < ps.size(); i++)
if (var(ps[i]) != v)
out_clause.push(ps[i]);
return true;
}
// Returns FALSE if clause is always satisfied.
bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size)
{
merges++;
bool ps_smallest = _ps.size() < _qs.size();
const Clause& ps = ps_smallest ? _qs : _ps;
const Clause& qs = ps_smallest ? _ps : _qs;
const Lit* __ps = (const Lit*)ps;
const Lit* __qs = (const Lit*)qs;
size = ps.size()-1;
for (int i = 0; i < qs.size(); i++){
if (var(__qs[i]) != v){
for (int j = 0; j < ps.size(); j++)
if (var(__ps[j]) == var(__qs[i]))
if (__ps[j] == ~__qs[i])
return false;
else
goto next;
size++;
}
next:;
}
return true;
}
void SimpSolver::gatherTouchedClauses()
{
if (n_touched == 0) return;
int i,j;
for (i = j = 0; i < subsumption_queue.size(); i++)
if (ca[subsumption_queue[i]].mark() == 0)
ca[subsumption_queue[i]].mark(2);
for (i = 0; i < touched.size(); i++)
if (touched[i]){
const vec<CRef>& cs = occurs.lookup(i);
for (j = 0; j < cs.size(); j++)
if (ca[cs[j]].mark() == 0){
subsumption_queue.insert(cs[j]);
ca[cs[j]].mark(2);
}
touched[i] = 0;
}
for (i = 0; i < subsumption_queue.size(); i++)
if (ca[subsumption_queue[i]].mark() == 2)
ca[subsumption_queue[i]].mark(0);
n_touched = 0;
}
bool SimpSolver::implied(const vec<Lit>& c)
{
assert(decisionLevel() == 0);
trail_lim.push(trail.size());
for (int i = 0; i < c.size(); i++)
if (value(c[i]) == l_True){
cancelUntil(0);
return false;
}else if (value(c[i]) != l_False){
assert(value(c[i]) == l_Undef);
uncheckedEnqueue(~c[i]);
}
bool result = propagate() != CRef_Undef;
cancelUntil(0);
return result;
}
// Backward subsumption + backward subsumption resolution
bool SimpSolver::backwardSubsumptionCheck(bool verbose)
{
int cnt = 0;
int subsumed = 0;
int deleted_literals = 0;
assert(decisionLevel() == 0);
while (subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()){
// Empty subsumption queue and return immediately on user-interrupt:
if (asynch_interrupt){
subsumption_queue.clear();
bwdsub_assigns = trail.size();
break; }
// Check top-level assignments by creating a dummy clause and placing it in the queue:
if (subsumption_queue.size() == 0 && bwdsub_assigns < trail.size()){
Lit l = trail[bwdsub_assigns++];
ca[bwdsub_tmpunit][0] = l;
ca[bwdsub_tmpunit].calcAbstraction();
subsumption_queue.insert(bwdsub_tmpunit); }
CRef cr = subsumption_queue.peek(); subsumption_queue.pop();
Clause& c = ca[cr];
if (c.mark()) continue;
if (verbose && verbosity >= 2 && cnt++ % 1000 == 0)
printf("subsumption left: %10d (%10d subsumed, %10d deleted literals)\r", subsumption_queue.size(), subsumed, deleted_literals);
assert(c.size() > 1 || value(c[0]) == l_True); // Unit-clauses should have been propagated before this point.
// Find best variable to scan:
Var best = var(c[0]);
for (int i = 1; i < c.size(); i++)
if (occurs[var(c[i])].size() < occurs[best].size())
best = var(c[i]);
// Search all candidates:
vec<CRef>& _cs = occurs.lookup(best);
CRef* cs = (CRef*)_cs;
for (int j = 0; j < _cs.size(); j++)
if (c.mark())
break;
else if (!ca[cs[j]].mark() && cs[j] != cr && (subsumption_lim == -1 || ca[cs[j]].size() < subsumption_lim)){
Lit l = c.subsumes(ca[cs[j]]);
if (l == lit_Undef)
subsumed++, removeClause(cs[j]);
else if (l != lit_Error){
deleted_literals++;
if (!strengthenClause(cs[j], ~l))
return false;
// Did current candidate get deleted from cs? Then check candidate at index j again:
if (var(l) == best)
j--;
}
}
}
return true;
}
bool SimpSolver::asymm(Var v, CRef cr)
{
Clause& c = ca[cr];
assert(decisionLevel() == 0);
if (c.mark() || satisfied(c)) return true;
trail_lim.push(trail.size());
Lit l = lit_Undef;
for (int i = 0; i < c.size(); i++)
if (var(c[i]) != v && value(c[i]) != l_False)
uncheckedEnqueue(~c[i]);
else
l = c[i];
if (propagate() != CRef_Undef){
cancelUntil(0);
asymm_lits++;
if (!strengthenClause(cr, l))
return false;
}else
cancelUntil(0);
return true;
}
bool SimpSolver::asymmVar(Var v)
{
assert(use_simplification);
const vec<CRef>& cls = occurs.lookup(v);
if (value(v) != l_Undef || cls.size() == 0)
return true;
for (int i = 0; i < cls.size(); i++)
if (!asymm(v, cls[i]))
return false;
return backwardSubsumptionCheck();
}
static void mkElimClause(vec<uint32_t>& elimclauses, Lit x)
{
elimclauses.push(toInt(x));
elimclauses.push(1);
}
static void mkElimClause(vec<uint32_t>& elimclauses, Var v, Clause& c)
{
int first = elimclauses.size();
int v_pos = -1;
// Copy clause to elimclauses-vector. Remember position where the
// variable 'v' occurs:
for (int i = 0; i < c.size(); i++){
elimclauses.push(toInt(c[i]));
if (var(c[i]) == v)
v_pos = i + first;
}
assert(v_pos != -1);
// Swap the first literal with the 'v' literal, so that the literal
// containing 'v' will occur first in the clause:
uint32_t tmp = elimclauses[v_pos];
elimclauses[v_pos] = elimclauses[first];
elimclauses[first] = tmp;
// Store the length of the clause last:
elimclauses.push(c.size());
}
bool SimpSolver::eliminateVar(Var v)
{
assert(!frozen[v]);
assert(!isEliminated(v));
assert(value(v) == l_Undef);
// Split the occurrences into positive and negative:
//
const vec<CRef>& cls = occurs.lookup(v);
vec<CRef> pos, neg;
for (int i = 0; i < cls.size(); i++)
(find(ca[cls[i]], mkLit(v)) ? pos : neg).push(cls[i]);
// Check wether the increase in number of clauses stays within the allowed ('grow'). Moreover, no
// clause must exceed the limit on the maximal clause size (if it is set):
//
int cnt = 0;
int clause_size = 0;
for (int i = 0; i < pos.size(); i++)
for (int j = 0; j < neg.size(); j++)
if (merge(ca[pos[i]], ca[neg[j]], v, clause_size) &&
(++cnt > cls.size() + grow || (clause_lim != -1 && clause_size > clause_lim)))
return true;
// Delete and store old clauses:
eliminated[v] = true;
setDecisionVar(v, false);
eliminated_vars++;
if (pos.size() > neg.size()){
for (int i = 0; i < neg.size(); i++)
mkElimClause(elimclauses, v, ca[neg[i]]);
mkElimClause(elimclauses, mkLit(v));
}else{
for (int i = 0; i < pos.size(); i++)
mkElimClause(elimclauses, v, ca[pos[i]]);
mkElimClause(elimclauses, ~mkLit(v));
}
for (int i = 0; i < cls.size(); i++)
removeClause(cls[i]);
// Produce clauses in cross product:
vec<Lit>& resolvent = add_tmp;
for (int i = 0; i < pos.size(); i++)
for (int j = 0; j < neg.size(); j++)
if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent))
return false;
// Free occurs list for this variable:
occurs[v].clear(true);
// Free watchers lists for this variable, if possible:
if (watches[ mkLit(v)].size() == 0) watches[ mkLit(v)].clear(true);
if (watches[~mkLit(v)].size() == 0) watches[~mkLit(v)].clear(true);
return backwardSubsumptionCheck();
}
bool SimpSolver::substitute(Var v, Lit x)
{
assert(!frozen[v]);
assert(!isEliminated(v));
assert(value(v) == l_Undef);
if (!ok) return false;
eliminated[v] = true;
setDecisionVar(v, false);
const vec<CRef>& cls = occurs.lookup(v);
vec<Lit>& subst_clause = add_tmp;
for (int i = 0; i < cls.size(); i++){
Clause& c = ca[cls[i]];
subst_clause.clear();
for (int j = 0; j < c.size(); j++){
Lit p = c[j];
subst_clause.push(var(p) == v ? x ^ sign(p) : p);
}
removeClause(cls[i]);
if (!addClause_(subst_clause))
return ok = false;
}
return true;
}
void SimpSolver::extendModel()
{
int i, j;
Lit x;
for (i = elimclauses.size()-1; i > 0; i -= j){
for (j = elimclauses[i--]; j > 1; j--, i--)
if (modelValue(toLit(elimclauses[i])) != l_False)
goto next;
x = toLit(elimclauses[i]);
model[var(x)] = lbool(!sign(x));
next:;
}
}
bool SimpSolver::eliminate(bool turn_off_elim)
{
if (!simplify())
return false;
else if (!use_simplification)
return true;
// Main simplification loop:
//
while (n_touched > 0 || bwdsub_assigns < trail.size() || elim_heap.size() > 0){
gatherTouchedClauses();
// printf(" ## (time = %6.2f s) BWD-SUB: queue = %d, trail = %d\n", cpuTime(), subsumption_queue.size(), trail.size() - bwdsub_assigns);
if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()) &&
!backwardSubsumptionCheck(true)){
ok = false; goto cleanup; }
// Empty elim_heap and return immediately on user-interrupt:
if (asynch_interrupt){
assert(bwdsub_assigns == trail.size());
assert(subsumption_queue.size() == 0);
assert(n_touched == 0);
elim_heap.clear();
goto cleanup; }
// printf(" ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size());
for (int cnt = 0; !elim_heap.empty(); cnt++){
Var elim = elim_heap.removeMin();
if (asynch_interrupt) break;
if (isEliminated(elim) || value(elim) != l_Undef) continue;
if (verbosity >= 2 && cnt % 100 == 0)
printf("elimination left: %10d\r", elim_heap.size());
if (use_asymm){
// Temporarily freeze variable. Otherwise, it would immediately end up on the queue again:
bool was_frozen = frozen[elim];
frozen[elim] = true;
if (!asymmVar(elim)){
ok = false; goto cleanup; }
frozen[elim] = was_frozen; }
// At this point, the variable may have been set by assymetric branching, so check it
// again. Also, don't eliminate frozen variables:
if (use_elim && value(elim) == l_Undef && !frozen[elim] && !eliminateVar(elim)){
ok = false; goto cleanup; }
checkGarbage(simp_garbage_frac);
}
assert(subsumption_queue.size() == 0);
}
cleanup:
// If no more simplification is needed, free all simplification-related data structures:
if (turn_off_elim){
touched .clear(true);
occurs .clear(true);
n_occ .clear(true);
elim_heap.clear(true);
subsumption_queue.clear(true);
use_simplification = false;
remove_satisfied = true;
ca.extra_clause_field = false;
// Force full cleanup (this is safe and desirable since it only happens once):
rebuildOrderHeap();
garbageCollect();
}else{
// Cheaper cleanup:
cleanUpClauses(); // TODO: can we make 'cleanUpClauses()' not be linear in the problem size somehow?
checkGarbage();
}
if (verbosity >= 1 && elimclauses.size() > 0)
printf("| Eliminated clauses: %10.2f Mb |\n",
double(elimclauses.size() * sizeof(uint32_t)) / (1024*1024));
return ok;
}
void SimpSolver::cleanUpClauses()
{
occurs.cleanAll();
int i,j;
for (i = j = 0; i < clauses.size(); i++)
if (ca[clauses[i]].mark() == 0)
clauses[j++] = clauses[i];
clauses.shrink(i - j);
}
//=================================================================================================
// Garbage Collection methods:
void SimpSolver::relocAll(ClauseAllocator& to)
{
if (!use_simplification) return;
// All occurs lists:
//
for (int i = 0; i < nVars(); i++){
vec<CRef>& cs = occurs[i];
for (int j = 0; j < cs.size(); j++)
ca.reloc(cs[j], to);
}
// Subsumption queue:
//
for (int i = 0; i < subsumption_queue.size(); i++)
ca.reloc(subsumption_queue[i], to);
// Temporary clause:
//
ca.reloc(bwdsub_tmpunit, to);
}
void SimpSolver::garbageCollect()
{
// Initialize the next region to a size corresponding to the estimated utilization degree. This
// is not precise but should avoid some unnecessary reallocations for the new region:
ClauseAllocator to(ca.size() - ca.wasted());
cleanUpClauses();
to.extra_clause_field = ca.extra_clause_field; // NOTE: this is important to keep (or lose) the extra fields.
relocAll(to);
Solver::relocAll(to);
if (verbosity >= 2)
printf("| Garbage collection: %12d bytes => %12d bytes |\n",
ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
to.moveTo(ca);
}

197
minisat/simp/SimpSolver.h Normal file
View File

@@ -0,0 +1,197 @@
/************************************************************************************[SimpSolver.h]
Copyright (c) 2006, Niklas Een, Niklas Sorensson
Copyright (c) 2007-2010, Niklas Sorensson
Permission is hereby granted, free of charge, to any person obtaining a copy of this software and
associated documentation files (the "Software"), to deal in the Software without restriction,
including without limitation the rights to use, copy, modify, merge, publish, distribute,
sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is
furnished to do so, subject to the following conditions:
The above copyright notice and this permission notice shall be included in all copies or
substantial portions of the Software.
THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT
NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/
#ifndef Minisat_SimpSolver_h
#define Minisat_SimpSolver_h
#include "mtl/Queue.h"
#include "core/Solver.h"
namespace Minisat {
//=================================================================================================
class SimpSolver : public Solver {
public:
// Constructor/Destructor:
//
SimpSolver();
~SimpSolver();
// Problem specification:
//
Var newVar (bool polarity = true, bool dvar = true);
bool addClause (const vec<Lit>& ps);
bool addEmptyClause(); // Add the empty clause to the solver.
bool addClause (Lit p); // Add a unit clause to the solver.
bool addClause (Lit p, Lit q); // Add a binary clause to the solver.
bool addClause (Lit p, Lit q, Lit r); // Add a ternary clause to the solver.
bool addClause_( vec<Lit>& ps);
bool substitute(Var v, Lit x); // Replace all occurences of v with x (may cause a contradiction).
// Variable mode:
//
void setFrozen (Var v, bool b); // If a variable is frozen it will not be eliminated.
bool isEliminated(Var v) const;
// Solving:
//
bool solve (const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);
lbool solveLimited(const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);
bool solve ( bool do_simp = true, bool turn_off_simp = false);
bool solve (Lit p , bool do_simp = true, bool turn_off_simp = false);
bool solve (Lit p, Lit q, bool do_simp = true, bool turn_off_simp = false);
bool solve (Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false);
bool eliminate (bool turn_off_elim = false); // Perform variable elimination based simplification.
// Memory managment:
//
virtual void garbageCollect();
// Generate a (possibly simplified) DIMACS file:
//
#if 0
void toDimacs (const char* file, const vec<Lit>& assumps);
void toDimacs (const char* file);
void toDimacs (const char* file, Lit p);
void toDimacs (const char* file, Lit p, Lit q);
void toDimacs (const char* file, Lit p, Lit q, Lit r);
#endif
// Mode of operation:
//
int grow; // Allow a variable elimination step to grow by a number of clauses (default to zero).
int clause_lim; // Variables are not eliminated if it produces a resolvent with a length above this limit.
// -1 means no limit.
int subsumption_lim; // Do not check if subsumption against a clause larger than this. -1 means no limit.
double simp_garbage_frac; // A different limit for when to issue a GC during simplification (Also see 'garbage_frac').
bool use_asymm; // Shrink clauses by asymmetric branching.
bool use_rcheck; // Check if a clause is already implied. Prett costly, and subsumes subsumptions :)
bool use_elim; // Perform variable elimination.
// Statistics:
//
int merges;
int asymm_lits;
int eliminated_vars;
protected:
// Helper structures:
//
struct ElimLt {
const vec<int>& n_occ;
explicit ElimLt(const vec<int>& no) : n_occ(no) {}
// TODO: are 64-bit operations here noticably bad on 32-bit platforms? Could use a saturating
// 32-bit implementation instead then, but this will have to do for now.
uint64_t cost (Var x) const { return (uint64_t)n_occ[toInt(mkLit(x))] * (uint64_t)n_occ[toInt(~mkLit(x))]; }
bool operator()(Var x, Var y) const { return cost(x) < cost(y); }
// TODO: investigate this order alternative more.
// bool operator()(Var x, Var y) const {
// int c_x = cost(x);
// int c_y = cost(y);
// return c_x < c_y || c_x == c_y && x < y; }
};
struct ClauseDeleted {
const ClauseAllocator& ca;
explicit ClauseDeleted(const ClauseAllocator& _ca) : ca(_ca) {}
bool operator()(const CRef& cr) const { return ca[cr].mark() == 1; } };
// Solver state:
//
int elimorder;
bool use_simplification;
vec<uint32_t> elimclauses;
vec<char> touched;
OccLists<Var, vec<CRef>, ClauseDeleted>
occurs;
vec<int> n_occ;
Heap<ElimLt> elim_heap;
Queue<CRef> subsumption_queue;
vec<char> frozen;
vec<char> eliminated;
int bwdsub_assigns;
int n_touched;
// Temporaries:
//
CRef bwdsub_tmpunit;
// Main internal methods:
//
lbool solve_ (bool do_simp = true, bool turn_off_simp = false);
bool asymm (Var v, CRef cr);
bool asymmVar (Var v);
void updateElimHeap (Var v);
void gatherTouchedClauses ();
bool merge (const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause);
bool merge (const Clause& _ps, const Clause& _qs, Var v, int& size);
bool backwardSubsumptionCheck (bool verbose = false);
bool eliminateVar (Var v);
void extendModel ();
void removeClause (CRef cr);
bool strengthenClause (CRef cr, Lit l);
void cleanUpClauses ();
bool implied (const vec<Lit>& c);
void relocAll (ClauseAllocator& to);
};
//=================================================================================================
// Implementation of inline methods:
inline bool SimpSolver::isEliminated (Var v) const { return eliminated[v]; }
inline void SimpSolver::updateElimHeap(Var v) {
assert(use_simplification);
// if (!frozen[v] && !isEliminated(v) && value(v) == l_Undef)
if (elim_heap.inHeap(v) || (!frozen[v] && !isEliminated(v) && value(v) == l_Undef))
elim_heap.update(v); }
inline bool SimpSolver::addClause (const vec<Lit>& ps) { ps.copyTo(add_tmp); return addClause_(add_tmp); }
inline bool SimpSolver::addEmptyClause() { add_tmp.clear(); return addClause_(add_tmp); }
inline bool SimpSolver::addClause (Lit p) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp); }
inline bool SimpSolver::addClause (Lit p, Lit q) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); }
inline bool SimpSolver::addClause (Lit p, Lit q, Lit r) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); }
inline void SimpSolver::setFrozen (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } }
inline bool SimpSolver::solve ( bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); return solve_(do_simp, turn_off_simp) == l_True; }
inline bool SimpSolver::solve (Lit p , bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); assumptions.push(p); return solve_(do_simp, turn_off_simp) == l_True; }
inline bool SimpSolver::solve (Lit p, Lit q, bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); return solve_(do_simp, turn_off_simp) == l_True; }
inline bool SimpSolver::solve (Lit p, Lit q, Lit r, bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_(do_simp, turn_off_simp) == l_True; }
inline bool SimpSolver::solve (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){
budgetOff(); assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp) == l_True; }
inline lbool SimpSolver::solveLimited (const vec<Lit>& assumps, bool do_simp, bool turn_off_simp){
assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp); }
//=================================================================================================
}
#endif