Compare commits
1 commit
| Author | SHA1 | Date | |
|---|---|---|---|
| 815d583f77 |
20 changed files with 3904 additions and 0 deletions
20
LICENSE
Normal file
20
LICENSE
Normal file
|
|
@ -0,0 +1,20 @@
|
||||||
|
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.
|
||||||
19
README
Normal file
19
README
Normal file
|
|
@ -0,0 +1,19 @@
|
||||||
|
Directory 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
|
||||||
344
core/Main.C
Normal file
344
core/Main.C
Normal file
|
|
@ -0,0 +1,344 @@
|
||||||
|
/******************************************************************************************[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 <ctime>
|
||||||
|
#include <cstring>
|
||||||
|
#include <stdint.h>
|
||||||
|
#include <errno.h>
|
||||||
|
|
||||||
|
#include <signal.h>
|
||||||
|
#include <zlib.h>
|
||||||
|
|
||||||
|
#include "Solver.h"
|
||||||
|
|
||||||
|
/*************************************************************************************/
|
||||||
|
#ifdef _MSC_VER
|
||||||
|
#include <ctime>
|
||||||
|
|
||||||
|
static inline double cpuTime(void) {
|
||||||
|
return (double)clock() / CLOCKS_PER_SEC; }
|
||||||
|
#else
|
||||||
|
|
||||||
|
#include <sys/time.h>
|
||||||
|
#include <sys/resource.h>
|
||||||
|
#include <unistd.h>
|
||||||
|
|
||||||
|
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 <fpu_control.h>
|
||||||
|
#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<class B>
|
||||||
|
static void skipWhitespace(B& in) {
|
||||||
|
while ((*in >= 9 && *in <= 13) || *in == 32)
|
||||||
|
++in; }
|
||||||
|
|
||||||
|
template<class B>
|
||||||
|
static void skipLine(B& in) {
|
||||||
|
for (;;){
|
||||||
|
if (*in == EOF || *in == '\0') return;
|
||||||
|
if (*in == '\n') { ++in; return; }
|
||||||
|
++in; } }
|
||||||
|
|
||||||
|
template<class B>
|
||||||
|
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<class B>
|
||||||
|
static void readClause(B& in, Solver& S, vec<Lit>& 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<class B>
|
||||||
|
static bool match(B& in, char* str) {
|
||||||
|
for (; *str != 0; ++str, ++in)
|
||||||
|
if (*str != *in)
|
||||||
|
return false;
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
template<class B>
|
||||||
|
static void parse_DIMACS_main(B& in, Solver& S) {
|
||||||
|
vec<Lit> 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] <input-file> <result-output-file>\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 = <num> [ 0 - 1 ]\n");
|
||||||
|
reportf(" -rnd-freq = <num> [ 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 ? "<stdin>" : 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
|
||||||
|
}
|
||||||
7
core/Makefile
Normal file
7
core/Makefile
Normal file
|
|
@ -0,0 +1,7 @@
|
||||||
|
MTL = ../mtl
|
||||||
|
CHDRS = $(wildcard *.h) $(wildcard $(MTL)/*.h)
|
||||||
|
EXEC = minisat
|
||||||
|
CFLAGS = -I$(MTL) -Wall -ffloat-store
|
||||||
|
LFLAGS = -lz
|
||||||
|
|
||||||
|
include ../mtl/template.mk
|
||||||
741
core/Solver.C
Normal file
741
core/Solver.C
Normal file
|
|
@ -0,0 +1,741 @@
|
||||||
|
/****************************************************************************************[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 <cmath>
|
||||||
|
|
||||||
|
|
||||||
|
//=================================================================================================
|
||||||
|
// 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<Lit>& 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<Lit>&) (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<Lit>& 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<Lit>& 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<Clause*>& 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<Clause*>& 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<Lit> 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<Lit>& 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);
|
||||||
|
}
|
||||||
|
}
|
||||||
302
core/Solver.h
Normal file
302
core/Solver.h
Normal file
|
|
@ -0,0 +1,302 @@
|
||||||
|
/****************************************************************************************[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 <cstdio>
|
||||||
|
|
||||||
|
#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<Lit>& 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<Lit>& 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<lbool> model; // If problem is satisfiable, this vector contains the model (if any).
|
||||||
|
vec<Lit> conflict; // If problem is unsatisfiable (possibly under assumptions),
|
||||||
|
// this vector represent the 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<double>& activity;
|
||||||
|
bool operator () (Var x, Var y) const { return activity[x] > activity[y]; }
|
||||||
|
VarOrderLt(const vec<double>& 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<Clause*> clauses; // List of problem clauses.
|
||||||
|
vec<Clause*> learnts; // List of learnt clauses.
|
||||||
|
double cla_inc; // Amount to bump next clause with.
|
||||||
|
vec<double> activity; // A heuristic measurement of the activity of a variable.
|
||||||
|
double var_inc; // Amount to bump next variable with.
|
||||||
|
vec<vec<Clause*> > watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
|
||||||
|
vec<char> assigns; // The current assignments (lbool:s stored as char:s).
|
||||||
|
vec<char> polarity; // The preferred polarity of each variable.
|
||||||
|
vec<char> decision_var; // Declares if a variable is eligible for selection in the decision heuristic.
|
||||||
|
vec<Lit> trail; // Assignment stack; stores all assigments made in the order they were made.
|
||||||
|
vec<int> trail_lim; // Separator indices for different decision levels in 'trail'.
|
||||||
|
vec<Clause*> reason; // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none.
|
||||||
|
vec<int> 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<Lit> assumptions; // Current set of assumptions provided to solve by the user.
|
||||||
|
Heap<VarOrderLt> 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<char> seen;
|
||||||
|
vec<Lit> analyze_stack;
|
||||||
|
vec<Lit> analyze_toclear;
|
||||||
|
vec<Lit> 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<Lit>& out_learnt, int& out_btlevel); // (bt = backtrack)
|
||||||
|
void analyzeFinal (Lit p, vec<Lit>& 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<Clause*>& 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<class C>
|
||||||
|
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<Lit> 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<Lit>& ls)
|
||||||
|
{
|
||||||
|
fprintf(f, "[ ");
|
||||||
|
if (ls.size() > 0){
|
||||||
|
logLit(f, ls[0]);
|
||||||
|
for (int i = 1; i < ls.size(); i++){
|
||||||
|
fprintf(f, ", ");
|
||||||
|
logLit(f, ls[i]);
|
||||||
|
}
|
||||||
|
}
|
||||||
|
fprintf(f, "] ");
|
||||||
|
}
|
||||||
|
|
||||||
|
static inline const char* showBool(bool b) { return b ? "true" : "false"; }
|
||||||
|
|
||||||
|
|
||||||
|
// Just like 'assert()' but expression will be evaluated in the release version as well.
|
||||||
|
static inline void check(bool expr) { assert(expr); }
|
||||||
|
|
||||||
|
|
||||||
|
inline void Solver::printLit(Lit l)
|
||||||
|
{
|
||||||
|
reportf("%s%d:%c", sign(l) ? "-" : "", var(l)+1, value(l) == l_True ? '1' : (value(l) == l_False ? '0' : 'X'));
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
template<class C>
|
||||||
|
inline void Solver::printClause(const C& c)
|
||||||
|
{
|
||||||
|
for (int i = 0; i < c.size(); i++){
|
||||||
|
printLit(c[i]);
|
||||||
|
fprintf(stderr, " ");
|
||||||
|
}
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
//=================================================================================================
|
||||||
|
#endif
|
||||||
197
core/SolverTypes.h
Normal file
197
core/SolverTypes.h
Normal file
|
|
@ -0,0 +1,197 @@
|
||||||
|
/***********************************************************************************[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 <cassert>
|
||||||
|
#include <stdint.h>
|
||||||
|
|
||||||
|
//=================================================================================================
|
||||||
|
// 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<class V>
|
||||||
|
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<class V>
|
||||||
|
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
|
||||||
57
mtl/Alg.h
Normal file
57
mtl/Alg.h
Normal file
|
|
@ -0,0 +1,57 @@
|
||||||
|
/*******************************************************************************************[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<class V, class T>
|
||||||
|
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<class V, class T>
|
||||||
|
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<class V, class T>
|
||||||
|
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
|
||||||
98
mtl/BasicHeap.h
Normal file
98
mtl/BasicHeap.h
Normal file
|
|
@ -0,0 +1,98 @@
|
||||||
|
/******************************************************************************************[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 Comp>
|
||||||
|
class BasicHeap {
|
||||||
|
Comp lt;
|
||||||
|
vec<int> 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
|
||||||
147
mtl/BoxedVec.h
Normal file
147
mtl/BoxedVec.h
Normal file
|
|
@ -0,0 +1,147 @@
|
||||||
|
/*******************************************************************************************[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 <cstdlib>
|
||||||
|
#include <cassert>
|
||||||
|
#include <new>
|
||||||
|
|
||||||
|
//=================================================================================================
|
||||||
|
// Automatically resizable arrays
|
||||||
|
//
|
||||||
|
// NOTE! Don't use this vector on datatypes that cannot be re-located in memory (with realloc)
|
||||||
|
|
||||||
|
template<class T>
|
||||||
|
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<T>& operator = (altvec<T>& other) { assert(0); }
|
||||||
|
altvec (altvec<T>& 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<T>& copy) const { copy.clear(); for (int i = 0; i < size(); i++) copy.push(ref->data[i]); }
|
||||||
|
void moveTo(altvec<T>& dest) { dest.clear(true); dest.ref = ref; ref = NULL; }
|
||||||
|
|
||||||
|
};
|
||||||
|
|
||||||
|
|
||||||
|
#endif
|
||||||
169
mtl/Heap.h
Normal file
169
mtl/Heap.h
Normal file
|
|
@ -0,0 +1,169 @@
|
||||||
|
/******************************************************************************************[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 Comp>
|
||||||
|
class Heap {
|
||||||
|
Comp lt;
|
||||||
|
vec<int> heap; // heap of ints
|
||||||
|
vec<int> 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<int>&)" method ***
|
||||||
|
template <class F>
|
||||||
|
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
|
||||||
118
mtl/Map.h
Normal file
118
mtl/Map.h
Normal file
|
|
@ -0,0 +1,118 @@
|
||||||
|
/*******************************************************************************************[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 <stdint.h>
|
||||||
|
|
||||||
|
#include "Vec.h"
|
||||||
|
|
||||||
|
//=================================================================================================
|
||||||
|
// Default hash/equals functions
|
||||||
|
//
|
||||||
|
|
||||||
|
template<class K> struct Hash { uint32_t operator()(const K& k) const { return hash(k); } };
|
||||||
|
template<class K> struct Equal { bool operator()(const K& k1, const K& k2) const { return k1 == k2; } };
|
||||||
|
|
||||||
|
template<class K> struct DeepHash { uint32_t operator()(const K* k) const { return hash(*k); } };
|
||||||
|
template<class K> 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 K, class D, class H = Hash<K>, class E = Equal<K> >
|
||||||
|
class Map {
|
||||||
|
struct Pair { K key; D data; };
|
||||||
|
|
||||||
|
H hash;
|
||||||
|
E equals;
|
||||||
|
|
||||||
|
vec<Pair>* table;
|
||||||
|
int cap;
|
||||||
|
int size;
|
||||||
|
|
||||||
|
// Don't allow copying (error prone):
|
||||||
|
Map<K,D,H,E>& operator = (Map<K,D,H,E>& other) { assert(0); }
|
||||||
|
Map (Map<K,D,H,E>& 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<Pair>* old = table;
|
||||||
|
|
||||||
|
int newsize = primes[0];
|
||||||
|
for (int i = 1; newsize <= cap && i < nprimes; i++)
|
||||||
|
newsize = primes[i];
|
||||||
|
|
||||||
|
table = new vec<Pair>[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<Pair>& 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<Pair>& 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
|
||||||
82
mtl/Queue.h
Normal file
82
mtl/Queue.h
Normal file
|
|
@ -0,0 +1,82 @@
|
||||||
|
/*****************************************************************************************[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 T>
|
||||||
|
class Queue {
|
||||||
|
vec<T> 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 T>
|
||||||
|
//class Queue {
|
||||||
|
// vec<T> 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<T> 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
|
||||||
93
mtl/Sort.h
Normal file
93
mtl/Sort.h
Normal file
|
|
@ -0,0 +1,93 @@
|
||||||
|
/******************************************************************************************[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<class T>
|
||||||
|
struct LessThan_default {
|
||||||
|
bool operator () (T x, T y) { return x < y; }
|
||||||
|
};
|
||||||
|
|
||||||
|
|
||||||
|
template <class T, class LessThan>
|
||||||
|
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 <class T> static inline void selectionSort(T* array, int size) {
|
||||||
|
selectionSort(array, size, LessThan_default<T>()); }
|
||||||
|
|
||||||
|
template <class T, class LessThan>
|
||||||
|
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 <class T> static inline void sort(T* array, int size) {
|
||||||
|
sort(array, size, LessThan_default<T>()); }
|
||||||
|
|
||||||
|
|
||||||
|
//=================================================================================================
|
||||||
|
// For 'vec's:
|
||||||
|
|
||||||
|
|
||||||
|
template <class T, class LessThan> void sort(vec<T>& v, LessThan lt) {
|
||||||
|
sort((T*)v, v.size(), lt); }
|
||||||
|
template <class T> void sort(vec<T>& v) {
|
||||||
|
sort(v, LessThan_default<T>()); }
|
||||||
|
|
||||||
|
|
||||||
|
//=================================================================================================
|
||||||
|
#endif
|
||||||
133
mtl/Vec.h
Normal file
133
mtl/Vec.h
Normal file
|
|
@ -0,0 +1,133 @@
|
||||||
|
/*******************************************************************************************[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 <cstdlib>
|
||||||
|
#include <cassert>
|
||||||
|
#include <new>
|
||||||
|
|
||||||
|
//=================================================================================================
|
||||||
|
// Automatically resizable arrays
|
||||||
|
//
|
||||||
|
// NOTE! Don't use this vector on datatypes that cannot be re-located in memory (with realloc)
|
||||||
|
|
||||||
|
template<class T>
|
||||||
|
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<T>& operator = (vec<T>& other) { assert(0); return *this; }
|
||||||
|
vec (vec<T>& 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<T>& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) new (©[i]) T(data[i]); }
|
||||||
|
void moveTo(vec<T>& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; }
|
||||||
|
};
|
||||||
|
|
||||||
|
template<class T>
|
||||||
|
void vec<T>::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<class T>
|
||||||
|
void vec<T>::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<class T>
|
||||||
|
void vec<T>::growTo(int size) {
|
||||||
|
if (sz >= size) return;
|
||||||
|
grow(size);
|
||||||
|
for (int i = sz; i < size; i++) new (&data[i]) T();
|
||||||
|
sz = size; }
|
||||||
|
|
||||||
|
template<class T>
|
||||||
|
void vec<T>::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
|
||||||
90
mtl/template.mk
Normal file
90
mtl/template.mk
Normal file
|
|
@ -0,0 +1,90 @@
|
||||||
|
##
|
||||||
|
## 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
|
||||||
415
simp/Main.C
Normal file
415
simp/Main.C
Normal file
|
|
@ -0,0 +1,415 @@
|
||||||
|
/******************************************************************************************[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 <ctime>
|
||||||
|
#include <cstring>
|
||||||
|
#include <stdint.h>
|
||||||
|
#include <errno.h>
|
||||||
|
|
||||||
|
#include <signal.h>
|
||||||
|
#include <zlib.h>
|
||||||
|
|
||||||
|
#include "SimpSolver.h"
|
||||||
|
|
||||||
|
/*************************************************************************************/
|
||||||
|
#ifdef _MSC_VER
|
||||||
|
#include <ctime>
|
||||||
|
|
||||||
|
static inline double cpuTime(void) {
|
||||||
|
return (double)clock() / CLOCKS_PER_SEC; }
|
||||||
|
#else
|
||||||
|
|
||||||
|
#include <sys/time.h>
|
||||||
|
#include <sys/resource.h>
|
||||||
|
#include <unistd.h>
|
||||||
|
|
||||||
|
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 <fpu_control.h>
|
||||||
|
#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<class B>
|
||||||
|
static void skipWhitespace(B& in) {
|
||||||
|
while ((*in >= 9 && *in <= 13) || *in == 32)
|
||||||
|
++in; }
|
||||||
|
|
||||||
|
template<class B>
|
||||||
|
static void skipLine(B& in) {
|
||||||
|
for (;;){
|
||||||
|
if (*in == EOF || *in == '\0') return;
|
||||||
|
if (*in == '\n') { ++in; return; }
|
||||||
|
++in; } }
|
||||||
|
|
||||||
|
template<class B>
|
||||||
|
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<class B>
|
||||||
|
static void readClause(B& in, SimpSolver& S, vec<Lit>& 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<class B>
|
||||||
|
static bool match(B& in, char* str) {
|
||||||
|
for (; *str != 0; ++str, ++in)
|
||||||
|
if (*str != *in)
|
||||||
|
return false;
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
template<class B>
|
||||||
|
static void parse_DIMACS_main(B& in, SimpSolver& S) {
|
||||||
|
vec<Lit> 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] <input-file> <result-output-file>\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 = <num> [ >0 ]\n");
|
||||||
|
reportf(" -polarity-mode = {true,false,rnd}\n");
|
||||||
|
reportf(" -decay = <num> [ 0 - 1 ]\n");
|
||||||
|
reportf(" -rnd-freq = <num> [ 0 - 1 ]\n");
|
||||||
|
reportf(" -dimacs = <output-file>\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 ? "<stdin>" : 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
|
||||||
|
}
|
||||||
|
|
||||||
|
}
|
||||||
11
simp/Makefile
Normal file
11
simp/Makefile
Normal file
|
|
@ -0,0 +1,11 @@
|
||||||
|
MTL = ../mtl
|
||||||
|
CORE = ../core
|
||||||
|
CHDRS = $(wildcard *.h) $(wildcard $(MTL)/*.h)
|
||||||
|
EXEC = minisat
|
||||||
|
CFLAGS = -I$(MTL) -I$(CORE) -Wall -ffloat-store
|
||||||
|
LFLAGS = -lz
|
||||||
|
|
||||||
|
CSRCS = $(wildcard *.C)
|
||||||
|
COBJS = $(addsuffix .o, $(basename $(CSRCS))) $(CORE)/Solver.o
|
||||||
|
|
||||||
|
include ../mtl/template.mk
|
||||||
700
simp/SimpSolver.C
Normal file
700
simp/SimpSolver.C
Normal file
|
|
@ -0,0 +1,700 @@
|
||||||
|
/************************************************************************************[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<Lit> 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<Lit>& assumps, bool do_simp, bool turn_off_simp) {
|
||||||
|
vec<Var> 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<Lit>& 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<Lit>& out_clause)
|
||||||
|
{
|
||||||
|
merges++;
|
||||||
|
out_clause.clear();
|
||||||
|
|
||||||
|
bool ps_smallest = _ps.size() < _qs.size();
|
||||||
|
const Clause& ps = ps_smallest ? _qs : _ps;
|
||||||
|
const Clause& qs = ps_smallest ? _ps : _qs;
|
||||||
|
|
||||||
|
for (int i = 0; i < qs.size(); i++){
|
||||||
|
if (var(qs[i]) != v){
|
||||||
|
for (int j = 0; j < ps.size(); j++)
|
||||||
|
if (var(ps[j]) == var(qs[i]))
|
||||||
|
if (ps[j] == ~qs[i])
|
||||||
|
return false;
|
||||||
|
else
|
||||||
|
goto next;
|
||||||
|
out_clause.push(qs[i]);
|
||||||
|
}
|
||||||
|
next:;
|
||||||
|
}
|
||||||
|
|
||||||
|
for (int i = 0; i < ps.size(); i++)
|
||||||
|
if (var(ps[i]) != v)
|
||||||
|
out_clause.push(ps[i]);
|
||||||
|
|
||||||
|
return true;
|
||||||
|
}
|
||||||
|
|
||||||
|
|
||||||
|
// Returns FALSE if clause is always satisfied.
|
||||||
|
bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v)
|
||||||
|
{
|
||||||
|
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<Clause*>& 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<Lit>& c)
|
||||||
|
{
|
||||||
|
assert(decisionLevel() == 0);
|
||||||
|
|
||||||
|
trail_lim.push(trail.size());
|
||||||
|
for (int i = 0; i < c.size(); i++)
|
||||||
|
if (value(c[i]) == l_True){
|
||||||
|
cancelUntil(0);
|
||||||
|
return false;
|
||||||
|
}else if (value(c[i]) != l_False){
|
||||||
|
assert(value(c[i]) == l_Undef);
|
||||||
|
uncheckedEnqueue(~c[i]);
|
||||||
|
}
|
||||||
|
|
||||||
|
bool result = propagate() != 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<Clause*>& _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<Clause*> pos, neg;
|
||||||
|
const vec<Clause*>& 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<Clause*>& 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<Clause*> 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<Lit> 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<Lit> 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<Var> 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<Var> 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);
|
||||||
|
}
|
||||||
161
simp/SimpSolver.h
Normal file
161
simp/SimpSolver.h
Normal file
|
|
@ -0,0 +1,161 @@
|
||||||
|
/************************************************************************************[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 <cstdio>
|
||||||
|
|
||||||
|
#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<Lit>& ps);
|
||||||
|
|
||||||
|
// Variable mode:
|
||||||
|
//
|
||||||
|
void setFrozen (Var v, bool b); // If a variable is frozen it will not be eliminated.
|
||||||
|
|
||||||
|
// Solving:
|
||||||
|
//
|
||||||
|
bool solve (const vec<Lit>& assumps, bool do_simp = true, bool turn_off_simp = false);
|
||||||
|
bool solve (bool do_simp = true, bool turn_off_simp = false);
|
||||||
|
bool 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<Clause*> eliminated;
|
||||||
|
ElimData() : order(0) {} };
|
||||||
|
|
||||||
|
struct ElimOrderLt {
|
||||||
|
const vec<ElimData>& elimtable;
|
||||||
|
ElimOrderLt(const vec<ElimData>& et) : elimtable(et) {}
|
||||||
|
bool operator()(Var x, Var y) { return elimtable[x].order > elimtable[y].order; } };
|
||||||
|
|
||||||
|
struct ElimLt {
|
||||||
|
const vec<int>& n_occ;
|
||||||
|
ElimLt(const vec<int>& no) : n_occ(no) {}
|
||||||
|
int cost (Var x) const { return n_occ[toInt(Lit(x))] * n_occ[toInt(~Lit(x))]; }
|
||||||
|
bool operator()(Var x, Var y) const { return cost(x) < cost(y); } };
|
||||||
|
|
||||||
|
|
||||||
|
// Solver state:
|
||||||
|
//
|
||||||
|
int elimorder;
|
||||||
|
bool use_simplification;
|
||||||
|
vec<ElimData> elimtable;
|
||||||
|
vec<char> touched;
|
||||||
|
vec<vec<Clause*> > occurs;
|
||||||
|
vec<int> n_occ;
|
||||||
|
Heap<ElimLt> elim_heap;
|
||||||
|
Queue<Clause*> subsumption_queue;
|
||||||
|
vec<char> 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<Clause*>& getOccurs (Var x);
|
||||||
|
void gatherTouchedClauses ();
|
||||||
|
bool merge (const Clause& _ps, const Clause& _qs, Var v, vec<Lit>& out_clause);
|
||||||
|
bool merge (const Clause& _ps, const Clause& _qs, Var v);
|
||||||
|
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<Lit>& 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<Clause*>& 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<Lit> tmp; return solve(tmp, do_simp, turn_off_simp); }
|
||||||
|
|
||||||
|
//=================================================================================================
|
||||||
|
#endif
|
||||||
Loading…
Reference in a new issue