/****************************************************************************************[Solver.h]
MiniSat -- Copyright (c) 2003-2006, Niklas Een, 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 Solver_h
#define Solver_h
//#define COMPETITION
#include <cstdio>
#include <stdint.h>
struct SolverStats {
uint64_t starts, decisions, rnd_decisions, propagations, conflicts;
uint64_t clauses_literals, learnts_literals, max_literals, tot_literals;
uint64_t asymm_lits;
uint64_t remembered_clauses;
uint64_t subsumption_checks, subsumption_misses, merges;
SolverStats() :
starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0)
, clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0)
, asymm_lits (0)
, remembered_clauses(0)
, subsumption_checks(0), subsumption_misses(0), merges(0)
{ }
};
struct SearchParams {
double var_decay, clause_decay, random_var_freq;
double restart_inc, learntsize_inc, learntsize_factor;
int restart_first;
SearchParams(double v = 0.95, double c = 0.999, double r = 0.02,
double ri = 1.5, double li = 1.1, double lf = (double)1/(double)3,
int rf = 100) :
var_decay(1 / v), clause_decay(1 / c), random_var_freq(r),
restart_inc(ri), learntsize_inc(li), learntsize_factor(lf),
restart_first(rf) { }
};
//#include "AltVec.h"
#include "Vec.h"
//#define Vec_h
//#define vec altvec
#include "Alg.h"
#include "SolverTypes.h"
#include "VarOrder.h"
//=================================================================================================
// Local helpers:
static inline void logLit(FILE* f, Lit l)
{
fprintf(f, "%sx%d", sign(l) ? "~" : "", var(l)+1);
}
static inline void logLits(FILE* f, const vec<Lit>& ls)
{
fprintf(f, "[ ");
if (ls.size() > 0){
logLit(f, ls[0]);
for (int i = 1; i < ls.size(); i++){
fprintf(f, ", ");
logLit(f, ls[i]);
}
}
fprintf(f, "] ");
}
static inline const char* showBool(bool b) { return b ? "true" : "false"; }
//=================================================================================================
// Solver -- the main class:
class Solver {
struct ElimData {
int order; // 0 means not eliminated, >0 gives an index in the elimination order
vec<Clause*> eliminated;
ElimData() : order(0) {} };
struct ElimOrderLt {
const vec<ElimData>& elimtable;
ElimOrderLt(const vec<ElimData>& et) : elimtable(et) {}
bool operator()(Var x, Var y) { return elimtable[x].order > elimtable[y].order; } };
struct ElimLt {
const vec<int>& n_occ;
ElimLt(const vec<int>& no) : n_occ(no) {}
int cost (Var x) const { return n_occ[toInt(Lit(x))] * n_occ[toInt(~Lit(x))]; }
bool operator()(Var x, Var y) const { return cost(x) < cost(y); } };
protected:
// Solver state:
//
bool ok; // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used!
vec<Clause*> clauses; // List of problem clauses.
vec<Clause*> learnts; // List of learnt clauses.
double cla_inc; // Amount to bump next clause with.
vec<double> activity; // A heuristic measurement of the activity of a variable.
double var_inc; // Amount to bump next variable with.
VarOrder order; // Keeps track of the decision variable order.
vec<vec<Clause*> > watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
vec<char> assigns; // The current assignments (lbool:s stored as char:s).
vec<Lit> trail; // Assignment stack; stores all assigments made in the order they were made.
vec<int> trail_lim; // Separator indices for different decision levels in 'trail'.
vec<Clause*> reason; // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none.
vec<TrailPos> trailpos; // 'trailpos[var]' contains the position in the trail at wich the assigment was made.
int qhead; // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat).
int simpDB_assigns; // Number of top-level assignments since last execution of 'simplify()'.
int64_t simpDB_props; // Remaining number of propagations that must be made before next execution of 'simplify()'.
int elimorder;
bool subsumption; // Simplification related data structures
vec<ElimData> elimtable;
vec<char> touched;
vec<vec<Clause*> > occurs;
vec<int> n_occ;
Heap<ElimLt> heap;
vec<Clause*> subsumption_queue;
vec<Lit> assumptions; // Current set of assumptions provided to solve by the user.
FILE* logfile;
// Temporaries (to reduce allocation overhead). Each variable is prefixed by the method in which it is
// used, exept 'seen' wich is used in several places.
//
vec<char> seen;
vec<Lit> analyze_stack;
vec<Lit> analyze_toclear;
Clause* propagate_tmpempty;
Clause* propagate_tmpbin;
Clause* analyze_tmpbin;
Clause* bwdsub_tmpunit;
vec<Lit> add_tmp;
// Main internal methods:
//
bool assume (Lit p);
void cancelUntil (int level);
void record (const vec<Lit>& clause);
void analyze (Clause* confl, vec<Lit>& out_learnt, int& out_btlevel); // (bt = backtrack)
bool analyze_removable(Lit p, unsigned int min_level); // (helper method for 'analyze()')
void analyzeFinal (Lit p, vec<Lit>& out_conflict);
bool enqueue (Lit fact, Clause* from = NULL);
Clause* propagate ();
void reduceDB ();
Lit pickBranchLit ();
lbool search (int nof_conflicts, int nof_learnts);
double progressEstimate ();
bool asymm (Var v, Clause& c);
bool asymmVar (Var v);
// Variable properties:
void setVarProp (Var v, int prop, bool b) { order.setVarProp(v, prop, b); }
bool hasVarProp (Var v, int prop) const { return order.hasVarProp(v, prop); }
void updateHeap (Var v) {
if (elimtable[v].order == 0)
heap.update(v); }
// Simplification methods:
//
void cleanOcc (Var v){
assert(subsumption);
Clause **begin = (Clause**)occurs[v];
Clause **end = begin + occurs[v].size();
Clause **i, **j;
for (i = begin, j = end; i < j; i++)
if ((*i)->mark() == 1){
*i = *(--j);
i--;
}
//occurs[v].shrink_(end - j); // varför blir detta långsammare?
occurs[v].shrink(end - j);
}
vec<Clause*>& getOccurs (Var x) { cleanOcc(x); return occurs[x]; }
void gather (vec<Clause*>& clauses);
Lit subsumes (const Clause& c, const Clause& d) const;
bool merge (const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause);
bool merge (const Clause& _ps, const Clause& _qs, Var v);
bool backwardSubsumptionCheck (bool verbose = false);
bool eliminateVar (Var v, bool fail = false);
void remember (Var v);
bool eliminate ();
void extendModel ();
void verifyModel ();
void watchRelevant();
// Activity:
//
void varBumpActivity(Lit p) {
if ( (activity[var(p)] += var_inc) > 1e100 ) varRescaleActivity();
order.update(var(p)); }
void varDecayActivity () { var_inc *= params.var_decay; }
void varRescaleActivity();
void claDecayActivity () { cla_inc *= params.clause_decay; }
void claRescaleActivity();
// Operations on clauses:
//
bool newClause(const vec<Lit>& ps, bool learnt = false, bool normalized = false);
void claBumpActivity (Clause& c) { if ( (c.activity() += cla_inc) > 1e20 ) claRescaleActivity(); }
//bool locked (const Clause& c) const { return reason[var(c[0])] == &c; }
bool locked (const Clause& c) const { return reason[var(c[0])] == &c && value(c[0]) == l_True; }
bool satisfied (const Clause& c) const;
bool strengthen (Clause& c, Lit l);
void removeClause (Clause& c, bool dealloc = true);
int decisionLevel() const { return trail_lim.size(); }
public:
Solver(char* log = NULL) :
ok (true)
, cla_inc (1)
, var_inc (1)
, order (stats, assigns, activity)
, qhead (0)
, simpDB_assigns (-1)
, simpDB_props (0)
, elimorder (1)
, subsumption (true)
, heap (n_occ)
, logfile (NULL)
, params ()
, grow (0)
, expensive_ccmin (true)
, rnd_mode (rnd_anyheap)
, polarity_mode (polarity_false)
, asymm_mode (false)
, verbosity (0)
, progress_estimate(0)
{
vec<Lit> dummy(2,lit_Undef);
propagate_tmpbin = Clause_new(dummy);
analyze_tmpbin = Clause_new(dummy);
dummy.pop();
bwdsub_tmpunit = Clause_new(dummy);
dummy.pop();
propagate_tmpempty = Clause_new(dummy);
if (log != NULL){
logfile = fopen(log, "w");
if (logfile == NULL){
fprintf(stderr, "failed to open log-file: %s\n", log);
fprintf(stderr, "aborting\n");
exit(-1); }
}
}
~Solver() {
free(propagate_tmpbin);
free(analyze_tmpbin);
free(bwdsub_tmpunit);
free(propagate_tmpempty);
for (int i = 0; i < learnts.size(); i++) free(learnts[i]);
for (int i = 0; i < clauses.size(); i++) free(clauses[i]);
//for (int i = 0; i < nVars(); i++)
// NOTE: elimtable.size() might be lower than nVars() at the moment
for (int i = 0; i < elimtable.size(); i++)
for (int j = 0; j < elimtable[i].eliminated.size(); j++)
free(elimtable[i].eliminated[j]);
}
// Helpers: (semi-internal)
//
lbool value(Var x) const { return toLbool(assigns[x]); }
//lbool value(Lit p) const { return sign(p) ? ~toLbool(assigns[var(p)]) : toLbool(assigns[var(p)]); }
lbool value(Lit p) const { return toLbool(assigns[var(p)]) ^ sign(p); }
int nAssigns () { return trail.size(); }
int nClauses () { return clauses.size(); }
int nLearnts () { return learnts.size(); }
int nConflicts () { return (int)stats.conflicts; }
int nRemembered () { return (int)stats.remembered_clauses; }
int nVars () { return assigns.size(); }
// Statistics: (read-only member variable)
//
SolverStats stats;
// Mode of operation:
//
SearchParams params; // Restart frequency etc.
int grow; // Allow a simplification step to grow by a number of clauses (default to zero).
bool expensive_ccmin; // Controls conflict clause minimization. TRUE by default.
int rnd_mode;
int polarity_mode;
bool asymm_mode;
int verbosity; // Verbosity level. 0=silent, 1=some progress report, 2=everything
// Problem specification:
//
Var newVar (bool polarity = true, bool dvar = true);
bool addClause (const vec<Lit>& ps) { if (ok && (!newClause(ps) || propagate() != NULL )) ok = false; return ok; }
//bool addClause (const vec<Lit>& ps) { if (ok && (!newClause(ps))) ok = false; return ok; }
bool addClause (Lit x) { add_tmp.clear(); add_tmp.push(x); return addClause(add_tmp); }
bool addClause (Lit x, Lit y) { add_tmp.clear(); add_tmp.push(x); add_tmp.push(y); return addClause(add_tmp); }
bool addClause (Lit x, Lit y, Lit z) { add_tmp.clear(); add_tmp.push(x); add_tmp.push(y); add_tmp.push(z); return addClause(add_tmp); }
bool addClause (Lit x, Lit y, Lit z, Lit w) { add_tmp.clear(); add_tmp.push(x); add_tmp.push(y); add_tmp.push(z); add_tmp.push(w); return addClause(add_tmp); }
// Variable mode:
//
void freezeVar (Var v) {
setVarProp(v, p_frozen, true); }
void unfreezeVar (Var v) {
setVarProp(v, p_frozen, false); updateHeap(v); }
bool varElimed (Var v) { return elimtable[v].order > 0; }
void setPolarity (Var v, bool b) { setVarProp(v, p_polarity, b); }
void setDecisionVar (Var v, bool b) { setVarProp(v, p_decisionvar, b); }
bool hasSubsumption() { return subsumption; }
// Solving:
//
bool simplify (bool do_elimination = true, bool turn_off_subsumption = false);
bool okay () { return ok; } // FALSE means solver is in a conflicting state
bool solve (const vec<Lit>& assumps, bool simplify = true);
bool solve (bool simplify = true) { vec<Lit> tmp; return solve(tmp, simplify); }
bool solve (Lit l, bool simplify = true) { vec<Lit> tmp; tmp.push(l); return solve(tmp, simplify); }
double progress_estimate; // Set by 'search()'.
vec<lbool> model; // If problem is satisfiable, this vector contains the model (if any).
vec<Lit> conflict; // If problem is unsatisfiable (possibly under assumptions), this vector represent the conflict clause expressed in the assumptions.
// !!! VERY TEMPORARY !!!
bool& ok_ref() { return ok; }
vec<char>& assigns_ref() { return assigns; }
vec<Lit>& trail_ref() { return trail; }
inline void printLit(Lit l);
template<class C>
inline void printClause(const C& c);
};
#ifdef COMPETITION
#define reportf(format, args...) ( fprintf(stdout, "c " format, ## args), fflush(stdout) )
#else
#define reportf(format, args...) ( fflush(stdout), fprintf(stderr, format, ## args), fflush(stderr) )
#endif
//=================================================================================================
// Debug:
// Just like 'assert()' but expression will be evaluated in the release version as well.
static inline void check(bool expr) { assert(expr); }
inline void Solver::printLit(Lit l)
{
reportf("%s%d:%c", sign(l) ? "-" : "", var(l)+1, value(l) == l_True ? '1' : (value(l) == l_False ? '0' : 'X'));
}
template<class C>
inline void Solver::printClause(const C& c)
{
for (int i = 0; i < c.size(); i++){
printLit(c[i]);
fprintf(stderr, " ");
}
}
//=================================================================================================
#endif