minisat/0000755000177400017740000000000011165245507012442 5ustar boothbyboothbyminisat/core/0000755000177400017740000000000010536340026013363 5ustar boothbyboothbyminisat/core/Main.C0000644000177400017740000002607010525172425014364 0ustar boothbyboothby/******************************************************************************************[Main.C] 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. **************************************************************************************************/ #include #include #include #include #include #include #include "Solver.h" /*************************************************************************************/ #ifdef _MSC_VER #include static inline double cpuTime(void) { return (double)clock() / CLOCKS_PER_SEC; } #else #include #include #include static inline double cpuTime(void) { struct rusage ru; getrusage(RUSAGE_SELF, &ru); return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; } #endif #if defined(__linux__) static inline int memReadStat(int field) { char name[256]; pid_t pid = getpid(); sprintf(name, "/proc/%d/statm", pid); FILE* in = fopen(name, "rb"); if (in == NULL) return 0; int value; for (; field >= 0; field--) fscanf(in, "%d", &value); fclose(in); return value; } static inline uint64_t memUsed() { return (uint64_t)memReadStat(0) * (uint64_t)getpagesize(); } #elif defined(__FreeBSD__) static inline uint64_t memUsed(void) { struct rusage ru; getrusage(RUSAGE_SELF, &ru); return ru.ru_maxrss*1024; } #else static inline uint64_t memUsed() { return 0; } #endif #if defined(__linux__) #include #endif //================================================================================================= // DIMACS Parser: #define CHUNK_LIMIT 1048576 class StreamBuffer { gzFile in; char buf[CHUNK_LIMIT]; int pos; int size; void assureLookahead() { if (pos >= size) { pos = 0; size = gzread(in, buf, sizeof(buf)); } } public: StreamBuffer(gzFile i) : in(i), pos(0), size(0) { assureLookahead(); } int operator * () { return (pos >= size) ? EOF : buf[pos]; } void operator ++ () { pos++; assureLookahead(); } }; //- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - template static void skipWhitespace(B& in) { while ((*in >= 9 && *in <= 13) || *in == 32) ++in; } template static void skipLine(B& in) { for (;;){ if (*in == EOF || *in == '\0') return; if (*in == '\n') { ++in; return; } ++in; } } template static int parseInt(B& in) { int val = 0; bool neg = false; skipWhitespace(in); if (*in == '-') neg = true, ++in; else if (*in == '+') ++in; if (*in < '0' || *in > '9') reportf("PARSE ERROR! Unexpected char: %c\n", *in), exit(3); while (*in >= '0' && *in <= '9') val = val*10 + (*in - '0'), ++in; return neg ? -val : val; } template static void readClause(B& in, Solver& S, vec& lits) { int parsed_lit, var; lits.clear(); for (;;){ parsed_lit = parseInt(in); if (parsed_lit == 0) break; var = abs(parsed_lit)-1; while (var >= S.nVars()) S.newVar(); lits.push( (parsed_lit > 0) ? Lit(var) : ~Lit(var) ); } } template static bool match(B& in, char* str) { for (; *str != 0; ++str, ++in) if (*str != *in) return false; return true; } template static void parse_DIMACS_main(B& in, Solver& S) { vec lits; for (;;){ skipWhitespace(in); if (*in == EOF) break; else if (*in == 'p'){ if (match(in, "p cnf")){ int vars = parseInt(in); int clauses = parseInt(in); reportf("| Number of variables: %-12d |\n", vars); reportf("| Number of clauses: %-12d |\n", clauses); }else{ reportf("PARSE ERROR! Unexpected char: %c\n", *in), exit(3); } } else if (*in == 'c' || *in == 'p') skipLine(in); else readClause(in, S, lits), S.addClause(lits); } } // Inserts problem into solver. // static void parse_DIMACS(gzFile input_stream, Solver& S) { StreamBuffer in(input_stream); parse_DIMACS_main(in, S); } //================================================================================================= void printStats(Solver& solver) { double cpu_time = cpuTime(); uint64_t mem_used = memUsed(); reportf("restarts : %lld\n", solver.starts); reportf("conflicts : %-12lld (%.0f /sec)\n", solver.conflicts , solver.conflicts /cpu_time); reportf("decisions : %-12lld (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions /cpu_time); reportf("propagations : %-12lld (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time); reportf("conflict literals : %-12lld (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals); if (mem_used != 0) reportf("Memory used : %.2f MB\n", mem_used / 1048576.0); reportf("CPU time : %g s\n", cpu_time); } Solver* solver; static void SIGINT_handler(int signum) { reportf("\n"); reportf("*** INTERRUPTED ***\n"); printStats(*solver); reportf("\n"); reportf("*** INTERRUPTED ***\n"); exit(1); } //================================================================================================= // Main: void printUsage(char** argv) { reportf("USAGE: %s [options] \n\n where input may be either in plain or gzipped DIMACS.\n\n", argv[0]); reportf("OPTIONS:\n\n"); reportf(" -polarity-mode = {true,false,rnd}\n"); reportf(" -decay = [ 0 - 1 ]\n"); reportf(" -rnd-freq = [ 0 - 1 ]\n"); reportf(" -verbosity = {0,1,2}\n"); reportf("\n"); } const char* hasPrefix(const char* str, const char* prefix) { int len = strlen(prefix); if (strncmp(str, prefix, len) == 0) return str + len; else return NULL; } int main(int argc, char** argv) { Solver S; S.verbosity = 1; int i, j; const char* value; for (i = j = 0; i < argc; i++){ if ((value = hasPrefix(argv[i], "-polarity-mode="))){ if (strcmp(value, "true") == 0) S.polarity_mode = Solver::polarity_true; else if (strcmp(value, "false") == 0) S.polarity_mode = Solver::polarity_false; else if (strcmp(value, "rnd") == 0) S.polarity_mode = Solver::polarity_rnd; else{ reportf("ERROR! unknown polarity-mode %s\n", value); exit(0); } }else if ((value = hasPrefix(argv[i], "-rnd-freq="))){ double rnd; if (sscanf(value, "%lf", &rnd) <= 0 || rnd < 0 || rnd > 1){ reportf("ERROR! illegal rnd-freq constant %s\n", value); exit(0); } S.random_var_freq = rnd; }else if ((value = hasPrefix(argv[i], "-decay="))){ double decay; if (sscanf(value, "%lf", &decay) <= 0 || decay <= 0 || decay > 1){ reportf("ERROR! illegal decay constant %s\n", value); exit(0); } S.var_decay = 1 / decay; }else if ((value = hasPrefix(argv[i], "-verbosity="))){ int verbosity = (int)strtol(value, NULL, 10); if (verbosity == 0 && errno == EINVAL){ reportf("ERROR! illegal verbosity level %s\n", value); exit(0); } S.verbosity = verbosity; }else if (strcmp(argv[i], "-h") == 0 || strcmp(argv[i], "-help") == 0 || strcmp(argv[i], "--help") == 0){ printUsage(argv); exit(0); }else if (strncmp(argv[i], "-", 1) == 0){ reportf("ERROR! unknown flag %s\n", argv[i]); exit(0); }else argv[j++] = argv[i]; } argc = j; reportf("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); reportf("WARNING: for repeatability, setting FPU to use double precision\n"); #endif double cpu_time = cpuTime(); solver = &S; signal(SIGINT,SIGINT_handler); signal(SIGHUP,SIGINT_handler); if (argc == 1) reportf("Reading from standard input... Use '-h' or '--help' for help.\n"); gzFile in = (argc == 1) ? gzdopen(0, "rb") : gzopen(argv[1], "rb"); if (in == NULL) reportf("ERROR! Could not open file: %s\n", argc == 1 ? "" : argv[1]), exit(1); reportf("============================[ Problem Statistics ]=============================\n"); reportf("| |\n"); parse_DIMACS(in, S); gzclose(in); FILE* res = (argc >= 3) ? fopen(argv[2], "wb") : NULL; double parse_time = cpuTime() - cpu_time; reportf("| Parsing time: %-12.2f s |\n", parse_time); if (!S.simplify()){ reportf("Solved by unit propagation\n"); if (res != NULL) fprintf(res, "UNSAT\n"), fclose(res); printf("UNSATISFIABLE\n"); exit(20); } bool ret = S.solve(); printStats(S); reportf("\n"); printf(ret ? "SATISFIABLE\n" : "UNSATISFIABLE\n"); if (res != NULL){ if (ret){ 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 fprintf(res, "UNSAT\n"); fclose(res); } #ifdef NDEBUG exit(ret ? 10 : 20); // (faster than "return", which will invoke the destructor for 'Solver') #endif } minisat/core/Solver.h0000644000177400017740000003767710525172425015036 0ustar boothbyboothby/****************************************************************************************[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 #include #include "Vec.h" #include "Heap.h" #include "Alg.h" #include "SolverTypes.h" //================================================================================================= // Solver -- the main class: class Solver { public: // Constructor/Destructor: // Solver(); ~Solver(); // Problem specification: // Var newVar (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode. bool addClause (vec& ps); // Add a clause to the solver. NOTE! 'ps' may be shrunk by this method! // Solving: // bool simplify (); // Removes already satisfied clauses. bool solve (const vec& assumps); // Search for a model that respects a given set of assumptions. bool solve (); // Search without assumptions. bool okay () const; // FALSE means solver is in a conflicting state // Variable mode: // void setPolarity (Var v, bool b); // Declare which polarity the decision heuristic should use for a variable. Requires mode 'polarity_user'. void setDecisionVar (Var v, bool b); // Declare if a variable should be eligible for selection in the decision heuristic. // Read state: // lbool value (Var x) const; // The current value of a variable. lbool value (Lit p) const; // The current value of a literal. lbool modelValue (Lit p) const; // The value of a literal in the last model. The last call to solve must have been satisfiable. int nAssigns () const; // The current number of assigned literals. int nClauses () const; // The current number of original clauses. int nLearnts () const; // The current number of learnt clauses. int nVars () const; // The current number of variables. // Extra results: (read-only member variable) // vec model; // If problem is satisfiable, this vector contains the model (if any). vec conflict; // If problem is unsatisfiable (possibly under assumptions), // this vector represent the final conflict clause expressed in the assumptions. // Mode of operation: // double var_decay; // Inverse of the variable activity decay factor. (default 1 / 0.95) double clause_decay; // Inverse of the clause activity decay factor. (1 / 0.999) double random_var_freq; // The frequency with which the decision heuristic tries to choose a random variable. (default 0.02) int restart_first; // The initial restart limit. (default 100) double restart_inc; // The factor with which the restart limit is multiplied in each restart. (default 1.5) double learntsize_factor; // The intitial limit for learnt clauses is a factor of the original clauses. (default 1 / 3) double learntsize_inc; // The limit for learnt clauses is multiplied with this factor each restart. (default 1.1) bool expensive_ccmin; // Controls conflict clause minimization. (default TRUE) int polarity_mode; // Controls which polarity the decision heuristic chooses. See enum below for allowed modes. (default polarity_false) int verbosity; // Verbosity level. 0=silent, 1=some progress report (default 0) enum { polarity_true = 0, polarity_false = 1, polarity_user = 2, polarity_rnd = 3 }; // Statistics: (read-only member variable) // uint64_t starts, decisions, rnd_decisions, propagations, conflicts; uint64_t clauses_literals, learnts_literals, max_literals, tot_literals; protected: // Helper structures: // struct VarOrderLt { const vec& activity; bool operator () (Var x, Var y) const { return activity[x] > activity[y]; } VarOrderLt(const vec& act) : activity(act) { } }; friend class VarFilter; struct VarFilter { const Solver& s; VarFilter(const Solver& _s) : s(_s) {} bool operator()(Var v) const { return toLbool(s.assigns[v]) == l_Undef && s.decision_var[v]; } }; // Solver state: // bool ok; // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used! vec clauses; // List of problem clauses. vec learnts; // List of learnt clauses. double cla_inc; // Amount to bump next clause with. vec activity; // A heuristic measurement of the activity of a variable. double var_inc; // Amount to bump next variable with. vec > watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true). vec assigns; // The current assignments (lbool:s stored as char:s). vec polarity; // The preferred polarity of each variable. vec decision_var; // Declares if a variable is eligible for selection in the decision heuristic. vec trail; // Assignment stack; stores all assigments made in the order they were made. vec trail_lim; // Separator indices for different decision levels in 'trail'. vec reason; // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none. vec level; // 'level[var]' contains the level at which the assignment 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()'. vec assumptions; // Current set of assumptions provided to solve by the user. Heap order_heap; // A priority queue of variables ordered with respect to the variable activity. double random_seed; // Used by the random variable selection. double progress_estimate;// Set by 'search()'. bool remove_satisfied; // Indicates whether possibly inefficient linear scan for satisfied clauses should be performed in 'simplify'. // 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 seen; vec analyze_stack; vec analyze_toclear; vec add_tmp; // Main internal methods: // void insertVarOrder (Var x); // Insert a variable in the decision order priority queue. Lit pickBranchLit (int polarity_mode, double random_var_freq); // Return the next decision variable. void newDecisionLevel (); // Begins a new decision level. void uncheckedEnqueue (Lit p, Clause* from = NULL); // Enqueue a literal. Assumes value of literal is undefined. bool enqueue (Lit p, Clause* from = NULL); // Test if fact 'p' contradicts current state, enqueue otherwise. Clause* propagate (); // Perform unit propagation. Returns possibly conflicting clause. void cancelUntil (int level); // Backtrack until a certain level. void analyze (Clause* confl, vec& out_learnt, int& out_btlevel); // (bt = backtrack) void analyzeFinal (Lit p, vec& out_conflict); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION? bool litRedundant (Lit p, uint32_t abstract_levels); // (helper method for 'analyze()') lbool search (int nof_conflicts, int nof_learnts); // Search for a given number of conflicts. void reduceDB (); // Reduce the set of learnt clauses. void removeSatisfied (vec& cs); // Shrink 'cs' to contain only non-satisfied clauses. // Maintaining Variable/Clause activity: // void varDecayActivity (); // Decay all variables with the specified factor. Implemented by increasing the 'bump' value instead. void varBumpActivity (Var v); // Increase a variable with the current 'bump' value. void claDecayActivity (); // Decay all clauses with the specified factor. Implemented by increasing the 'bump' value instead. void claBumpActivity (Clause& c); // Increase a clause with the current 'bump' value. // Operations on clauses: // void attachClause (Clause& c); // Attach a clause to watcher lists. void detachClause (Clause& c); // Detach a clause to watcher lists. void removeClause (Clause& c); // Detach and free a clause. bool locked (const Clause& c) const; // Returns TRUE if a clause is a reason for some implication in the current state. bool satisfied (const Clause& c) const; // Returns TRUE if a clause is satisfied in the current state. // Misc: // int decisionLevel () const; // Gives the current decisionlevel. uint32_t abstractLevel (Var x) const; // Used to represent an abstraction of sets of decision levels. double progressEstimate () const; // DELETE THIS ?? IT'S NOT VERY USEFUL ... // Debug: void printLit (Lit l); template void printClause (const C& c); void verifyModel (); void checkLiteralCount(); // Static helpers: // // Returns a random float 0 <= x < 1. Seed must never be 0. static inline double drand(double& seed) { seed *= 1389796; int q = (int)(seed / 2147483647); seed -= (double)q * 2147483647; return seed / 2147483647; } // Returns a random integer 0 <= x < size. Seed must never be 0. static inline int irand(double& seed, int size) { return (int)(drand(seed) * size); } }; //================================================================================================= // Implementation of inline methods: inline void Solver::insertVarOrder(Var x) { if (!order_heap.inHeap(x) && decision_var[x]) order_heap.insert(x); } inline void Solver::varDecayActivity() { var_inc *= var_decay; } inline void Solver::varBumpActivity(Var v) { if ( (activity[v] += var_inc) > 1e100 ) { // Rescale: for (int i = 0; i < nVars(); i++) activity[i] *= 1e-100; var_inc *= 1e-100; } // Update order_heap with respect to new activity: if (order_heap.inHeap(v)) order_heap.decrease(v); } inline void Solver::claDecayActivity() { cla_inc *= clause_decay; } inline void Solver::claBumpActivity (Clause& c) { if ( (c.activity() += cla_inc) > 1e20 ) { // Rescale: for (int i = 0; i < learnts.size(); i++) learnts[i]->activity() *= 1e-20; cla_inc *= 1e-20; } } inline bool Solver::enqueue (Lit p, Clause* from) { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); } inline bool Solver::locked (const Clause& c) const { return reason[var(c[0])] == &c && value(c[0]) == l_True; } inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); } inline int Solver::decisionLevel () const { return trail_lim.size(); } inline uint32_t Solver::abstractLevel (Var x) const { return 1 << (level[x] & 31); } inline lbool Solver::value (Var x) const { return toLbool(assigns[x]); } inline lbool Solver::value (Lit p) const { return toLbool(assigns[var(p)]) ^ sign(p); } inline lbool Solver::modelValue (Lit p) const { return model[var(p)] ^ sign(p); } inline int Solver::nAssigns () const { return trail.size(); } inline int Solver::nClauses () const { return clauses.size(); } inline int Solver::nLearnts () const { return learnts.size(); } inline int Solver::nVars () const { return assigns.size(); } inline void Solver::setPolarity (Var v, bool b) { polarity [v] = (char)b; } inline void Solver::setDecisionVar(Var v, bool b) { decision_var[v] = (char)b; if (b) { insertVarOrder(v); } } inline bool Solver::solve () { vec tmp; return solve(tmp); } inline bool Solver::okay () const { return ok; } //================================================================================================= // Debug + etc: #define reportf(format, args...) ( fflush(stdout), fprintf(stderr, format, ## args), fflush(stderr) ) 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& 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"; } // 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 inline void Solver::printClause(const C& c) { for (int i = 0; i < c.size(); i++){ printLit(c[i]); fprintf(stderr, " "); } } //================================================================================================= #endif minisat/core/Makefile0000644000177400017740000000026511165245204015027 0ustar boothbyboothbyMTL = ../mtl CHDRS = $(wildcard *.h) $(wildcard $(MTL)/*.h) EXEC = minisat CFLAGS = -I$(MTL) -Wall -ffloat-store -fPIC LFLAGS = -lz include ../mtl/template.mk minisat/core/SolverTypes.h0000644000177400017740000001705010525172426016043 0ustar boothbyboothby/***********************************************************************************[SolverTypes.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 SolverTypes_h #define SolverTypes_h #include #include //================================================================================================= // Variables, literals, lifted booleans, clauses: // NOTE! Variables are just integers. No abstraction here. They should be chosen from 0..N, // so that they can be used as array indices. typedef int Var; #define var_Undef (-1) class Lit { int x; public: Lit() : x(2*var_Undef) { } // (lit_Undef) explicit Lit(Var var, bool sign = false) : x((var+var) + (int)sign) { } // Don't use these for constructing/deconstructing literals. Use the normal constructors instead. friend int toInt (Lit p); // Guarantees small, positive integers suitable for array indexing. friend Lit toLit (int i); // Inverse of 'toInt()' friend Lit operator ~(Lit p); friend bool sign (Lit p); friend int var (Lit p); friend Lit unsign (Lit p); friend Lit id (Lit p, bool sgn); bool operator == (Lit p) const { return x == p.x; } bool operator != (Lit p) const { return x != p.x; } bool operator < (Lit p) const { return x < p.x; } // '<' guarantees that p, ~p are adjacent in the ordering. }; inline int toInt (Lit p) { return p.x; } inline Lit toLit (int i) { Lit p; p.x = i; return p; } inline Lit operator ~(Lit p) { Lit q; q.x = p.x ^ 1; return q; } inline bool sign (Lit p) { return p.x & 1; } inline int var (Lit p) { return p.x >> 1; } inline Lit unsign (Lit p) { Lit q; q.x = p.x & ~1; return q; } inline Lit id (Lit p, bool sgn) { Lit q; q.x = p.x ^ (int)sgn; return q; } const Lit lit_Undef(var_Undef, false); // }- Useful special constants. const Lit lit_Error(var_Undef, true ); // } //================================================================================================= // Lifted booleans: class lbool { char value; explicit lbool(int v) : value(v) { } public: lbool() : value(0) { } lbool(bool x) : value((int)x*2-1) { } int toInt(void) const { return value; } bool operator == (lbool b) const { return value == b.value; } bool operator != (lbool b) const { return value != b.value; } lbool operator ^ (bool b) const { return b ? lbool(-value) : lbool(value); } friend int toInt (lbool l); friend lbool toLbool(int v); }; inline int toInt (lbool l) { return l.toInt(); } inline lbool toLbool(int v) { return lbool(v); } const lbool l_True = toLbool( 1); const lbool l_False = toLbool(-1); const lbool l_Undef = toLbool( 0); //================================================================================================= // Clause -- a simple class for representing a clause: class Clause { uint32_t size_etc; union { float act; uint32_t abst; } extra; Lit data[0]; public: void calcAbstraction() { uint32_t abstraction = 0; for (int i = 0; i < size(); i++) abstraction |= 1 << (var(data[i]) & 31); extra.abst = abstraction; } // NOTE: This constructor cannot be used directly (doesn't allocate enough memory). template Clause(const V& ps, bool learnt) { size_etc = (ps.size() << 3) | (uint32_t)learnt; for (int i = 0; i < ps.size(); i++) data[i] = ps[i]; if (learnt) extra.act = 0; else calcAbstraction(); } // -- use this function instead: template friend Clause* Clause_new(const V& ps, bool learnt = false) { assert(sizeof(Lit) == sizeof(uint32_t)); assert(sizeof(float) == sizeof(uint32_t)); void* mem = malloc(sizeof(Clause) + sizeof(uint32_t)*(ps.size())); return new (mem) Clause(ps, learnt); } int size () const { return size_etc >> 3; } void shrink (int i) { assert(i <= size()); size_etc = (((size_etc >> 3) - i) << 3) | (size_etc & 7); } void pop () { shrink(1); } bool learnt () const { return size_etc & 1; } uint32_t mark () const { return (size_etc >> 1) & 3; } void mark (uint32_t m) { size_etc = (size_etc & ~6) | ((m & 3) << 1); } const Lit& last () const { return data[size()-1]; } // NOTE: somewhat unsafe to change the clause in-place! Must manually call 'calcAbstraction' afterwards for // subsumption operations to behave correctly. Lit& operator [] (int i) { return data[i]; } Lit operator [] (int i) const { return data[i]; } operator const Lit* (void) const { return data; } float& activity () { return extra.act; } uint32_t abstraction () const { return extra.abst; } Lit subsumes (const Clause& other) const; void strengthen (Lit p); }; /*_________________________________________________________________________________________________ | | subsumes : (other : const Clause&) -> Lit | | Description: | Checks if clause subsumes 'other', and at the same time, if it can be used to simplify 'other' | by subsumption resolution. | | Result: | lit_Error - No subsumption or simplification | lit_Undef - Clause subsumes 'other' | p - The literal p can be deleted from 'other' |________________________________________________________________________________________________@*/ inline Lit Clause::subsumes(const Clause& other) const { if (other.size() < size() || (extra.abst & ~other.extra.abst) != 0) return lit_Error; Lit ret = lit_Undef; const Lit* c = (const Lit*)(*this); const Lit* d = (const Lit*)other; for (int i = 0; i < size(); i++) { // search for c[i] or ~c[i] for (int j = 0; j < other.size(); j++) if (c[i] == d[j]) goto ok; else if (ret == lit_Undef && c[i] == ~d[j]){ ret = c[i]; goto ok; } // did not find it return lit_Error; ok:; } return ret; } inline void Clause::strengthen(Lit p) { remove(*this, p); calcAbstraction(); } #endif minisat/core/Solver.C0000644000177400017740000005670110536337764014771 0ustar boothbyboothby/****************************************************************************************[Solver.C] 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. **************************************************************************************************/ #include "Solver.h" #include "Sort.h" #include //================================================================================================= // Constructor/Destructor: Solver::Solver() : // Parameters: (formerly in 'SearchParams') var_decay(1 / 0.95), clause_decay(1 / 0.999), random_var_freq(0.02) , restart_first(100), restart_inc(1.5), learntsize_factor((double)1/(double)3), learntsize_inc(1.1) // More parameters: // , expensive_ccmin (true) , polarity_mode (polarity_false) , verbosity (0) // Statistics: (formerly in 'SolverStats') // , starts(0), decisions(0), rnd_decisions(0), propagations(0), conflicts(0) , clauses_literals(0), learnts_literals(0), max_literals(0), tot_literals(0) , ok (true) , cla_inc (1) , var_inc (1) , qhead (0) , simpDB_assigns (-1) , simpDB_props (0) , order_heap (VarOrderLt(activity)) , random_seed (91648253) , progress_estimate(0) , remove_satisfied (true) {} Solver::~Solver() { for (int i = 0; i < learnts.size(); i++) free(learnts[i]); for (int i = 0; i < clauses.size(); i++) free(clauses[i]); } //================================================================================================= // Minor methods: // Creates a new SAT variable in the solver. If 'decision_var' is cleared, variable will not be // used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result). // Var Solver::newVar(bool sign, bool dvar) { int v = nVars(); watches .push(); // (list for positive literal) watches .push(); // (list for negative literal) reason .push(NULL); assigns .push(toInt(l_Undef)); level .push(-1); activity .push(0); seen .push(0); polarity .push((char)sign); decision_var.push((char)dvar); insertVarOrder(v); return v; } bool Solver::addClause(vec& ps) { assert(decisionLevel() == 0); if (!ok) return false; else{ // Check if clause is satisfied and remove false/duplicate literals: sort(ps); Lit p; int i, j; for (i = j = 0, p = lit_Undef; i < ps.size(); i++) if (value(ps[i]) == l_True || ps[i] == ~p) return true; else if (value(ps[i]) != l_False && ps[i] != p) ps[j++] = p = ps[i]; ps.shrink(i - j); } if (ps.size() == 0) return ok = false; else if (ps.size() == 1){ assert(value(ps[0]) == l_Undef); uncheckedEnqueue(ps[0]); return ok = (propagate() == NULL); }else{ Clause* c = Clause_new(ps, false); clauses.push(c); attachClause(*c); } return true; } void Solver::attachClause(Clause& c) { assert(c.size() > 1); watches[toInt(~c[0])].push(&c); watches[toInt(~c[1])].push(&c); if (c.learnt()) learnts_literals += c.size(); else clauses_literals += c.size(); } void Solver::detachClause(Clause& c) { assert(c.size() > 1); assert(find(watches[toInt(~c[0])], &c)); assert(find(watches[toInt(~c[1])], &c)); remove(watches[toInt(~c[0])], &c); remove(watches[toInt(~c[1])], &c); if (c.learnt()) learnts_literals -= c.size(); else clauses_literals -= c.size(); } void Solver::removeClause(Clause& c) { detachClause(c); free(&c); } bool Solver::satisfied(const Clause& c) const { for (int i = 0; i < c.size(); i++) if (value(c[i]) == l_True) return true; return false; } // Revert to the state at given level (keeping all assignment at 'level' but not beyond). // void Solver::cancelUntil(int level) { if (decisionLevel() > level){ for (int c = trail.size()-1; c >= trail_lim[level]; c--){ Var x = var(trail[c]); assigns[x] = toInt(l_Undef); insertVarOrder(x); } qhead = trail_lim[level]; trail.shrink(trail.size() - trail_lim[level]); trail_lim.shrink(trail_lim.size() - level); } } //================================================================================================= // Major methods: Lit Solver::pickBranchLit(int polarity_mode, double random_var_freq) { Var next = var_Undef; // Random decision: if (drand(random_seed) < random_var_freq && !order_heap.empty()){ next = order_heap[irand(random_seed,order_heap.size())]; if (toLbool(assigns[next]) == l_Undef && decision_var[next]) rnd_decisions++; } // Activity based decision: while (next == var_Undef || toLbool(assigns[next]) != l_Undef || !decision_var[next]) if (order_heap.empty()){ next = var_Undef; break; }else next = order_heap.removeMin(); bool sign = false; switch (polarity_mode){ case polarity_true: sign = false; break; case polarity_false: sign = true; break; case polarity_user: sign = polarity[next]; break; case polarity_rnd: sign = irand(random_seed, 2); break; default: assert(false); } return next == var_Undef ? lit_Undef : Lit(next, sign); } /*_________________________________________________________________________________________________ | | analyze : (confl : Clause*) (out_learnt : vec&) (out_btlevel : int&) -> [void] | | Description: | Analyze conflict and produce a reason clause. | | Pre-conditions: | * 'out_learnt' is assumed to be cleared. | * Current decision level must be greater than root level. | | Post-conditions: | * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'. | | Effect: | Will undo part of the trail, upto but not beyond the assumption of the current decision level. |________________________________________________________________________________________________@*/ void Solver::analyze(Clause* confl, vec& out_learnt, int& out_btlevel) { int pathC = 0; Lit p = lit_Undef; // Generate conflict clause: // out_learnt.push(); // (leave room for the asserting literal) int index = trail.size() - 1; out_btlevel = 0; do{ assert(confl != NULL); // (otherwise should be UIP) Clause& c = *confl; if (c.learnt()) claBumpActivity(c); for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){ Lit q = c[j]; if (!seen[var(q)] && level[var(q)] > 0){ varBumpActivity(var(q)); seen[var(q)] = 1; if (level[var(q)] >= decisionLevel()) pathC++; else{ out_learnt.push(q); if (level[var(q)] > out_btlevel) out_btlevel = level[var(q)]; } } } // Select next clause to look at: while (!seen[var(trail[index--])]); p = trail[index+1]; confl = reason[var(p)]; seen[var(p)] = 0; pathC--; }while (pathC > 0); out_learnt[0] = ~p; // Simplify conflict clause: // int i, j; if (expensive_ccmin){ uint32_t abstract_level = 0; for (i = 1; i < out_learnt.size(); i++) abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involved in conflict) out_learnt.copyTo(analyze_toclear); for (i = j = 1; i < out_learnt.size(); i++) if (reason[var(out_learnt[i])] == NULL || !litRedundant(out_learnt[i], abstract_level)) out_learnt[j++] = out_learnt[i]; }else{ out_learnt.copyTo(analyze_toclear); for (i = j = 1; i < out_learnt.size(); i++){ Clause& c = *reason[var(out_learnt[i])]; for (int k = 1; k < c.size(); k++) if (!seen[var(c[k])] && level[var(c[k])] > 0){ out_learnt[j++] = out_learnt[i]; break; } } } max_literals += out_learnt.size(); out_learnt.shrink(i - j); tot_literals += out_learnt.size(); // Find correct backtrack level: // if (out_learnt.size() == 1) out_btlevel = 0; else{ int max_i = 1; for (int i = 2; i < out_learnt.size(); i++) if (level[var(out_learnt[i])] > level[var(out_learnt[max_i])]) max_i = i; Lit p = out_learnt[max_i]; out_learnt[max_i] = out_learnt[1]; out_learnt[1] = p; out_btlevel = level[var(p)]; } for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0; // ('seen[]' is now cleared) } // Check if 'p' can be removed. 'abstract_levels' is used to abort early if the algorithm is // visiting literals at levels that cannot be removed later. bool Solver::litRedundant(Lit p, uint32_t abstract_levels) { analyze_stack.clear(); analyze_stack.push(p); int top = analyze_toclear.size(); while (analyze_stack.size() > 0){ assert(reason[var(analyze_stack.last())] != NULL); Clause& c = *reason[var(analyze_stack.last())]; analyze_stack.pop(); for (int i = 1; i < c.size(); i++){ Lit p = c[i]; if (!seen[var(p)] && level[var(p)] > 0){ if (reason[var(p)] != NULL && (abstractLevel(var(p)) & abstract_levels) != 0){ seen[var(p)] = 1; analyze_stack.push(p); analyze_toclear.push(p); }else{ for (int j = top; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0; analyze_toclear.shrink(analyze_toclear.size() - top); return false; } } } } return true; } /*_________________________________________________________________________________________________ | | analyzeFinal : (p : Lit) -> [void] | | Description: | Specialized analysis procedure to express the final conflict in terms of assumptions. | Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and | stores the result in 'out_conflict'. |________________________________________________________________________________________________@*/ void Solver::analyzeFinal(Lit p, vec& out_conflict) { out_conflict.clear(); out_conflict.push(p); if (decisionLevel() == 0) return; seen[var(p)] = 1; for (int i = trail.size()-1; i >= trail_lim[0]; i--){ Var x = var(trail[i]); if (seen[x]){ if (reason[x] == NULL){ assert(level[x] > 0); out_conflict.push(~trail[i]); }else{ Clause& c = *reason[x]; for (int j = 1; j < c.size(); j++) if (level[var(c[j])] > 0) seen[var(c[j])] = 1; } seen[x] = 0; } } seen[var(p)] = 0; } void Solver::uncheckedEnqueue(Lit p, Clause* from) { assert(value(p) == l_Undef); assigns [var(p)] = toInt(lbool(!sign(p))); // <<== abstract but not uttermost effecient level [var(p)] = decisionLevel(); reason [var(p)] = from; trail.push(p); } /*_________________________________________________________________________________________________ | | propagate : [void] -> [Clause*] | | Description: | Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned, | otherwise NULL. | | Post-conditions: | * the propagation queue is empty, even if there was a conflict. |________________________________________________________________________________________________@*/ Clause* Solver::propagate() { Clause* confl = NULL; int num_props = 0; while (qhead < trail.size()){ Lit p = trail[qhead++]; // 'p' is enqueued fact to propagate. vec& ws = watches[toInt(p)]; Clause **i, **j, **end; num_props++; for (i = j = (Clause**)ws, end = i + ws.size(); i != end;){ Clause& c = **i++; // Make sure the false literal is data[1]: Lit false_lit = ~p; if (c[0] == false_lit) c[0] = c[1], c[1] = false_lit; assert(c[1] == false_lit); // If 0th watch is true, then clause is already satisfied. Lit first = c[0]; if (value(first) == l_True){ *j++ = &c; }else{ // Look for new watch: for (int k = 2; k < c.size(); k++) if (value(c[k]) != l_False){ c[1] = c[k]; c[k] = false_lit; watches[toInt(~c[1])].push(&c); goto FoundWatch; } // Did not find watch -- clause is unit under assignment: *j++ = &c; if (value(first) == l_False){ confl = &c; qhead = trail.size(); // Copy the remaining watches: while (i < end) *j++ = *i++; }else uncheckedEnqueue(first, &c); } FoundWatch:; } ws.shrink(i - j); } propagations += num_props; simpDB_props -= num_props; return confl; } /*_________________________________________________________________________________________________ | | reduceDB : () -> [void] | | Description: | Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked | clauses are clauses that are reason to some assignment. Binary clauses are never removed. |________________________________________________________________________________________________@*/ struct reduceDB_lt { bool operator () (Clause* x, Clause* y) { return x->size() > 2 && (y->size() == 2 || x->activity() < y->activity()); } }; void Solver::reduceDB() { int i, j; double extra_lim = cla_inc / learnts.size(); // Remove any clause below this activity sort(learnts, reduceDB_lt()); for (i = j = 0; i < learnts.size() / 2; i++){ if (learnts[i]->size() > 2 && !locked(*learnts[i])) removeClause(*learnts[i]); else learnts[j++] = learnts[i]; } for (; i < learnts.size(); i++){ if (learnts[i]->size() > 2 && !locked(*learnts[i]) && learnts[i]->activity() < extra_lim) removeClause(*learnts[i]); else learnts[j++] = learnts[i]; } learnts.shrink(i - j); } void Solver::removeSatisfied(vec& cs) { int i,j; for (i = j = 0; i < cs.size(); i++){ if (satisfied(*cs[i])) removeClause(*cs[i]); else cs[j++] = cs[i]; } cs.shrink(i - j); } /*_________________________________________________________________________________________________ | | simplify : [void] -> [bool] | | Description: | Simplify the clause database according to the current top-level assigment. Currently, the only | thing done here is the removal of satisfied clauses, but more things can be put here. |________________________________________________________________________________________________@*/ bool Solver::simplify() { assert(decisionLevel() == 0); if (!ok || propagate() != NULL) return ok = false; if (nAssigns() == simpDB_assigns || (simpDB_props > 0)) return true; // Remove satisfied clauses: removeSatisfied(learnts); if (remove_satisfied) // Can be turned off. removeSatisfied(clauses); // Remove fixed variables from the variable heap: order_heap.filter(VarFilter(*this)); simpDB_assigns = nAssigns(); simpDB_props = clauses_literals + learnts_literals; // (shouldn't depend on stats really, but it will do for now) return true; } /*_________________________________________________________________________________________________ | | search : (nof_conflicts : int) (nof_learnts : int) (params : const SearchParams&) -> [lbool] | | Description: | Search for a model the specified number of conflicts, keeping the number of learnt clauses | below the provided limit. NOTE! Use negative value for 'nof_conflicts' or 'nof_learnts' to | indicate infinity. | | Output: | 'l_True' if a partial assigment that is consistent with respect to the clauseset is found. If | all variables are decision variables, this means that the clause set is satisfiable. 'l_False' | if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached. |________________________________________________________________________________________________@*/ lbool Solver::search(int nof_conflicts, int nof_learnts) { assert(ok); int backtrack_level; int conflictC = 0; vec learnt_clause; starts++; bool first = true; for (;;){ Clause* confl = propagate(); if (confl != NULL){ // CONFLICT conflicts++; conflictC++; if (decisionLevel() == 0) return l_False; first = false; learnt_clause.clear(); analyze(confl, learnt_clause, backtrack_level); cancelUntil(backtrack_level); assert(value(learnt_clause[0]) == l_Undef); if (learnt_clause.size() == 1){ uncheckedEnqueue(learnt_clause[0]); }else{ Clause* c = Clause_new(learnt_clause, true); learnts.push(c); attachClause(*c); claBumpActivity(*c); uncheckedEnqueue(learnt_clause[0], c); } varDecayActivity(); claDecayActivity(); }else{ // NO CONFLICT if (nof_conflicts >= 0 && conflictC >= nof_conflicts){ // Reached bound on number of conflicts: progress_estimate = progressEstimate(); cancelUntil(0); return l_Undef; } // Simplify the set of problem clauses: if (decisionLevel() == 0 && !simplify()) return l_False; if (nof_learnts >= 0 && learnts.size()-nAssigns() >= nof_learnts) // Reduce the set of learnt clauses: reduceDB(); Lit next = lit_Undef; while (decisionLevel() < assumptions.size()){ // Perform user provided assumption: Lit p = assumptions[decisionLevel()]; if (value(p) == l_True){ // Dummy decision level: newDecisionLevel(); }else if (value(p) == l_False){ analyzeFinal(~p, conflict); return l_False; }else{ next = p; break; } } if (next == lit_Undef){ // New variable decision: decisions++; next = pickBranchLit(polarity_mode, random_var_freq); if (next == lit_Undef) // Model found: return l_True; } // Increase decision level and enqueue 'next' assert(value(next) == l_Undef); newDecisionLevel(); uncheckedEnqueue(next); } } } double Solver::progressEstimate() const { double progress = 0; double F = 1.0 / nVars(); for (int i = 0; i <= decisionLevel(); i++){ int beg = i == 0 ? 0 : trail_lim[i - 1]; int end = i == decisionLevel() ? trail.size() : trail_lim[i]; progress += pow(F, i) * (end - beg); } return progress / nVars(); } bool Solver::solve(const vec& assumps) { model.clear(); conflict.clear(); if (!ok) return false; assumps.copyTo(assumptions); double nof_conflicts = restart_first; double nof_learnts = nClauses() * learntsize_factor; lbool status = l_Undef; if (verbosity >= 1){ reportf("============================[ Search Statistics ]==============================\n"); reportf("| Conflicts | ORIGINAL | LEARNT | Progress |\n"); reportf("| | Vars Clauses Literals | Limit Clauses Lit/Cl | |\n"); reportf("===============================================================================\n"); } // Search: while (status == l_Undef){ if (verbosity >= 1) reportf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n", (int)conflicts, order_heap.size(), nClauses(), (int)clauses_literals, (int)nof_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progress_estimate*100), fflush(stdout); status = search((int)nof_conflicts, (int)nof_learnts); nof_conflicts *= restart_inc; nof_learnts *= learntsize_inc; } if (verbosity >= 1) reportf("===============================================================================\n"); if (status == l_True){ // Extend & copy model: model.growTo(nVars()); for (int i = 0; i < nVars(); i++) model[i] = value(i); #ifndef NDEBUG verifyModel(); #endif }else{ assert(status == l_False); if (conflict.size() == 0) ok = false; } cancelUntil(0); return status == l_True; } //================================================================================================= // Debug methods: void Solver::verifyModel() { bool failed = false; for (int i = 0; i < clauses.size(); i++){ assert(clauses[i]->mark() == 0); Clause& c = *clauses[i]; for (int j = 0; j < c.size(); j++) if (modelValue(c[j]) == l_True) goto next; reportf("unsatisfied clause: "); printClause(*clauses[i]); reportf("\n"); failed = true; next:; } assert(!failed); reportf("Verified %d original clauses.\n", clauses.size()); } void Solver::checkLiteralCount() { // Check that sizes are calculated correctly: int cnt = 0; for (int i = 0; i < clauses.size(); i++) if (clauses[i]->mark() == 0) cnt += clauses[i]->size(); if ((int)clauses_literals != cnt){ fprintf(stderr, "literal count: %d, real value = %d\n", (int)clauses_literals, cnt); assert((int)clauses_literals == cnt); } } minisat/spkg-install0000755000177400017740000000035711165245263015004 0ustar boothbyboothbymkdir $SAGE_LOCAL/include/minisat cd core make Solver.o cd .. cd simp make SimpSolver.o cd .. ar rcs libminisat.a core/Solver.o simp/SimpSolver.o cp simp/*.h core/*.h mtl/*.h $SAGE_LOCAL/include/minisat cp libminisat.a $SAGE_LOCAL/lib minisat/LICENSE0000640000177400017740000000210110511272556013433 0ustar boothbyboothbyMiniSat -- 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. minisat/simp/0000755000177400017740000000000010650231025013376 5ustar boothbyboothbyminisat/simp/Main.C0000644000177400017740000003325510525173055014407 0ustar boothbyboothby/******************************************************************************************[Main.C] 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. **************************************************************************************************/ #include #include #include #include #include #include #include "SimpSolver.h" /*************************************************************************************/ #ifdef _MSC_VER #include static inline double cpuTime(void) { return (double)clock() / CLOCKS_PER_SEC; } #else #include #include #include static inline double cpuTime(void) { struct rusage ru; getrusage(RUSAGE_SELF, &ru); return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; } #endif #if defined(__linux__) static inline int memReadStat(int field) { char name[256]; pid_t pid = getpid(); sprintf(name, "/proc/%d/statm", pid); FILE* in = fopen(name, "rb"); if (in == NULL) return 0; int value; for (; field >= 0; field--) fscanf(in, "%d", &value); fclose(in); return value; } static inline uint64_t memUsed() { return (uint64_t)memReadStat(0) * (uint64_t)getpagesize(); } #elif defined(__FreeBSD__) static inline uint64_t memUsed(void) { struct rusage ru; getrusage(RUSAGE_SELF, &ru); return ru.ru_maxrss*1024; } #else static inline uint64_t memUsed() { return 0; } #endif #if defined(__linux__) #include #endif //================================================================================================= // DIMACS Parser: #define CHUNK_LIMIT 1048576 class StreamBuffer { gzFile in; char buf[CHUNK_LIMIT]; int pos; int size; void assureLookahead() { if (pos >= size) { pos = 0; size = gzread(in, buf, sizeof(buf)); } } public: StreamBuffer(gzFile i) : in(i), pos(0), size(0) { assureLookahead(); } int operator * () { return (pos >= size) ? EOF : buf[pos]; } void operator ++ () { pos++; assureLookahead(); } }; //- - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - template static void skipWhitespace(B& in) { while ((*in >= 9 && *in <= 13) || *in == 32) ++in; } template static void skipLine(B& in) { for (;;){ if (*in == EOF || *in == '\0') return; if (*in == '\n') { ++in; return; } ++in; } } template static int parseInt(B& in) { int val = 0; bool neg = false; skipWhitespace(in); if (*in == '-') neg = true, ++in; else if (*in == '+') ++in; if (*in < '0' || *in > '9') reportf("PARSE ERROR! Unexpected char: %c\n", *in), exit(3); while (*in >= '0' && *in <= '9') val = val*10 + (*in - '0'), ++in; return neg ? -val : val; } template static void readClause(B& in, SimpSolver& S, vec& lits) { int parsed_lit, var; lits.clear(); for (;;){ parsed_lit = parseInt(in); if (parsed_lit == 0) break; var = abs(parsed_lit)-1; while (var >= S.nVars()) S.newVar(); lits.push( (parsed_lit > 0) ? Lit(var) : ~Lit(var) ); } } template static bool match(B& in, char* str) { for (; *str != 0; ++str, ++in) if (*str != *in) return false; return true; } template static void parse_DIMACS_main(B& in, SimpSolver& S) { vec lits; for (;;){ skipWhitespace(in); if (*in == EOF) break; else if (*in == 'p'){ if (match(in, "p cnf")){ int vars = parseInt(in); int clauses = parseInt(in); reportf("| Number of variables: %-12d |\n", vars); reportf("| Number of clauses: %-12d |\n", clauses); // SATRACE'06 hack if (clauses > 4000000) S.eliminate(true); }else{ reportf("PARSE ERROR! Unexpected char: %c\n", *in), exit(3); } } else if (*in == 'c' || *in == 'p') skipLine(in); else{ readClause(in, S, lits); S.addClause(lits); } } } // Inserts problem into solver. // static void parse_DIMACS(gzFile input_stream, SimpSolver& S) { StreamBuffer in(input_stream); parse_DIMACS_main(in, S); } //================================================================================================= void printStats(Solver& S) { double cpu_time = cpuTime(); uint64_t mem_used = memUsed(); reportf("restarts : %lld\n", S.starts); reportf("conflicts : %-12lld (%.0f /sec)\n", S.conflicts , S.conflicts /cpu_time); reportf("decisions : %-12lld (%4.2f %% random) (%.0f /sec)\n", S.decisions, (float)S.rnd_decisions*100 / (float)S.decisions, S.decisions /cpu_time); reportf("propagations : %-12lld (%.0f /sec)\n", S.propagations, S.propagations/cpu_time); reportf("conflict literals : %-12lld (%4.2f %% deleted)\n", S.tot_literals, (S.max_literals - S.tot_literals)*100 / (double)S.max_literals); if (mem_used != 0) reportf("Memory used : %.2f MB\n", mem_used / 1048576.0); reportf("CPU time : %g s\n", cpu_time); } SimpSolver* solver; static void SIGINT_handler(int signum) { reportf("\n"); reportf("*** INTERRUPTED ***\n"); printStats(*solver); reportf("\n"); reportf("*** INTERRUPTED ***\n"); exit(1); } //================================================================================================= // Main: void printUsage(char** argv) { reportf("USAGE: %s [options] \n\n where input may be either in plain or gzipped DIMACS.\n\n", argv[0]); reportf("OPTIONS:\n\n"); reportf(" -pre = {none,once}\n"); reportf(" -asymm\n"); reportf(" -rcheck\n"); reportf(" -grow = [ >0 ]\n"); reportf(" -polarity-mode = {true,false,rnd}\n"); reportf(" -decay = [ 0 - 1 ]\n"); reportf(" -rnd-freq = [ 0 - 1 ]\n"); reportf(" -dimacs = \n"); reportf(" -verbosity = {0,1,2}\n"); reportf("\n"); } typedef enum { pre_none, pre_once, pre_repeat } preprocessMode; const char* hasPrefix(const char* str, const char* prefix) { int len = strlen(prefix); if (strncmp(str, prefix, len) == 0) return str + len; else return NULL; } int main(int argc, char** argv) { reportf("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); reportf("WARNING: for repeatability, setting FPU to use double precision\n"); #endif preprocessMode pre = pre_once; const char* dimacs = NULL; const char* freeze = NULL; SimpSolver S; S.verbosity = 1; // This just grew and grew, and I didn't have time to do sensible argument parsing yet :) // int i, j; const char* value; for (i = j = 0; i < argc; i++){ if ((value = hasPrefix(argv[i], "-polarity-mode="))){ if (strcmp(value, "true") == 0) S.polarity_mode = Solver::polarity_true; else if (strcmp(value, "false") == 0) S.polarity_mode = Solver::polarity_false; else if (strcmp(value, "rnd") == 0) S.polarity_mode = Solver::polarity_rnd; else{ reportf("ERROR! unknown polarity-mode %s\n", value); exit(0); } }else if ((value = hasPrefix(argv[i], "-rnd-freq="))){ double rnd; if (sscanf(value, "%lf", &rnd) <= 0 || rnd < 0 || rnd > 1){ reportf("ERROR! illegal rnd-freq constant %s\n", value); exit(0); } S.random_var_freq = rnd; }else if ((value = hasPrefix(argv[i], "-decay="))){ double decay; if (sscanf(value, "%lf", &decay) <= 0 || decay <= 0 || decay > 1){ reportf("ERROR! illegal decay constant %s\n", value); exit(0); } S.var_decay = 1 / decay; }else if ((value = hasPrefix(argv[i], "-verbosity="))){ int verbosity = (int)strtol(value, NULL, 10); if (verbosity == 0 && errno == EINVAL){ reportf("ERROR! illegal verbosity level %s\n", value); exit(0); } S.verbosity = verbosity; }else if ((value = hasPrefix(argv[i], "-pre="))){ if (strcmp(value, "none") == 0) pre = pre_none; else if (strcmp(value, "once") == 0) pre = pre_once; else if (strcmp(value, "repeat") == 0){ pre = pre_repeat; reportf("ERROR! preprocessing mode \"repeat\" is not supported at the moment.\n"); exit(0); }else{ reportf("ERROR! unknown preprocessing mode %s\n", value); exit(0); } }else if (strcmp(argv[i], "-asymm") == 0){ S.asymm_mode = true; }else if (strcmp(argv[i], "-rcheck") == 0){ S.redundancy_check = true; }else if ((value = hasPrefix(argv[i], "-grow="))){ int grow = (int)strtol(value, NULL, 10); if (grow == 0 && errno == EINVAL){ reportf("ERROR! illegal grow constant %s\n", &argv[i][6]); exit(0); } S.grow = grow; }else if ((value = hasPrefix(argv[i], "-dimacs="))){ dimacs = value; }else if ((value = hasPrefix(argv[i], "-freeze="))){ freeze = value; }else if (strcmp(argv[i], "-h") == 0 || strcmp(argv[i], "-help") == 0){ printUsage(argv); exit(0); }else if (strncmp(argv[i], "-", 1) == 0){ reportf("ERROR! unknown flag %s\n", argv[i]); exit(0); }else argv[j++] = argv[i]; } argc = j; double cpu_time = cpuTime(); if (pre == pre_none) S.eliminate(true); solver = &S; signal(SIGINT,SIGINT_handler); signal(SIGHUP,SIGINT_handler); if (argc == 1) reportf("Reading from standard input... Use '-h' or '--help' for help.\n"); gzFile in = (argc == 1) ? gzdopen(0, "rb") : gzopen(argv[1], "rb"); if (in == NULL) reportf("ERROR! Could not open file: %s\n", argc == 1 ? "" : argv[1]), exit(1); reportf("============================[ Problem Statistics ]=============================\n"); reportf("| |\n"); parse_DIMACS(in, S); gzclose(in); FILE* res = (argc >= 3) ? fopen(argv[2], "wb") : NULL; double parse_time = cpuTime() - cpu_time; reportf("| Parsing time: %-12.2f s |\n", parse_time); /*HACK: Freeze variables*/ if (freeze != NULL && pre != pre_none){ int count = 0; FILE* in = fopen(freeze, "rb"); for(;;){ Var x; fscanf(in, "%d", &x); if (x == 0) break; x--; /**/assert(S.n_occ[toInt(Lit(x))] + S.n_occ[toInt(~Lit(x))] != 0); /**/assert(S.value(x) == l_Undef); S.setFrozen(x, true); count++; } fclose(in); reportf("| Frozen vars : %-12.0f |\n", (double)count); } /*END*/ if (!S.simplify()){ reportf("Solved by unit propagation\n"); if (res != NULL) fprintf(res, "UNSAT\n"), fclose(res); printf("UNSATISFIABLE\n"); exit(20); } if (dimacs){ if (pre != pre_none) S.eliminate(true); reportf("==============================[ Writing DIMACS ]===============================\n"); S.toDimacs(dimacs); printStats(S); exit(0); }else{ bool ret = S.solve(true, true); printStats(S); reportf("\n"); printf(ret ? "SATISFIABLE\n" : "UNSATISFIABLE\n"); if (res != NULL){ if (ret){ 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 fprintf(res, "UNSAT\n"); fclose(res); } #ifdef NDEBUG exit(ret ? 10 : 20); // (faster than "return", which will invoke the destructor for 'Solver') #endif } } minisat/simp/SimpSolver.h0000644000177400017740000001414710525172426015673 0ustar boothbyboothby/************************************************************************************[SimpSolver.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 SimpSolver_h #define SimpSolver_h #include #include "Queue.h" #include "Solver.h" class SimpSolver : public Solver { public: // Constructor/Destructor: // SimpSolver(); ~SimpSolver(); // Problem specification: // Var newVar (bool polarity = true, bool dvar = true); bool addClause (vec& ps); // Variable mode: // void setFrozen (Var v, bool b); // If a variable is frozen it will not be eliminated. // Solving: // bool solve (const vec& assumps, bool do_simp = true, bool turn_off_simp = false); bool solve (bool do_simp = true, bool turn_off_simp = false); bool eliminate (bool turn_off_elim = false); // Perform variable elimination based simplification. // Generate a (possibly simplified) DIMACS file: // void toDimacs (const char* file); // Mode of operation: // int grow; // Allow a variable elimination step to grow by a number of clauses (default to zero). bool asymm_mode; // Shrink clauses by asymmetric branching. bool redundancy_check; // Check if a clause is already implied. Prett costly, and subsumes subsumptions :) // Statistics: // int merges; int asymm_lits; int remembered_clauses; // protected: public: // Helper structures: // struct ElimData { int order; // 0 means not eliminated, >0 gives an index in the elimination order vec eliminated; ElimData() : order(0) {} }; struct ElimOrderLt { const vec& elimtable; ElimOrderLt(const vec& et) : elimtable(et) {} bool operator()(Var x, Var y) { return elimtable[x].order > elimtable[y].order; } }; struct ElimLt { const vec& n_occ; ElimLt(const vec& 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); } }; // Solver state: // int elimorder; bool use_simplification; vec elimtable; vec touched; vec > occurs; vec n_occ; Heap elim_heap; Queue subsumption_queue; vec frozen; int bwdsub_assigns; // Temporaries: // Clause* bwdsub_tmpunit; // Main internal methods: // bool asymm (Var v, Clause& c); bool asymmVar (Var v); void updateElimHeap (Var v); void cleanOcc (Var v); vec& getOccurs (Var x); void gatherTouchedClauses (); bool merge (const Clause& _ps, const Clause& _qs, Var v, vec& 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); void extendModel (); void verifyModel (); void removeClause (Clause& c); bool strengthenClause (Clause& c, Lit l); void cleanUpClauses (); bool implied (const vec& c); void toDimacs (FILE* f, Clause& c); bool isEliminated (Var v) const; }; //================================================================================================= // Implementation of inline methods: inline void SimpSolver::updateElimHeap(Var v) { if (elimtable[v].order == 0) elim_heap.update(v); } inline void SimpSolver::cleanOcc(Var v) { assert(use_simplification); 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); // This seems slower. Why?! occurs[v].shrink(end - j); } inline vec& SimpSolver::getOccurs(Var x) { cleanOcc(x); return occurs[x]; } inline bool SimpSolver::isEliminated (Var v) const { return v < elimtable.size() && elimtable[v].order != 0; } inline void SimpSolver::setFrozen (Var v, bool b) { frozen[v] = (char)b; if (b) { updateElimHeap(v); } } inline bool SimpSolver::solve (bool do_simp, bool turn_off_simp) { vec tmp; return solve(tmp, do_simp, turn_off_simp); } //================================================================================================= #endif minisat/simp/Makefile0000644000177400017740000000046311165245226015053 0ustar boothbyboothbyMTL = ../mtl CORE = ../core CHDRS = $(wildcard *.h) $(wildcard $(MTL)/*.h) EXEC = minisat CFLAGS = -I$(MTL) -I$(CORE) -Wall -ffloat-store -fPIC LFLAGS = -lz CSRCS = $(wildcard *.C) COBJS = $(addsuffix .o, $(basename $(CSRCS))) $(CORE)/Solver.o include ../mtl/template.mk minisat/simp/SimpSolver.C0000644000177400017740000004724010650231025015614 0ustar boothbyboothby/************************************************************************************[SimpSolver.C] 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. **************************************************************************************************/ #include "Sort.h" #include "SimpSolver.h" //================================================================================================= // Constructor/Destructor: SimpSolver::SimpSolver() : grow (0) , asymm_mode (false) , redundancy_check (false) , merges (0) , asymm_lits (0) , remembered_clauses (0) , elimorder (1) , use_simplification (true) , elim_heap (ElimLt(n_occ)) , bwdsub_assigns (0) { vec dummy(1,lit_Undef); bwdsub_tmpunit = Clause_new(dummy); remove_satisfied = false; } SimpSolver::~SimpSolver() { free(bwdsub_tmpunit); // 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]); } Var SimpSolver::newVar(bool sign, bool dvar) { Var v = Solver::newVar(sign, dvar); if (use_simplification){ n_occ .push(0); n_occ .push(0); occurs .push(); frozen .push((char)false); touched .push(0); elim_heap.insert(v); elimtable.push(); } return v; } bool SimpSolver::solve(const vec& assumps, bool do_simp, bool turn_off_simp) { vec extra_frozen; bool result = true; do_simp &= use_simplification; if (do_simp){ // Assumptions must be temporarily frozen to run variable elimination: for (int i = 0; i < assumps.size(); i++){ Var v = var(assumps[i]); // If an assumption has been eliminated, remember it. if (isEliminated(v)) remember(v); if (!frozen[v]){ // Freeze and store. setFrozen(v, true); extra_frozen.push(v); } } result = eliminate(turn_off_simp); } if (result) result = Solver::solve(assumps); if (result) { extendModel(); #ifndef NDEBUG verifyModel(); #endif } 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& ps) { for (int i = 0; i < ps.size(); i++) if (isEliminated(var(ps[i]))) remember(var(ps[i])); int nclauses = clauses.size(); if (redundancy_check && implied(ps)) return true; if (!Solver::addClause(ps)) return false; if (use_simplification && clauses.size() == nclauses + 1){ Clause& c = *clauses.last(); subsumption_queue.insert(&c); for (int i = 0; i < c.size(); i++){ assert(occurs.size() > var(c[i])); assert(!find(occurs[var(c[i])], &c)); occurs[var(c[i])].push(&c); n_occ[toInt(c[i])]++; touched[var(c[i])] = 1; assert(elimtable[var(c[i])].order == 0); if (elim_heap.inHeap(var(c[i]))) elim_heap.increase_(var(c[i])); } } return true; } void SimpSolver::removeClause(Clause& c) { assert(!c.learnt()); if (use_simplification) for (int i = 0; i < c.size(); i++){ n_occ[toInt(c[i])]--; updateElimHeap(var(c[i])); } detachClause(c); c.mark(1); } bool SimpSolver::strengthenClause(Clause& c, Lit l) { assert(decisionLevel() == 0); assert(c.mark() == 0); assert(!c.learnt()); assert(find(watches[toInt(~c[0])], &c)); assert(find(watches[toInt(~c[1])], &c)); // FIX: this is too inefficient but would be nice to have (properly implemented) // if (!find(subsumption_queue, &c)) subsumption_queue.insert(&c); // If l is watched, delete it from watcher list and watch a new literal if (c[0] == l || c[1] == l){ Lit other = c[0] == l ? c[1] : c[0]; if (c.size() == 2){ removeClause(c); c.strengthen(l); }else{ c.strengthen(l); remove(watches[toInt(~l)], &c); // Add a watch for the correct literal watches[toInt(~(c[1] == other ? c[0] : c[1]))].push(&c); // !! this version assumes that remove does not change the order !! //watches[toInt(~c[1])].push(&c); clauses_literals -= 1; } } else{ c.strengthen(l); clauses_literals -= 1; } // if subsumption-indexing is active perform the necessary updates if (use_simplification){ remove(occurs[var(l)], &c); n_occ[toInt(l)]--; updateElimHeap(var(l)); } return c.size() == 1 ? enqueue(c[0]) && propagate() == NULL : 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& 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) { 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; 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; } next:; } return true; } void SimpSolver::gatherTouchedClauses() { //fprintf(stderr, "Gathering clauses for backwards subsumption\n"); int ntouched = 0; for (int i = 0; i < touched.size(); i++) if (touched[i]){ const vec& cs = getOccurs(i); ntouched++; for (int j = 0; j < cs.size(); j++) if (cs[j]->mark() == 0){ subsumption_queue.insert(cs[j]); cs[j]->mark(2); } touched[i] = 0; } //fprintf(stderr, "Touched variables %d of %d yields %d clauses to check\n", ntouched, touched.size(), clauses.size()); for (int i = 0; i < subsumption_queue.size(); i++) subsumption_queue[i]->mark(0); } bool SimpSolver::implied(const vec& 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() != NULL; 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()){ // 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++]; (*bwdsub_tmpunit)[0] = l; bwdsub_tmpunit->calcAbstraction(); assert(bwdsub_tmpunit->mark() == 0); subsumption_queue.insert(bwdsub_tmpunit); } Clause& c = *subsumption_queue.peek(); subsumption_queue.pop(); if (c.mark()) continue; if (verbose && verbosity >= 2 && cnt++ % 1000 == 0) reportf("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& _cs = getOccurs(best); Clause** cs = (Clause**)_cs; for (int j = 0; j < _cs.size(); j++) if (c.mark()) break; else if (!cs[j]->mark() && cs[j] != &c){ Lit l = c.subsumes(*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, Clause& c) { 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() != NULL){ cancelUntil(0); asymm_lits++; if (!strengthenClause(c, l)) return false; }else cancelUntil(0); return true; } bool SimpSolver::asymmVar(Var v) { assert(!frozen[v]); assert(use_simplification); vec pos, neg; const vec& cls = getOccurs(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(); } void SimpSolver::verifyModel() { bool failed = false; int cnt = 0; // NOTE: elimtable.size() might be lower than nVars() at the moment for (int i = 0; i < elimtable.size(); i++) if (elimtable[i].order > 0) for (int j = 0; j < elimtable[i].eliminated.size(); j++){ cnt++; Clause& c = *elimtable[i].eliminated[j]; for (int k = 0; k < c.size(); k++) if (modelValue(c[k]) == l_True) goto next; reportf("unsatisfied clause: "); printClause(*elimtable[i].eliminated[j]); reportf("\n"); failed = true; next:; } assert(!failed); reportf("Verified %d eliminated clauses.\n", cnt); } bool SimpSolver::eliminateVar(Var v, bool fail) { if (!fail && asymm_mode && !asymmVar(v)) return false; const vec& cls = getOccurs(v); // if (value(v) != l_Undef || cls.size() == 0) return true; if (value(v) != l_Undef) return true; // Split the occurrences into positive and negative: vec pos, neg; for (int i = 0; i < cls.size(); i++) (find(*cls[i], Lit(v)) ? pos : neg).push(cls[i]); // Check if number of clauses decreases: int cnt = 0; for (int i = 0; i < pos.size(); i++) for (int j = 0; j < neg.size(); j++) if (merge(*pos[i], *neg[j], v) && ++cnt > cls.size() + grow) return true; // Delete and store old clauses: setDecisionVar(v, false); elimtable[v].order = elimorder++; assert(elimtable[v].eliminated.size() == 0); for (int i = 0; i < cls.size(); i++){ elimtable[v].eliminated.push(Clause_new(*cls[i])); removeClause(*cls[i]); } // Produce clauses in cross product: int top = clauses.size(); vec resolvent; for (int i = 0; i < pos.size(); i++) for (int j = 0; j < neg.size(); j++) if (merge(*pos[i], *neg[j], v, resolvent) && !addClause(resolvent)) return false; // DEBUG: For checking that a clause set is saturated with respect to variable elimination. // If the clause set is expected to be saturated at this point, this constitutes an // error. if (fail){ reportf("eliminated var %d, %d <= %d\n", v+1, cnt, cls.size()); reportf("previous clauses:\n"); for (int i = 0; i < cls.size(); i++){ printClause(*cls[i]); reportf("\n"); } reportf("new clauses:\n"); for (int i = top; i < clauses.size(); i++){ printClause(*clauses[i]); reportf("\n"); } assert(0); } return backwardSubsumptionCheck(); } void SimpSolver::remember(Var v) { assert(decisionLevel() == 0); assert(isEliminated(v)); vec clause; // Re-activate variable: elimtable[v].order = 0; setDecisionVar(v, true); // Not good if the variable wasn't a decision variable before. Not sure how to fix this right now. if (use_simplification) updateElimHeap(v); // Reintroduce all old clauses which may implicitly remember other clauses: for (int i = 0; i < elimtable[v].eliminated.size(); i++){ Clause& c = *elimtable[v].eliminated[i]; clause.clear(); for (int j = 0; j < c.size(); j++) clause.push(c[j]); remembered_clauses++; check(addClause(clause)); free(&c); } elimtable[v].eliminated.clear(); } void SimpSolver::extendModel() { vec vs; // NOTE: elimtable.size() might be lower than nVars() at the moment for (int v = 0; v < elimtable.size(); v++) if (elimtable[v].order > 0) vs.push(v); sort(vs, ElimOrderLt(elimtable)); for (int i = 0; i < vs.size(); i++){ Var v = vs[i]; Lit l = lit_Undef; for (int j = 0; j < elimtable[v].eliminated.size(); j++){ Clause& c = *elimtable[v].eliminated[j]; for (int k = 0; k < c.size(); k++) if (var(c[k]) == v) l = c[k]; else if (modelValue(c[k]) != l_False) goto next; assert(l != lit_Undef); model[v] = lbool(!sign(l)); break; next:; } if (model[v] == l_Undef) model[v] = l_True; } } bool SimpSolver::eliminate(bool turn_off_elim) { if (!ok || !use_simplification) return ok; // Main simplification loop: //assert(subsumption_queue.size() == 0); //gatherTouchedClauses(); while (subsumption_queue.size() > 0 || elim_heap.size() > 0){ //fprintf(stderr, "subsumption phase: (%d)\n", subsumption_queue.size()); if (!backwardSubsumptionCheck(true)) return false; //fprintf(stderr, "elimination phase:\n (%d)", elim_heap.size()); for (int cnt = 0; !elim_heap.empty(); cnt++){ Var elim = elim_heap.removeMin(); if (verbosity >= 2 && cnt % 100 == 0) reportf("elimination left: %10d\r", elim_heap.size()); if (!frozen[elim] && !eliminateVar(elim)) return false; } assert(subsumption_queue.size() == 0); gatherTouchedClauses(); } // Cleanup: cleanUpClauses(); order_heap.filter(VarFilter(*this)); #ifdef INVARIANTS // Check that no more subsumption is possible: reportf("Checking that no more subsumption is possible\n"); for (int i = 0; i < clauses.size(); i++){ if (i % 1000 == 0) reportf("left %10d\r", clauses.size() - i); assert(clauses[i]->mark() == 0); for (int j = 0; j < i; j++) assert(clauses[i]->subsumes(*clauses[j]) == lit_Error); } reportf("done.\n"); // Check that no more elimination is possible: reportf("Checking that no more elimination is possible\n"); for (int i = 0; i < nVars(); i++) if (!frozen[i]) eliminateVar(i, true); reportf("done.\n"); checkLiteralCount(); #endif // If no more simplification is needed, free all simplification-related data structures: if (turn_off_elim){ use_simplification = false; touched.clear(true); occurs.clear(true); n_occ.clear(true); subsumption_queue.clear(true); elim_heap.clear(true); remove_satisfied = true; } return true; } void SimpSolver::cleanUpClauses() { int i , j; vec dirty; for (i = 0; i < clauses.size(); i++) if (clauses[i]->mark() == 1){ Clause& c = *clauses[i]; for (int k = 0; k < c.size(); k++) if (!seen[var(c[k])]){ seen[var(c[k])] = 1; dirty.push(var(c[k])); } } for (i = 0; i < dirty.size(); i++){ cleanOcc(dirty[i]); seen[dirty[i]] = 0; } for (i = j = 0; i < clauses.size(); i++) if (clauses[i]->mark() == 1) free(clauses[i]); else clauses[j++] = clauses[i]; clauses.shrink(i - j); } //================================================================================================= // Convert to DIMACS: void SimpSolver::toDimacs(FILE* f, Clause& c) { if (satisfied(c)) return; for (int i = 0; i < c.size(); i++) if (value(c[i]) != l_False) fprintf(f, "%s%d ", sign(c[i]) ? "-" : "", var(c[i])+1); fprintf(f, "0\n"); } void SimpSolver::toDimacs(const char* file) { assert(decisionLevel() == 0); FILE* f = fopen(file, "wr"); if (f != NULL){ // Cannot use removeClauses here because it is not safe // to deallocate them at this point. Could be improved. int cnt = 0; for (int i = 0; i < clauses.size(); i++) if (!satisfied(*clauses[i])) cnt++; fprintf(f, "p cnf %d %d\n", nVars(), cnt); for (int i = 0; i < clauses.size(); i++) toDimacs(f, *clauses[i]); fprintf(stderr, "Wrote %d clauses...\n", clauses.size()); }else fprintf(stderr, "could not open file %s\n", file); } minisat/.hg/0000755000177400017740000000000011165245554013120 5ustar boothbyboothbyminisat/.hg/store/0000755000177400017740000000000011165245554014254 5ustar boothbyboothbyminisat/.hg/store/00changelog.i0000644000177400017740000000125511165245554016520 0ustar boothbyboothbyΦ3[2x]j0IibalݟQ1'kJo%\0) 'I]5RTX89>[[y\L㭉eTPe,b$吽vOyFJ;*eJ p\`O9^thNO,^5'0paGc?hq݁?+s~ ]s5!(@Gs5z.ł FϙarRx-A ذ,c?ZhI+ރ&c(:Ԭ^! CDCHh5c37RbJJjnZBI{BfLu1I%minisat/.hg/store/data/0000755000177400017740000000000011165241121015147 5ustar boothbyboothbyminisat/.hg/store/data/_r_e_a_d_m_e.i0000644000177400017740000000044011165241121017646 0ustar boothbyboothby,\=m~tR N=xJAuTxx$MfgN⢾񇈞cQ|]K|r>MZ7B`m1Wzel@V y14!Ng8|FpaEوw6B\#QLX類Uw&Zg4W#;Y`p\FN60G0k|lzomݞQIݖWՊxminisat/.hg/store/data/spkg-install.i0000644000177400017740000000057111165244726017752 0ustar boothbyboothbyZ D0H ՛xN,RP vtwwvK)MI,N,JNQH/JMNU(* gB\\E E 9IPz`9eEz ]@&4C4EWBnIN1("JpMrAzpzD7Kfϣfxc``f``0bT"|==. P83 Ȃ6) L.PH/J3rKrJk~f^rNiJ~nf^fqb #minisat/.hg/store/data/mtl/0000755000177400017740000000000011165241121015743 5ustar boothbyboothbyminisat/.hg/store/data/mtl/template.mk.i0000644000177400017740000000167711165241121020351 0ustar boothbyboothby x|dž[;Y`nTIgxVmo0 DV&[nmkJ4 !ɜns8 tڤ!ܻt:$2[QP*0ϼ{a*ca$uf"^{;ͼ,ỐiG)*Vڅ6ifr?! GAj ɼ ɋ(8ɂm uekۦq *,@Fedm#UjU^ gwa16φse t{OA}RZlx5>ʡy[}/1T6, M I@@:E9fd .C0Fqt#'9T0D,F>>fwgs-?a }fz7\(+Ɯgp!_wcDX I|He܈T}4Ly2-#H86CD7ȉV#>>,k{MNֆpS2xa߾lh-7f㳛9q)ke(:#rO-LXmwJQU%J.QU>(Y]_1 DD\D~ mO7mw{Ik7k#V.LH;i4FaVjsKўp5.7đ3dSobADc{ =¢gl}] zŤ T:5eBheF <-@-ƄB7M-+:$TBƒҮ&k!vZfLCٞicjz_Ex.^D=R0A=pV!dQk!<3s\=_R BD#jJfE޽Dˋ漐,j&eABR+>*)48rBiT&URRӜW0r8PRB)赦#ˉK*1K@x4.Ō*Qo"r.2N2$c$ ҲʅKUTcLik\ĊAH @iӬ~s|1ʅl =Z(n3S 㤬H<~X2 U޻G"$,،K&0NyVy^Ҳ X Q2*R(\]o,#pMv©tR40u) :E4K?ʋ0&h_S!ǿϞ߶sQDAH^\y~7l{c14H<7`}7luuν_b_cv c59! \з{~'w^bCQ 3 CS7]95jow.\c%4j+﮺9Vq(xczEMNE:!0ۄt2Xv[T^Ev"m|^nF^I1=v׌Z|nI:qvɧ~fo #d&q*Zd)>^)aB,pI{\8K&Y~03*˜JܿDaQ#(0[Kw:&=90bMqƖӉko)CL #hm@XMS_i$1Տ^>ѻ& Ac}xhh&Br?]bgiP#W ]==a⦹YmW-&%8#!)^}VU뭔+aYR}d[ }ƫvE?s,&ņ>4T$zh'eL k4 _NtgX6@c'ӣ}e03( gѨɷG6ts8kBPVߦ{J! *v~¿ҹռ`ʼ1NïiMvE6,:ކUg{P?]8~2N3Ƙminisat/.hg/store/data/mtl/_heap.h.i0000644000177400017740000000371511165241121017425 0ustar boothbyboothby_8xEVxXoJJn I~%+b]Șv]3ICۛ}ZUgws&g~s;`k#/Ղؾn--C'`h>1DD6a' ,fH1+~| ,Ff zk|cKGEQ,E۰Hxh54hJɒ!h/߂'.b'!fy@2 GA[ v7<@ 4`#|EL-B XrIfh -g"!IhNѐ-*3ާT=ቶdg)2P= $Jx"-9y\j[B<2KHH455-m%km_nEx;19H ͷ#| @Lɸ_R7 =f$7% ]-wOk|9` FJuEO&X9:,@yjOw^PT2]xM5=tx7(3:( kց"/Qʉ s$g4uW} r 4?䂔J|+|):% BP1Nba/S? W2k ]Jw|CGS֜p#FR)fLfwA'dqj(,v[D  G1 fpR!^@oi x ʹcWSVQ;9`󳧰$Pj-lp9hIgcXϤ /2js Sweq+:I)wxD3:02J*P)N>]FbMjUR np[Wx;-=Y9WB,YiJ)m&EGY. P BMUMtI EW~0= {94<NtPo f鼜*ή%#S{ ͖P[KAz] gq/tI^R0}ow,>BcW'zx_P%?!o SӲ#D}b}jfd "͏蔧kCJjAeܟV^)I5UMd]l^;+r9HzIB^F`eAQ_s'E N^,x$;>95ߜ*T# .!Y,TG]~YKEˤtC:/~*pmP 1t(_U8|W minisat/.hg/store/data/mtl/_vec.h.i0000644000177400017740000000401411165241121017256 0ustar boothbyboothbyzMN"tu{ aoBLxXmOJ_qn+Q8Pz*\buCnUq&d! 3~ ޫ*y9y댻oE74d,GA&:W Ђ?/ WH%"NSƹH2MA0* LLl&BB8 +aC װ g l0f yb(D˹ #}Sl&(xc"1Z+2DY"C° rBHe').Sx0W9_f-H3&LFJ! 7*TD!HͶVxiYCEw5SMKdjLI*Lf4Cۧ*ԊL Up:u]"3cժШF9s>,5@!o}9uy 9}2x8ʡ_~F CN3НJ F!WFDp /Fnť:=p} {T[9'b شό*cpQ'$i6S!>U0~:Yfj$JYSw8BK`ڄ]˨ BƎ8 Xc [uXThF*ƈ8s6KPadbpa;cć{wuy$ һ= mG7JN@O};bf"XͭWZֹ#c^FD}IF/ Dxwv\rf1$܃jF%/AʇΟA4͔΁ (<b6ʽXkDK$5%k̓CLz9nu|"l>eQRRY?ĺ1{7Ȗ*ǔ(ɒ:-kRXiqR^<008mSFW C ScWPd>JumԐVsd^4ކVkХf\Ị0 :nYnt+On(;kiΏHU"Axq3Vz4D l}=m,|&q@o}_|Ɵe(mёi wqL}F/&lo-=38NFP+\ tKEMgS6FoS#HM>,voX`X)n) sǸ)l;9k4 W?XzBjY&ͿdNѸDҹg啃Z{;[F]lv>}Yɣ:eRm5 7+B6. ( G*]g}̛(p%Mp^{9+\,\$bgH3Unx)4,hO  :A%oc^n湺5fToq}f'Z˔LmxhobNL%MS&StxH\gMu#` L}RTUNT!Xa5'>*10]t+Oo&}սP;x,%-/E`T2oi Nc_{rBT_}z$gk%os{Mminisat/.hg/store/data/mtl/_queue.h.i0000644000177400017740000000264011165241121017630 0ustar boothbyboothby` $Wu.dѯFrxVmoFίt~/Mlp'Ҩx cחKY xwgg^߽umY/f0dQ V3KaD#=YaDȧdh"$yx*2ė eʠCXρΚ#x2-J&dc05vE14_UMnf@q.V<;SimˌԄ'V2Sc%e1n>:eC,*Kxb} Z-sdgU`L@GK!ȲR|)#qi!E+ST- V!P6G"0%r!/7jSRBb9~S8Olmp޵3б\wLq‰-| o˽O;6cAl>ulst1v܏p5 a̜ACrf?ҺtNxk•y-?tF|ϽF1º{#=ݰz`_5**k*7&tl楍YS¤FS˙ؚYm!n&B> ?\Jc乡KÝ&XPA|ofSCOkW(Tj8zXƶ5E=fk+[\hP:,M_4M&b " Z %pB5M͏L)WkWUUpxRᛁ[/vo)Ya3n MK&qtTw qPЛb"vqƢR_ElVpI  0"K@To;:4मRDHTc8YuIe t*s~_srˆBc* H"}M֔nej}2Eʦo gM֑p7Y-4z'\[F*CߜLR7wR:DZsXt U]& /rۍAW݊ne+CV'k+bʪPy+&P-ݓJ R0kRC{eOѳm5V5 ]M{OEaPiJ~PӅ#]؋ gs2lO7~qj~|}L%f5z*@;M`vikoxR$zh@N (gf,<#i( jK~OTHTH;TP[Py 64:8nGjļ F Sminisat/.hg/store/data/mtl/_map.h.i0000644000177400017740000000343711165241121017266 0ustar boothbyboothbydp>M.#km&QD<43xWSX_qκ1O4 505:pS!\Hݮ{:뗖q ~ fdVq>|377Ҽ j0Kώ@g~&BGe".|,dw?[h1sTXXܵoLX .0Gx]4E` F98b^1?c[pEP]{Tc,Af{} ^ƂbCȢ8s*ܟ{k|_eN"20Sp~ +Xy fsJ3u0f05'_އ=m= k0%Lml]5\ SS`b1 ilx7Ɵӥ' aQk2'chX*֘lQ igC̈́9tٱ1>7Ec00há.{Sw6^ɰ#񓎞izA 5c*}m}֥R,jKiwf1q6[&UҴ6WLWA3%ܜTt*1FPo'V(հUL}mH(\Q~JCEyK뫫[̤!8q{Z }a󊻧('?B 賅bp=dm/ڗ&BE*pqFpq 28Tx5ѨAڱKp>,˰}%G\j1n[Z{O{L'PNOyB~w589AF/{X#7xP (Q'ĊAK&g8vldHhן'zNLvP*͏AP"MM?F}ys2 w+rQ?}p[F⠕JFs.k%b*Ύ#, r#,VxވɝMMX`}J$ő_mO(%l_.m~[@O脤rWoR՞Ĕ!ǭ؈'(#pR)A^R"|sKP!?Rr汘-Ԝd'L?i0Sc>&(/C`Aش4ǧtR>YK%śdKlc|JʀI/R|G)>k] [lcMQy[-gsXf߇ z=Wz: ڴnK<Ic,/4X"#73~?.q7(;B\blEf[*N7\2Lliɇf;S mD3[M:\`K]tY@vVtgkAУ/jminisat/.hg/store/data/mtl/_alg.h.i0000644000177400017740000000170011165241121017243 0ustar boothbyboothbybXidm'xT_o6秸%@a/lfb11Y2$:YP,Q3D*AZH+M3@_0tQow} ݤ#+d[8=n:-1tv)@,jrT/ϙ2F+B֢KcV Ԣ'u ]AQN`5 Za1QAһL[#ѕ};%ɑ9A~/ͭd# l-(*ƞyR{ނGik[脱,F@*t+=17 `KY~HSPJq Tw`D8u>DZvh}iHw ))5,du+.MBR:GWB8n[ Ñ+mQA;T-S}ܾaȋͿ9K};o_RȒ S ,u\9Qa| d30淐, owSeVQ\c,Y|NCV#(OPflEE`d#U@Ovc?qbfh_vp2V mƷ@td>+Zminisat/.hg/store/data/mtl/_basic_heap.h.i0000644000177400017740000000271011165241121020560 0ustar boothbyboothby ]d5-iȩM+<5xVaoHίReZ$=>uN&1 :aX^0u_~ MS*aw͛;evL¢.)ͩ 8:!+6%Kt#>v~7Y"g%9gHS吒,7pW II4,Ao %:[ wBᥥHD<%AX 1PDCăEE(dfCW:~UZTl-$\4F([ǒC#Hw kHXLKTZzQS \ bh\NF`ǬNL"PrݱS62J!D*cVP%2ǐD %3#M"!gy²="Tf4-pʥ ZQPv^iܗ[ qQްN)7+U4{l^צgs#kv0vg: `:7vFX<&s3Gs@s&4pAl˗`Sռ'vpc8AM^`ӃܛGΥQ= |lN&*9G7tg7}5`NFN^X̼XU(Lj81̩ye)/Qh˳Wts' YB#kNś0|܅{= ]־4*myRmJ[=Ml~GӀ)R2PvQ.;[et 2-ES3'aI\QFxu_N*pvo]󌏣mFYv/ǿ0_(eﱐ,sY s\ds1&xQV d D,̅B@m`$1)"T {b'b0HU$ Ob!LE Kxr7cs⍣H,Jg@{-Xb&HDŽZ t s1 ϔY$̅)'ɲ`b~BHHYGvJX¸Hfb޴VR2uf*e. ,.hbE"r(?xdLVjYO[9 yѽQIB*]3ʇ2|p3~ . xqƅOAx5 %F K`p?pM?q-߆`B?B @*vzW8΃~~v2yx0܎nc/v .G_Ya0#N`|ʻEGJ(pհ⹏y}_SQ\օw}թ!ӕ?0Ȍppꢕ<).x`L ]@wZxb@(jhDEh~;+].|Xc:\>~`2Ȳ$ŚMs}Yoq3V_B1>΋i'&RV]:::9[b]%ƚP FKNh a?~.Z|Ēށ8/mXm veXTSU9gs!7`SC-$cY/Ryc !Z ɲGN/F˳f6XjqP̠y3mvF˘HwصP9́MMJ#NY$1&B鈵$QSС.mVr<|\' FhӰ[(7ҨP$6r8X)АGnJ٪a'=0Bة^pPzjj2-ukؽ?1lg?㷆_tV:V+*ç/iwLUvpYX&Ov]vZ>Y% ;~dV6hmURx5PYfu[@[Sz꺎vpPu 7NjR,ͺ=Su&k*e>#2kXsHTO#Nѷ98R^f$HսsSh<.3'ёGЎĮ@Y4N:N8_^ϾJK koOYh/?P7fl&BPֲ4{b }2kʄ$W=i_,v;Vѣg|m?/M$iS긻7k]F T5@]\{V'5;ԗٛ:&- yxdM)7 ظՊnx]eeٔ''*minisat/.hg/store/data/_l_i_c_e_n_s_e.i0000644000177400017740000000130611165241121020174 0ustar boothbyboothbyAq+e"#`?Ƈ-+<x]QK +F{ڕU+1&Hl:&h}'dٞa{mt{}ᶽ=tfƷy3FBj6Fz^t1vMс_h<.F=h"}=g ws`ƨc!7un"f6mFCpPy=^IH 5i;g z{ bN>8 CB{nArLkDwN0ɏHiɮ&ߦ %0sucgGzGQEB^BQ\3x;>чo16so`}X) I+1Zm' دZ!B_%gU^ ^= *KT HW(#K&tK6̹JR|UR J֢aH_JTKdaKVdE*`X@e9Q#!F򧅂( #%]T^R̠KĦ-(UzQ|rEE0\TJbKV׼aPɛ\ Oq↘@pb5|IaZ FKj2Zminisat/.hg/store/data/core/0000755000177400017740000000000011165241121016077 5ustar boothbyboothbyminisat/.hg/store/data/core/_makefile.i0000644000177400017740000000047711165245507020211 0ustar boothbyboothby"Es^]9ֶR\jgx Q[==ܒ.g`FyfNJrbQ^&2_E7GS$ 3%73/8=" QX[\_僬0+3/94%܂ĒTl.Is/[;+WP4fZg;Z/CFLAGS = -I$(MTL) -Wall -ffloat-store -fPIC minisat/.hg/store/data/core/_solver.h.i0000644000177400017740000001220111165241121020144 0ustar boothbyboothbyA?REmTcx;sHhB-1 =aI;e;qT.%KX,u|h$H4qƷ"kͮjQvw8]" "A˹Hr?'|(|&`gW4I(wQ>K9dBYf-Jx s#3O$]JلyFS)x[$ aD'\4kN}u*q=oNw^5@(CCAq<菇]vQ awD 9ΛuBDp _:-'vah;UlT<G$SPvzV{oQ"23^َ3p&EyЀ3`B8"ӹm.bf| K20֟Z5?ūqXA.DM a {?;7IS:EbFƣ-Q#BC4K#23.r4{Y.;-.`8(w+7(l~,@ԖR*yy#YL>4H, Yn }2/b#6`bX=̈́>DiFV);grr/ CT@ ? f 240ƍ|nE)'[ކsn4NO7L?vC{4~"( D1yst?y4 yW"0jKDBj͝(E7e&D5e9 =8PA(p y!ߙT2 fV (FV4u"n"CpcbU[mCTAɒZZl~ԊtW(ƈT6QI1A+(-E:yO|C3::[Nz6P7lZOP)ux5mWٽb%גY`{xpƼnPi5" Ok5xd,w$~@̚dY;*- Na4#tD6+Re6Ѳ-Q:؂h8[( eNZF|Kl&'(gJ(=͑*i%Km~N֊ts` LD=ϮѬ='h0yT>ڣ[2>> GM}x{WӨPY&j"͌?NR)yJ a:&aJ@BOK* RnfwRpJҔր/Se^kEt"`?˯Qfq 0Ɗjoo5 ְ|)Fi# " 9k /id2V5 /ղ#R|CVT[ȱla &l;{7J`:QbtIo(RIf`{ 8QC/, q%|-UƈuȜ_~΁uN6Wp" klZe8ZӯMp4[ hrt",R33/Q%/)d{9&߆E-f`֙Y| EHHMΦtRbO,Wx{:fA=~Nѣ$0(F6TvFW6O@4^yʵ$ZG?|]ni&zc__ra 2zD^'TvZVVsOSѦ ނ1!T{)kA?Fn|t0e "UxRE1$&,ECʺCŃJZT2GHĽu rڵ93~j}6P[SbT*h.I`VF]~D+sUW@Yj OJE'0"M2::f1GylN21n>&$x:6_r_܂*L"#0^9(dTڨFW4dZA1 )=3Hr{7Cadx7 It@^EhF#A%OrQFJ}qծ:o>hd$TJ7\Nrť;z׫|4ٲ]&:j"J4 ##V|խ;*j$VT 'ˬ2{bq:(D/GNic3T=9v$ѷ<]:gRi5&q/%#uS=u5(`iPuW(9װ&Jq8fd;UNĵ(TKUQbP:4oFa/lТ폒[:RKLkަRCt. ^RD^I #1 M d]r 2}]|qڶ Tm#GS[V1~Lb|HK~lj18)s\[}csiC"KIu6Zq"#}Ia!\poPQ$ ]#Q4I'Z%]~`XD`bcɷr ߜQ[&u>_9djôp m +ي3U|7" >3=Y,%MXjZ*ԟi3d D3-[-=oHܐ3Rmɲ߭]nEID{n24A{bLyQ=[(Z,) ۝\wX1 Bi<!iЇu mE3bN#7]*/kPܐIrkQrQi(0ڲsr Ϻ|.% };!Iv?FCF ;Ѡ^uaGVdT!z$u|e(ʥb i&TMG{suM:Fk:X#tj#Y<3ȫMw^/B1 m2T> bcXbdu$O ~Y%:*T\'ļaw+{ܠYKPm2M"Rԅra. yŐK*J*שPHNk#di 5kfuΖ8c]U 'LgqTd 8|pjI[`h`'f_1igAm\;>zg*?Dlu^v~'7Y+dӸњΌh¹ * :qf)PR?HIh=Vkv"Ħa)Ą; ]D7\fWW|䕜G>fifѨJm35ԟtzqG~>[p3@w@O/{j:f$Yh;91"z o,v4 ubGE9_Ps388祖JF]‚"&٦4N!.a*' taG F!J5ÆCwxz/W=ҾQxsx?/?8(ř G3]mNVgggݭ}7"EZ^XA ܌670'd9a{&F:tSjDDiGu&YAQT$btOč2hA񘼩LD"3ţ̅ф\ ))`xݺo.ȏLDql*@su_!4^d4K1jVyga0 f>ItֳF+Y( iGLԬ= c+N(aI2gfER4U- RkH"ǏA2^aq-őEe 7BڢBTU*pETtBdKA.I4C~'RS3ҢAxoQ{@gޗQ6x~[I|H7o;fըϳ~k0^ڧgv kaL·V7N=G,PC[;mOjtvM:kNOgޠG}Hi:RG/xIӑо/;}? 9jaS 5?uZJ:4ۧ5yܒ\=%IK.A^^8u}<`ehX5;;i'Am)v5U"~> ]Z\&[G=,z#_Խ.;,x bu$;(-j=O,kkkw_A_$pGT5tL$n(Fq 7‚h/\̃n)8kjfLLE'E%c }JϥMTO&z)7i=7bBe9{!>*>Ef)bYq\ː؛;iJ4p1_w KuGoWvhġz_pFnAЁ@_V&Li0hPm|':L0%G;rCM x=lh[sŃܰ`I3u)e"򕻲Fd+NCy .Ć7$z?6-$TQA$ƅ$$@KjGTnRY_⎱;0ˏeOYET`=K)`74,M5ћ8^o7ڝqՌL1o^xV{]{bS'Գz4v}ޑZaEt*$khVJug m5jG)9mH#_9Qy97@*1VdsDI%mސ9s%]41Y>Kڢ4\eKy*v1) SDE1|7so_4e4dRT T(0lڰ:~Ɯ!䫌svhoRAҒ:ĭ)Qǣ6fGl?)ϙb(^L48w /ThU![ۗ5z@LАJyZW>a?:ܳ|١_xJ[08hy\7KnU79^D*Lzx})(lH>`PKm3ެ]f\VJ*, u. 74|DyʾQD %N"lq`C})#D>{Z30za {C*M93m"¡M0Yj^ߜOΕZ;{ǩn_@ϗLd_37~Ց3wdYiN̈9ڜJz=!eVz0wklf*[ks碱x&n I,SjTOS1s?!?ibKnėT.Ogb.fs Ԡ#1uWDzŊ,[\.+NBvY`x72Ԡ&n%vjW&hy׳b3 T܏s)+xUYO4`cEkM@|h6.e~%[j 恴H$: :M^kF;C13Qc^ꆼsY0ϙ}%1ovD}.¬P` $K fh4C u &ot|\`l&minisat/.hg/store/data/core/_main._c.i0000644000177400017740000000744211165241121017723 0ustar boothbyboothby,8@A7h?),&xZ{SHߟ`ݚ1&ؔn%K#,$B6g_όdIdri=R],+7o W J%jETt\,O&uRKxW(\`{4}"15 ߦ IOH r8Y4{f v`ӂF=\x1?qEHh&hg1v d*,x.'ˈF3af&r2Ӯ3w4F6 2,Is_H[ g&M&}Yyp;zTBLRוt,ؠ60YM`/,ę0ID<6Ba)ֿRrϏ XyUO3 ߂4¼VJ#8ށ~ ,eFE]{osi cһ7 7]P קuX7t6!uW!{ 5vkĮZ%gN{Iai^ha94t=_-?n{U;,+u{z\6:ɪ1})_w[rHy g-H8+(4WfqxӒX=PK0-ݻ˖~vj4{a&wAˤF=`\{W&`$u[ 2?,F._J9zE;^o]z(,=&y( y:Y0d^NPN Sajm-&Xr ,w,rL @!1PQן|,TA ׭xjS"cǰ&QdLLr3K$h*]Kd`Zwȭ9z'"5RXsa^4N6,rFPLpg+tTR.6v "O1D_~2%y_X&l;m߳?~Q"/8TgpSʄ ld"'iΑ!/ڝ#֑‹ <_1bSU,rB ؈'J:RݗJ0l)dړ4Ka fy< ?8V05b!qhx\w@'~T~2B8L&xB >;"C%2,Mk>$T~]ciO9!Y O ^|"Sn6#\Ŀ 1sP#Q5Mb! d0 a;QY$&%+H)Ƹ7/5PGR'ZC_5y>TX[G։V"1Pd啵~&u/ǤTJ٩eOMYwC2 ȪP.lEI8{;yנSXU&Ւqղ0Iap:gk]W/Y໡nVgҜbc9w7ZwkHcX͇5h<)m;+,#Zzd= 1$XW }dn%9v+K}6s)m+6"DF+ͶJڦ}y*q4"ߍIDe3# U-oo0ڊ+׭&h5bRÎ0+ųi橺Gn@l"m-ٮuT: 20>STn]OOxϋD!+3rUYdbc,zw<0yP|ףְ(' rXG~s(:QIB w~}S{:FYGA" n!?qA1z>zƄW/7]$u 3dy:HRq)!+)Wem'LU].iK}.UK]Y)&'/Cz|9]oe}#2n{c.DR{R؃tl5l(=\KiweN/g _^_RȜ*y@ YN]ernyPRu:|(#|]m~/́ƳD>u=\mf}:_ ʡ3_XLox>#2$E:.Yy*&y6a20Ɛ1c s\{p!?rwﭺbo-p%[ >KnR|>^&O^?rvrMmEuB1U' R? \iaXw /{k~fuc8xIhly,ٜg]f~\i2Y2c.y { ,g10y2+nCiÇxl fass^列-d1w y,X" nq-zP΀É&9]ij4῜./04D˂96@'XO2(B!Mk5Q%ED4 y}k9.8/!>M2.GϽQ xt`^6<|<:01NdGw'~xш >}h OIh†O 1PS ?`09Dǎ{`dѸfN0+;|G>4fþ 7 >O}uPFMbc`72'# Mσqz r0:f@8" 0/ ~o8m,eF)sIs_:mYᴼ ~1m4;?9@uưAd\ [!z- tgͷ7K2P%=nY0yEo|dl@*mwxw,q(/Fw-i|fymnlL"<'?ϛ&xks]O l}RFNXbxσ`+-0M"? sPxeGļHrhd6c9h*e ^VbD=$3D'ےfI_} \gi8|ϣV8S/I+q߹ ER \3s!wB_ܟ:$yHߟ /AqËΦW;Clʳs*X6 $' 9{oo_%D1?q as5I`sd,r_ aW`;¸`!a;ł. ׂ7oZxix^9\f|#?< 6OhIehG[6MPBrC`ƚJQW4с Q!yp#|X_5]=0l  . ۗQSLED )L<1$n"sn,< bq:{ccz<έ~x2Jd^t~O%;EǦ](G ^lvR1`;PӼo!r-v jg{7rh Aٍyb?ўnxnY+z4NSΘ"&# W%΃k)#J E"`O)(m*yDAm2D|-l+B( +T(8*F =TƏCD'طoڰfQu S2wWoi&̳0Ewؕ$у^g`v\lJiыPTƠ>_\wޮESf\hmW FA/X5_~0[b-p0MNV^3Н(MW W8V٬A]a Vǰ7;LMoz3U<70zo3XS:o: ǻmݾK(A^[H^ b*]T/YEj+׃FU tUSE9& d:n=(x``ciYkSJ:c#,2攰[z4Ų.}Oc4G'qFJH *]M!T,E懑$Ogsve#pyqJcϠӱ >w hi`=)yޡ^wcߑ "vL &^XVir5\PNn (IH=6ZN $\Bȿ{mБi'mˈ󬐪4&BEZ܃1$'6}N2ܶ@peqQ)!*OIuL4a0͛me=^zwX$Dib/ bc%ED{ MuíiSް\) X 8]2Js l~K&VتYI[L{rFe}Wɉ ?;ζЏ'ai3Y;O[(؏F.[ h\Ь&k Chd]N$!`AoHN%(wTS7U`;x>0&u5 +N,₫A[fV(kX,s2j?fYH+jcwQ7A{/dmШYz>e($ϘXb޲P'dl2@M\Հv0X+y)R<  p1C6 dgXR#GM '`Wk< r̚MPH,KlK#><#\J涞IZ'I%{ F" s< K%dplva5%gRr y"9U/V2-Pn_rkKF 9 Wgt L!uv!woE;|GCiVr |H2atx)KޗW Aj#pL HGxKM@EIr $;d)!ġRٴaG s 2ӑr :d渌4 gj7*+Y2ο=xÂZI6Ej ^ ޷" d[dJ>z4"*ݠvE ;<ǟ$TEBU[⿻37#?҈Ozᜎjv_y~Wg8J}5%muQe"+B]^lWOavOtvU-yMj>\DPB =kkAwlw;X}lt%Yk ]䤮f1*]VG\a,,B8& X5;Drowíd=)36 A1^hgs.(,:v#XӉ ?^(fS3' au 1<Ñq<‘Lf˒Ysf0^K6(A^{HzSQxQN 6H xUv Ogǭ4m!*sQdwƕήαѽnOT* _vS G>%hB^ #v +u[qQT$#7Ҷsa^^S& !ޚu\;j݌2hKAr嬾]YHE0h=:\-xk]g5m We"xy-. kjWlB3y&KZy?~9nXHԹG)\yHХs U3-]Vl /~$oYl >vֵpqY[fUWsJʐۃX*aga ^+=i)%Z1aJQ*70(Xʗb ( @ߞHN)%@NΒz%Zu]?-7xļH?nai$8ARmc`W;|wP&ďP:L\<=ɹItdI OM\ cdѲ-%vO 5;wia^`~[,Rri0@T|f[mK)>j m{ VngE)dlj,6U 7B +Enч칼$~p8NxI'֑zt8vP୺Xuc)i/. F+,!;&՛S^H䨝hA̠iNP k7bKݰc͒ZX+s݊*L]-ʃCf=ˤyITN,ly_x8ft[QڴcpZD6bq_R-_w(k?b%q^ gtp䃆t< TοZLuפuP΅>QIT8i)N3$byi9ys'H0}SwOaK݅]ѽu9zZ$IXj't,V4#[i̇U (Th"![\I[@DB9 /Eս eEuJxeAߍL1B5^__t3 >Uj]BbL}fr˱2g3 <쥪 [@6hl^ň!.GegꍑQUminisat/.hg/store/data/simp/0000755000177400017740000000000011165241121016117 5ustar boothbyboothbyminisat/.hg/store/data/simp/_simp_solver._c.i0000644000177400017740000001270711165241121021361 0ustar boothbyboothbyNU WJY$[+xbeg,)ٜaVf,h7Ǫ[ 솅,4e>Âp a( a>j*pY՜ݥEb,>S}RU ^VENE*F4Y$rN4)qU ;@<{l 紭:My N}xSyJ8Cx^ v,${?N3[,iLz VQw|i~[,NpGa3Gu,U2`i*p`.7S yAշهdrFcxx̶cc?&/& .瓟 1:???\cvqFgNGC7:?::co& ;&0rp /hs&8 L:`}p10V '}X_G $.>|9z~_!`6x{:KN^xp6x7Q0%I~z?[MF縍%|./'zO1ǀqAI~ .)56pw(z|'eռmgpy}`-3UTŋc>vu BseM3  @XLph% 8̢i4]1riRG_5Xx!XR?`"5xp&$2p3p:8{UM( ,{r߉LkxTYZ,`?b>$9Z,WK^#4E0v,g WƮ?l~IDЃb0/=1K3< WueV/Ȩ !яaQ3h9:2x *j/SnGSCn!}d4zk->~ &ny20?2A3jC4J &34eF?r)(#ɬ~`\Jd|c̬E_/`]{(xf/U a_2iHfS砸j,s"Mٌ)P kp*+ TUZ{Pc%#+n[̒p@ pUI_a+ D"1%l0)ؖ.H*8#J`@B8+)P ƑٚC4{;#(;3 rAJ $[֟k{R&"< 7J^G%8|dXe9 ED5e1|*Ys2D(`V7m5Ud3ڭ/pfE$~FZD"\r)/1C%78h| XҀ/f%(d/-H!kWiFQŞ$f&AZb)`rY;b2ْ/2VϿ|k*br A8|#|6+4#u a)-[ݥK+,܎[jv#HP6i) 9&"P eteCcNdľK9mKy^>#l@rĤ^2N> .ȑI=#PDO`ﵝ4 qx4Ffչcdn Rtdbյ#.Z˽dbVJvU:T 4(T !sHn+/LYC֖*y|rG~vE0ةR1. : hp )gHm9AM%꣚$uI} "+QnNItĢ@"fҌꁽ~~uVg`_lfYflۊYuȞC I.MQv){Fg W]pڠվc;_JB)7%3\Y6HXeSRw$]:VW2AEt߶K8㚵tGیBdcJlak{B7vւ'ڜܑ_ 8P70wfaSM#M sR-7Cq)|"Y;*x)a\s ;m?%o "/ZǺDчV.?Җ/QX:lʶ)mo1 Zm"I^nhЦyT-Nllr4% <|㆞V/P xVC- // tV0|n y5Ɇ [ k>?/X> +hY:/,l_5dEӀ@4|sC+|qf 3]zP:Rd(UxOL }s(\S輶yK~FώE3nSdy]lձH,M>ZtK8WG䱤v[-nr#]e R2#E""[xP򥧛N85Sl ~.<=KWݤgʐmPbY"BU!c-W`=j,UHz=&zWM1pWZEnYKќ-BVDI>6|qxM%vR>;`nDW!հocٹ\ٲ¹i F:8MKYvɺ4lkSڛSukj. BrmmU,u%rHz 0 ʴK֫Zh-Ь&i]Rf} ;_~ & ,_~gT,nDC аj1^'qwH}9rb xw)rj[05$ h3+n۽F}^Cl@sUAT&LbGΒ9T[/E-luгʪ)ap*$ ꮥ xmYCVR+;fW0YV"Z<v0`""|̰T2:8 'c`@)Nl:2ѡ‘=2d`SN/=EHB-=Nu@vrs'Lh ʻ;)v;60VoeRLr(2GePISq$yzRe-a3c.ƻ {OOU"@^`87#y^-\kWԴ!^0c켏=?2PY^ucu: `=vkCIQ=آYi irx"K[%ʡ2W>LuݐLGEhl,qpƥ9{v6MQsQ3c]EP*GCTq28wsOoMgOmSTLl?+ R2İ7l{omeP{M޹8_ءzzJ jYaBc:^vfP/H#W g/+#,yAssK / =g׏pn*X>cY`uU!@wa| u| ` y &^% hPe;,%3-1Cpos/ gAᨖlp"x{aK 4$ QUXxm_ZF׎̫`ڄ: YK(G!`Cl˚raʒJqsoJVH9*Rʌ9wOk$Q*&8_{w"Lz!*X ,Sʡ`#H+ z8> hxu|N(f@N>w=kp1}N`V>'gbN)tIz4 Fc_ =|vӓ#O'hyH'# U޸{? ɐp"\tƓ~w:b:i=$h{IpOYg0:S~.?Ml48r9);ϫyc!1}>WHhHbtG(xLzU)t<:3F R5, ƫ2JJc C 2r٦ /@ xƭB]m]]3=o XN)ABo1kzoF"LBUbdf)? ̯{BFO5 dqpZ?R։Gu?En0*#m^_Bp̈VDpeS͐a6S  ?a_nj8гe3TKB$Z诫/?_ 9 7I>Q06Pƶ L*!O^bmcJ_27_oIA6 )G[t'b╅r d6BZM&0tBHjDv8IB #i<!͸}!1h;+"EUh!ߊ%*BhSNV!F/\=\[\8pE8%(*!*ȯjJ-c<Y 6bIR 7a ߿'̍oVfLwΝ(灚w-I4܍:/.A0$2>*yƒ±yN3?uksbnhI1WE)$#Jx!b6I\8_N !6wc5i-,ǣaM 6"Zm|qq1‰?M@ D!ѩƔMEhZ=IP-ut>U;U;<3 F&5qR7X7q)D3qĜI.̀sp d|:@@*PZp-0|D?jP+1 =i =4汒Oʴ bR{j>*%L9;L7T3xbŀ :Y=m7jFZJ.wrHB\Z[j(vW4W@- k~hqg%[?hlⴍw7UYd/,u{h^0:m+O!,HD^OgYnv=\%HV؜ɥ!9Oπ曽\w\hoyUTvϵ*Ԗ~օ빬{Z?AC1g߻9D:K8j<+LJUSü[PD ,߫&B7 =M)VvW_'xE#Y%ٌ[ߑNdzE >- sTsPvs=e?(ٷȾXrر)8to9:|*MQE>ƥBi#^aѪ mQx6߄_|\_ob K٪2sL㾊q/^Lg{gb⣨v/Ϥ7<靨]:Mq|j;a'aPƵ  C:=x-Vb)c7 #x/mi5tRwStuFzmؓ&Un"=?˥qGLw7Dgcb l yuJJyd!T=1uU,~;O`!4T [g pi(k_aOYmAt+ΡU Gb$(j%ES5JS49̌\Sw{L҆[ƾaSkB_A^Q[R6S(o NލWe.5YwVos {94Z"rشϋȁ_++:H329lP-3} ֚ ܤ/Mi]sĞbۑ-N]Z9^$ pRm4@b)u:LX.mָ.dH| |`Ք_WA _7\{W}uʰ9&_ lAoOż'b yAvWʭ,{y!-SL|Ba6%SYY,\{ιV %q*li@޴Yj|,~|ނSr#q+עŅM&J3 4 /rKBy֜Ӆ1?WC>?~fI|X1]Z$Q.7<ø =:oT *+GAg6uMf,ԴॗS^bGfF7([+sbZ k!.mCLak[,vۙMH|*?NbhJZЭK|S'Ǽk +5Ѱd|AzbbE]1 Hsۘ=v$by7&GuBbOqWnc> minisat/.hg/store/data/simp/_simp_solver.h.i0000644000177400017740000000442711165241121021227 0ustar boothbyboothbygS9{D$ڟ.)xXmo8_1:Nqk+p~YJsEQDLd+Nܢwԫ.p A,>gF:k_$;uV_O*8=3\)#~~Sk1 %,-}TJZ-\J.RV,c=,0U,n"c U-Y0Æe bB4 ]B'JB1R,S1$Ez:i!D AkP$;߭l!Nܱ~F53ziPale"T1WoٖuV' O,ˊdM\A., A3-O%vzR!6AnX<)Rs!%a.-@(ѫiJX/q? ޱ5[P<:Vzw+7MrsK1}WHADYZD'B`lSN"\Rt Bz# LbQ3X[0iJڨxLYٺ XL<%-iJʲ@,e y/YTba$˘RniZEņV&O2O]_ڣ6T/wR 5,BH96tbǣnؾL8f9z=JVJURI&2F8D+,4ƭ,ZQWrS=aTa0ރ3/^0rBdoZ9uCVd~1©꜆ U -dfΣHi%-sh½綆=b*/_;-.u0Sh N5jS rCt_sA'J<-^lfqB{8(!cP7w{Kƒ9zD pD`CۨZ !UM["h;Rb)Gu{j9aIjIB&VaHSW f֚}5~Ͱe*5 @Kn1j٦\ RV<:K# !( s,ۚ^g"f)~ 5Qu9=sh:XMӊ12|;wT<}327 csfCc]<9LAћ_zygҘF$7|I4%VTz[Eaӫ|ztT]5_{C?.rh 03֝g_4yV}) h :իE ']bse[Q k>2elyjlYTW嘶PaA:CJߘ}(߃Yķ.yۆEa]8[<ϻw#ŝӫu=؉S ^tHX>=}p ~zZ-XR2ɓSx 15w(u~/j9izrvRsƑ2gPq+msVqFmq-,MUG W}8؂hq]C{pvf|ݹ|8M48ԔblE\%{S&o^# minisat/.hg/store/data/simp/_makefile.i0000644000177400017740000000060611165245507020223 0ustar boothbyboothby-ئ<,kzxmP0 :D/`P^*Bj` M""!t>w' jJG4P+"z.= \م`;$4jhO1XSJxd:.t-h @`멢 f8Y99 ii9%%E@^3R{minisat/.hg/store/undo0000644000177400017740000000012511165245554015142 0ustar boothbyboothbydata/core/Makefile.i196 data/simp/Makefile.i258 00manifest.i870 00changelog.i487 minisat/.hg/store/00manifest.i0000644000177400017740000000203411165245507016371 0ustar boothbyboothbypreh&`w:}￦xeKoE :ge)@"H~|('M{X|gkDĞ!:w>db-v.ci&I6({(/}wjx X8IͣO_C,^8ޠSg#X1bi]ߝ̇64m0w55h3}/Radc-Rsh "  }> Q\BJRY]>8}*@i\t rS.8?/0-6 YmvZ}R m&w2H/V9+7CN9[p)y^g.밴XٻL!^К`2W& ГBv&\hN_, Y*m ճxiy0%[wC<3bU [Pl1~hc6%?#Oy{ZO0ݧ nNQGjeLmLՋ[-ToUA˷ͪNKͽAOKZzQ@+O>/u4y 녓+ֱ(CU6|n-4"ųKwڋiխ^ͧ_th]jÄ,0:X`@T] eACp{3zFcCh 9p7spkg-install417a70b4d5f87f9c7a884411374b066615cfa366x vpв 4ޯ;!3=+avxE̽ 1 @aKtv<CĎ#` j_'sخG()0Frq!&F)z{8T;jEhi8B"minisat/.hg/00changelog.i0000644000177400017740000000007111165241053015345 0ustar boothbyboothby dummy changelog to prevent using the old repo layoutminisat/.hg/undo.branch0000644000177400017740000000000711165241121015223 0ustar boothbyboothbydefaultminisat/.hg/dirstate0000644000177400017740000000121211165245554014656 0ustar boothbyboothbypJ\e?~aO Mn E! mtl/Queue.hnD~ mtl/Alg.hn?ET core/Solver.hn6ET- simp/Main.CnIJ spkg-installnAE%unLICENSEn xE!mtl/template.mknNF2simp/SimpSolver.CnIJ core/MakefilenET/READMEn Emtl/BasicHeap.hnEOhmtl/BoxedVec.hngETsimp/SimpSolver.hn ET mtl/Sort.hn,8ET core/Main.CndD< mtl/Map.hn(ETcore/SolverTypes.hn]Ey core/Solver.CnETK mtl/Heap.hn3IJ simp/MakefilenzET mtl/Vec.hminisat/.hg/undo.dirstate0000644000177400017740000000121211165245507015620 0ustar boothbyboothby.ł FϙarRn E! mtl/Queue.hnD~ mtl/Alg.hn?ET core/Solver.hn6ET- simp/Main.CnIJ spkg-installnAE%unLICENSEn xE!mtl/template.mknNF2simp/SimpSolver.CnE! core/Makefilen(ETcore/SolverTypes.hn Emtl/BasicHeap.hnEOhmtl/BoxedVec.hngETsimp/SimpSolver.hn ET mtl/Sort.hn,8ET core/Main.CndD< mtl/Map.hnET/READMEn]Ey core/Solver.CnETK mtl/Heap.hn-E! simp/MakefilenzET mtl/Vec.hminisat/.hg/requires0000644000177400017740000000001711165241053014666 0ustar boothbyboothbyrevlogv1 store minisat/README0000644000177400017740000000062010525172457013322 0ustar boothbyboothbyDirectory overview: ================== mtl/ Mini Template Library core/ A core version of the solver simp/ An extended solver with simplification capabilities README LICENSE To build (release version: without assertions, statically linked, etc): ====================================================================== cd { core | simp } gmake rs Usage: ====== TODO minisat/mtl/0000755000177400017740000000000010536337740013240 5ustar boothbyboothbyminisat/mtl/Sort.h0000644000177400017740000000620510525172426014337 0ustar boothbyboothby/******************************************************************************************[Sort.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 Sort_h #define Sort_h #include "Vec.h" //================================================================================================= // Some sorting algorithms for vec's template struct LessThan_default { bool operator () (T x, T y) { return x < y; } }; template void selectionSort(T* array, int size, LessThan lt) { int i, j, best_i; T tmp; for (i = 0; i < size-1; i++){ best_i = i; for (j = i+1; j < size; j++){ if (lt(array[j], array[best_i])) best_i = j; } tmp = array[i]; array[i] = array[best_i]; array[best_i] = tmp; } } template static inline void selectionSort(T* array, int size) { selectionSort(array, size, LessThan_default()); } template void sort(T* array, int size, LessThan lt) { if (size <= 15) selectionSort(array, size, lt); else{ T pivot = array[size / 2]; T tmp; int i = -1; int j = size; for(;;){ do i++; while(lt(array[i], pivot)); do j--; while(lt(pivot, array[j])); if (i >= j) break; tmp = array[i]; array[i] = array[j]; array[j] = tmp; } sort(array , i , lt); sort(&array[i], size-i, lt); } } template static inline void sort(T* array, int size) { sort(array, size, LessThan_default()); } //================================================================================================= // For 'vec's: template void sort(vec& v, LessThan lt) { sort((T*)v, v.size(), lt); } template void sort(vec& v) { sort(v, LessThan_default()); } //================================================================================================= #endif minisat/mtl/template.mk0000644000177400017740000000457010510201313015364 0ustar boothbyboothby## ## Template makefile for Standard, Profile, Debug, Release, and Release-static versions ## ## eg: "make rs" for a statically linked release version. ## "make d" for a debug version (no optimizations). ## "make" for the standard version (optimized, but with debug information and assertions active) CSRCS ?= $(wildcard *.C) CHDRS ?= $(wildcard *.h) COBJS ?= $(addsuffix .o, $(basename $(CSRCS))) PCOBJS = $(addsuffix p, $(COBJS)) DCOBJS = $(addsuffix d, $(COBJS)) RCOBJS = $(addsuffix r, $(COBJS)) EXEC ?= $(notdir $(shell pwd)) LIB ?= $(EXEC) CXX ?= g++ CFLAGS ?= -Wall LFLAGS ?= -Wall COPTIMIZE ?= -O3 .PHONY : s p d r rs lib libd clean s: $(EXEC) p: $(EXEC)_profile d: $(EXEC)_debug r: $(EXEC)_release rs: $(EXEC)_static lib: lib$(LIB).a libd: lib$(LIB)d.a ## Compile options %.o: CFLAGS +=$(COPTIMIZE) -ggdb -D DEBUG %.op: CFLAGS +=$(COPTIMIZE) -pg -ggdb -D NDEBUG %.od: CFLAGS +=-O0 -ggdb -D DEBUG # -D INVARIANTS %.or: CFLAGS +=$(COPTIMIZE) -D NDEBUG ## Link options $(EXEC): LFLAGS := -ggdb $(LFLAGS) $(EXEC)_profile: LFLAGS := -ggdb -pg $(LFLAGS) $(EXEC)_debug: LFLAGS := -ggdb $(LFLAGS) $(EXEC)_release: LFLAGS := $(LFLAGS) $(EXEC)_static: LFLAGS := --static $(LFLAGS) ## Dependencies $(EXEC): $(COBJS) $(EXEC)_profile: $(PCOBJS) $(EXEC)_debug: $(DCOBJS) $(EXEC)_release: $(RCOBJS) $(EXEC)_static: $(RCOBJS) lib$(LIB).a: $(filter-out Main.or, $(RCOBJS)) lib$(LIB)d.a: $(filter-out Main.od, $(DCOBJS)) ## Build rule %.o %.op %.od %.or: %.C @echo Compiling: "$@ ( $< )" @$(CXX) $(CFLAGS) -c -o $@ $< ## Linking rules (standard/profile/debug/release) $(EXEC) $(EXEC)_profile $(EXEC)_debug $(EXEC)_release $(EXEC)_static: @echo Linking: "$@ ( $^ )" @$(CXX) $^ $(LFLAGS) -o $@ ## Library rule lib$(LIB).a lib$(LIB)d.a: @echo Library: "$@ ( $^ )" @rm -f $@ @ar cq $@ $^ ## Clean rule clean: @rm -f $(EXEC) $(EXEC)_profile $(EXEC)_debug $(EXEC)_release $(EXEC)_static \ $(COBJS) $(PCOBJS) $(DCOBJS) $(RCOBJS) *.core depend.mak lib$(LIB).a lib$(LIB)d.a ## Make dependencies depend.mk: $(CSRCS) $(CHDRS) @echo Making dependencies ... @$(CXX) $(CFLAGS) -MM $(CSRCS) > depend.mk @cp depend.mk /tmp/depend.mk.tmp @sed "s/o:/op:/" /tmp/depend.mk.tmp >> depend.mk @sed "s/o:/od:/" /tmp/depend.mk.tmp >> depend.mk @sed "s/o:/or:/" /tmp/depend.mk.tmp >> depend.mk @rm /tmp/depend.mk.tmp -include depend.mk minisat/mtl/Vec.h0000644000177400017740000001317210525172426014126 0ustar boothbyboothby/*******************************************************************************************[Vec.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 Vec_h #define Vec_h #include #include #include //================================================================================================= // Automatically resizable arrays // // NOTE! Don't use this vector on datatypes that cannot be re-located in memory (with realloc) template class vec { T* data; int sz; int cap; void init(int size, const T& pad); void grow(int min_cap); // Don't allow copying (error prone): vec& operator = (vec& other) { assert(0); return *this; } vec (vec& other) { assert(0); } static inline int imin(int x, int y) { int mask = (x-y) >> (sizeof(int)*8-1); return (x&mask) + (y&(~mask)); } static inline int imax(int x, int y) { int mask = (y-x) >> (sizeof(int)*8-1); return (x&mask) + (y&(~mask)); } public: // Types: typedef int Key; typedef T Datum; // Constructors: vec(void) : data(NULL) , sz(0) , cap(0) { } vec(int size) : data(NULL) , sz(0) , cap(0) { growTo(size); } vec(int size, const T& pad) : data(NULL) , sz(0) , cap(0) { growTo(size, pad); } vec(T* array, int size) : data(array), sz(size), cap(size) { } // (takes ownership of array -- will be deallocated with 'free()') ~vec(void) { clear(true); } // Ownership of underlying array: T* release (void) { T* ret = data; data = NULL; sz = 0; cap = 0; return ret; } operator T* (void) { return data; } // (unsafe but convenient) operator const T* (void) const { return data; } // Size operations: int size (void) const { return sz; } void shrink (int nelems) { assert(nelems <= sz); for (int i = 0; i < nelems; i++) sz--, data[sz].~T(); } void shrink_(int nelems) { assert(nelems <= sz); sz -= nelems; } void pop (void) { sz--, data[sz].~T(); } void growTo (int size); void growTo (int size, const T& pad); void clear (bool dealloc = false); void capacity (int size) { grow(size); } // Stack interface: #if 1 void push (void) { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); } new (&data[sz]) T(); sz++; } //void push (const T& elem) { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); } new (&data[sz]) T(elem); sz++; } void push (const T& elem) { if (sz == cap) { cap = imax(2, (cap*3+1)>>1); data = (T*)realloc(data, cap * sizeof(T)); } data[sz++] = elem; } void push_ (const T& elem) { assert(sz < cap); data[sz++] = elem; } #else void push (void) { if (sz == cap) grow(sz+1); new (&data[sz]) T() ; sz++; } void push (const T& elem) { if (sz == cap) grow(sz+1); new (&data[sz]) T(elem); sz++; } #endif const T& last (void) const { return data[sz-1]; } T& last (void) { return data[sz-1]; } // Vector interface: const T& operator [] (int index) const { return data[index]; } T& operator [] (int index) { return data[index]; } // Duplicatation (preferred instead): void copyTo(vec& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) new (©[i]) T(data[i]); } void moveTo(vec& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; } }; template void vec::grow(int min_cap) { if (min_cap <= cap) return; if (cap == 0) cap = (min_cap >= 2) ? min_cap : 2; else do cap = (cap*3+1) >> 1; while (cap < min_cap); data = (T*)realloc(data, cap * sizeof(T)); } template void vec::growTo(int size, const T& pad) { if (sz >= size) return; grow(size); for (int i = sz; i < size; i++) new (&data[i]) T(pad); sz = size; } template void vec::growTo(int size) { if (sz >= size) return; grow(size); for (int i = sz; i < size; i++) new (&data[i]) T(); sz = size; } template void vec::clear(bool dealloc) { if (data != NULL){ for (int i = 0; i < sz; i++) data[i].~T(); sz = 0; if (dealloc) free(data), data = NULL, cap = 0; } } #endif minisat/mtl/BasicHeap.h0000644000177400017740000000671410502000006015207 0ustar boothbyboothby/******************************************************************************************[Heap.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 BasicHeap_h #define BasicHeap_h #include "Vec.h" //================================================================================================= // A heap implementation with support for decrease/increase key. template class BasicHeap { Comp lt; vec heap; // heap of ints // Index "traversal" functions static inline int left (int i) { return i*2+1; } static inline int right (int i) { return (i+1)*2; } static inline int parent(int i) { return (i-1) >> 1; } inline void percolateUp(int i) { int x = heap[i]; while (i != 0 && lt(x, heap[parent(i)])){ heap[i] = heap[parent(i)]; i = parent(i); } heap [i] = x; } inline void percolateDown(int i) { int x = heap[i]; while (left(i) < heap.size()){ int child = right(i) < heap.size() && lt(heap[right(i)], heap[left(i)]) ? right(i) : left(i); if (!lt(heap[child], x)) break; heap[i] = heap[child]; i = child; } heap[i] = x; } bool heapProperty(int i) { return i >= heap.size() || ((i == 0 || !lt(heap[i], heap[parent(i)])) && heapProperty(left(i)) && heapProperty(right(i))); } public: BasicHeap(const C& c) : comp(c) { } int size () const { return heap.size(); } bool empty () const { return heap.size() == 0; } int operator[](int index) const { return heap[index+1]; } void clear (bool dealloc = false) { heap.clear(dealloc); } void insert (int n) { heap.push(n); percolateUp(heap.size()-1); } int removeMin() { int r = heap[0]; heap[0] = heap.last(); heap.pop(); if (heap.size() > 1) percolateDown(0); return r; } // DEBUG: consistency checking bool heapProperty() { return heapProperty(1); } // COMPAT: should be removed int getmin () { return removeMin(); } }; //================================================================================================= #endif minisat/mtl/Alg.h0000644000177400017740000000402610467344576014126 0ustar boothbyboothby/*******************************************************************************************[Alg.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 Alg_h #define Alg_h //================================================================================================= // Useful functions on vectors #if 1 template static inline void remove(V& ts, const T& t) { int j = 0; for (; j < ts.size() && ts[j] != t; j++); assert(j < ts.size()); for (; j < ts.size()-1; j++) ts[j] = ts[j+1]; ts.pop(); } #else template static inline void remove(V& ts, const T& t) { int j = 0; for (; j < ts.size() && ts[j] != t; j++); assert(j < ts.size()); ts[j] = ts.last(); ts.pop(); } #endif template static inline bool find(V& ts, const T& t) { int j = 0; for (; j < ts.size() && ts[j] != t; j++); return j < ts.size(); } #endif minisat/mtl/Heap.h0000644000177400017740000001226110525172513014261 0ustar boothbyboothby/******************************************************************************************[Heap.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 Heap_h #define Heap_h #include "Vec.h" //================================================================================================= // A heap implementation with support for decrease/increase key. template class Heap { Comp lt; vec heap; // heap of ints vec indices; // int -> index in heap // Index "traversal" functions static inline int left (int i) { return i*2+1; } static inline int right (int i) { return (i+1)*2; } static inline int parent(int i) { return (i-1) >> 1; } inline void percolateUp(int i) { int x = heap[i]; while (i != 0 && lt(x, heap[parent(i)])){ heap[i] = heap[parent(i)]; indices[heap[i]] = i; i = parent(i); } heap [i] = x; indices[x] = i; } inline void percolateDown(int i) { int x = heap[i]; while (left(i) < heap.size()){ int child = right(i) < heap.size() && lt(heap[right(i)], heap[left(i)]) ? right(i) : left(i); if (!lt(heap[child], x)) break; heap[i] = heap[child]; indices[heap[i]] = i; i = child; } heap [i] = x; indices[x] = i; } bool heapProperty (int i) const { return i >= heap.size() || ((i == 0 || !lt(heap[i], heap[parent(i)])) && heapProperty(left(i)) && heapProperty(right(i))); } public: Heap(const Comp& c) : lt(c) { } int size () const { return heap.size(); } bool empty () const { return heap.size() == 0; } bool inHeap (int n) const { return n < indices.size() && indices[n] >= 0; } int operator[](int index) const { assert(index < heap.size()); return heap[index]; } void decrease (int n) { assert(inHeap(n)); percolateUp(indices[n]); } // RENAME WHEN THE DEPRECATED INCREASE IS REMOVED. void increase_ (int n) { assert(inHeap(n)); percolateDown(indices[n]); } void insert(int n) { indices.growTo(n+1, -1); assert(!inHeap(n)); indices[n] = heap.size(); heap.push(n); percolateUp(indices[n]); } int removeMin() { int x = heap[0]; heap[0] = heap.last(); indices[heap[0]] = 0; indices[x] = -1; heap.pop(); if (heap.size() > 1) percolateDown(0); return x; } void clear(bool dealloc = false) { for (int i = 0; i < heap.size(); i++) indices[heap[i]] = -1; #ifdef NDEBUG for (int i = 0; i < indices.size(); i++) assert(indices[i] == -1); #endif heap.clear(dealloc); } // Fool proof variant of insert/decrease/increase void update (int n) { if (!inHeap(n)) insert(n); else { percolateUp(indices[n]); percolateDown(indices[n]); } } // Delete elements from the heap using a given filter function (-object). // *** this could probaly be replaced with a more general "buildHeap(vec&)" method *** template void filter(const F& filt) { int i,j; for (i = j = 0; i < heap.size(); i++) if (filt(heap[i])){ heap[j] = heap[i]; indices[heap[i]] = j++; }else indices[heap[i]] = -1; heap.shrink(i - j); for (int i = heap.size() / 2 - 1; i >= 0; i--) percolateDown(i); assert(heapProperty()); } // DEBUG: consistency checking bool heapProperty() const { return heapProperty(1); } // COMPAT: should be removed void setBounds (int n) { } void increase (int n) { decrease(n); } int getmin () { return removeMin(); } }; //================================================================================================= #endif minisat/mtl/Map.h0000644000177400017740000001054410417171600014117 0ustar boothbyboothby/*******************************************************************************************[Map.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 Map_h #define Map_h #include #include "Vec.h" //================================================================================================= // Default hash/equals functions // template struct Hash { uint32_t operator()(const K& k) const { return hash(k); } }; template struct Equal { bool operator()(const K& k1, const K& k2) const { return k1 == k2; } }; template struct DeepHash { uint32_t operator()(const K* k) const { return hash(*k); } }; template struct DeepEqual { bool operator()(const K* k1, const K* k2) const { return *k1 == *k2; } }; //================================================================================================= // Some primes // static const int nprimes = 25; static const int primes [nprimes] = { 31, 73, 151, 313, 643, 1291, 2593, 5233, 10501, 21013, 42073, 84181, 168451, 337219, 674701, 1349473, 2699299, 5398891, 10798093, 21596719, 43193641, 86387383, 172775299, 345550609, 691101253 }; //================================================================================================= // Hash table implementation of Maps // template, class E = Equal > class Map { struct Pair { K key; D data; }; H hash; E equals; vec* table; int cap; int size; // Don't allow copying (error prone): Map& operator = (Map& other) { assert(0); } Map (Map& other) { assert(0); } int32_t index (const K& k) const { return hash(k) % cap; } void _insert (const K& k, const D& d) { table[index(k)].push(); table[index(k)].last().key = k; table[index(k)].last().data = d; } void rehash () { const vec* old = table; int newsize = primes[0]; for (int i = 1; newsize <= cap && i < nprimes; i++) newsize = primes[i]; table = new vec[newsize]; for (int i = 0; i < cap; i++){ for (int j = 0; j < old[i].size(); j++){ _insert(old[i][j].key, old[i][j].data); }} delete [] old; cap = newsize; } public: Map () : table(NULL), cap(0), size(0) {} Map (const H& h, const E& e) : Map(), hash(h), equals(e) {} ~Map () { delete [] table; } void insert (const K& k, const D& d) { if (size+1 > cap / 2) rehash(); _insert(k, d); size++; } bool peek (const K& k, D& d) { if (size == 0) return false; const vec& ps = table[index(k)]; for (int i = 0; i < ps.size(); i++) if (equals(ps[i].key, k)){ d = ps[i].data; return true; } return false; } void remove (const K& k) { assert(table != NULL); vec& ps = table[index(k)]; int j = 0; for (; j < ps.size() && !equals(ps[j].key, k); j++); assert(j < ps.size()); ps[j] = ps.last(); ps.pop(); } void clear () { cap = size = 0; delete [] table; table = NULL; } }; #endif minisat/mtl/BoxedVec.h0000644000177400017740000001275210501247550015106 0ustar boothbyboothby/*******************************************************************************************[Vec.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 BoxedVec_h #define BoxedVec_h #include #include #include //================================================================================================= // Automatically resizable arrays // // NOTE! Don't use this vector on datatypes that cannot be re-located in memory (with realloc) template class bvec { static inline int imin(int x, int y) { int mask = (x-y) >> (sizeof(int)*8-1); return (x&mask) + (y&(~mask)); } static inline int imax(int x, int y) { int mask = (y-x) >> (sizeof(int)*8-1); return (x&mask) + (y&(~mask)); } struct Vec_t { int sz; int cap; T data[0]; static Vec_t* alloc(Vec_t* x, int size){ x = (Vec_t*)realloc((void*)x, sizeof(Vec_t) + sizeof(T)*size); x->cap = size; return x; } }; Vec_t* ref; static const int init_size = 2; static int nextSize (int current) { return (current * 3 + 1) >> 1; } static int fitSize (int needed) { int x; for (x = init_size; needed > x; x = nextSize(x)); return x; } void fill (int size) { assert(ref != NULL); for (T* i = ref->data; i < ref->data + size; i++) new (i) T(); } void fill (int size, const T& pad) { assert(ref != NULL); for (T* i = ref->data; i < ref->data + size; i++) new (i) T(pad); } // Don't allow copying (error prone): altvec& operator = (altvec& other) { assert(0); } altvec (altvec& other) { assert(0); } public: void clear (bool dealloc = false) { if (ref != NULL){ for (int i = 0; i < ref->sz; i++) (*ref).data[i].~T(); if (dealloc) { free(ref); ref = NULL; }else ref->sz = 0; } } // Constructors: altvec(void) : ref (NULL) { } altvec(int size) : ref (Vec_t::alloc(NULL, fitSize(size))) { fill(size); ref->sz = size; } altvec(int size, const T& pad) : ref (Vec_t::alloc(NULL, fitSize(size))) { fill(size, pad); ref->sz = size; } ~altvec(void) { clear(true); } // Ownership of underlying array: operator T* (void) { return ref->data; } // (unsafe but convenient) operator const T* (void) const { return ref->data; } // Size operations: int size (void) const { return ref != NULL ? ref->sz : 0; } void pop (void) { assert(ref != NULL && ref->sz > 0); int last = --ref->sz; ref->data[last].~T(); } void push (const T& elem) { int size = ref != NULL ? ref->sz : 0; int cap = ref != NULL ? ref->cap : 0; if (size == cap){ cap = cap != 0 ? nextSize(cap) : init_size; ref = Vec_t::alloc(ref, cap); } //new (&ref->data[size]) T(elem); ref->data[size] = elem; ref->sz = size+1; } void push () { int size = ref != NULL ? ref->sz : 0; int cap = ref != NULL ? ref->cap : 0; if (size == cap){ cap = cap != 0 ? nextSize(cap) : init_size; ref = Vec_t::alloc(ref, cap); } new (&ref->data[size]) T(); ref->sz = size+1; } void shrink (int nelems) { for (int i = 0; i < nelems; i++) pop(); } void shrink_(int nelems) { for (int i = 0; i < nelems; i++) pop(); } void growTo (int size) { while (this->size() < size) push(); } void growTo (int size, const T& pad) { while (this->size() < size) push(pad); } void capacity (int size) { growTo(size); } const T& last (void) const { return ref->data[ref->sz-1]; } T& last (void) { return ref->data[ref->sz-1]; } // Vector interface: const T& operator [] (int index) const { return ref->data[index]; } T& operator [] (int index) { return ref->data[index]; } void copyTo(altvec& copy) const { copy.clear(); for (int i = 0; i < size(); i++) copy.push(ref->data[i]); } void moveTo(altvec& dest) { dest.clear(true); dest.ref = ref; ref = NULL; } }; #endif minisat/mtl/Queue.h0000644000177400017740000000624510510201265014464 0ustar boothbyboothby/*****************************************************************************************[Queue.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 Queue_h #define Queue_h #include "Vec.h" //================================================================================================= template class Queue { vec elems; int first; public: Queue(void) : first(0) { } void insert(T x) { elems.push(x); } T peek () const { return elems[first]; } void pop () { first++; } void clear(bool dealloc = false) { elems.clear(dealloc); first = 0; } int size(void) { return elems.size() - first; } //bool has(T x) { for (int i = first; i < elems.size(); i++) if (elems[i] == x) return true; return false; } const T& operator [] (int index) const { return elems[first + index]; } }; //template //class Queue { // vec buf; // int first; // int end; // //public: // typedef T Key; // // Queue() : buf(1), first(0), end(0) {} // // void clear () { buf.shrinkTo(1); first = end = 0; } // int size () { return (end >= first) ? end - first : end - first + buf.size(); } // // T peek () { assert(first != end); return buf[first]; } // void pop () { assert(first != end); first++; if (first == buf.size()) first = 0; } // void insert(T elem) { // INVARIANT: buf[end] is always unused // buf[end++] = elem; // if (end == buf.size()) end = 0; // if (first == end){ // Resize: // vec tmp((buf.size()*3 + 1) >> 1); // //**/printf("queue alloc: %d elems (%.1f MB)\n", tmp.size(), tmp.size() * sizeof(T) / 1000000.0); // int i = 0; // for (int j = first; j < buf.size(); j++) tmp[i++] = buf[j]; // for (int j = 0 ; j < end ; j++) tmp[i++] = buf[j]; // first = 0; // end = buf.size(); // tmp.moveTo(buf); // } // } //}; //================================================================================================= #endif