Compare commits
1 commit
| Author | SHA1 | Date | |
|---|---|---|---|
| 73296d190b |
21 changed files with 4 additions and 3904 deletions
20
LICENSE
20
LICENSE
|
|
@ -1,20 +0,0 @@
|
||||||
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
19
README
|
|
@ -1,19 +0,0 @@
|
||||||
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
|
|
||||||
4
README.md
Normal file
4
README.md
Normal file
|
|
@ -0,0 +1,4 @@
|
||||||
|
# Minisat
|
||||||
|
|
||||||
|
This Git repository holds all major release versions of [Minisat](http://minisat.se/Main.html) plus occasional patches for your convenience.
|
||||||
|
To get a specific version, see the branches of this repository.
|
||||||
344
core/Main.C
344
core/Main.C
|
|
@ -1,344 +0,0 @@
|
||||||
/******************************************************************************************[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
|
|
||||||
}
|
|
||||||
|
|
@ -1,7 +0,0 @@
|
||||||
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
741
core/Solver.C
|
|
@ -1,741 +0,0 @@
|
||||||
/****************************************************************************************[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
302
core/Solver.h
|
|
@ -1,302 +0,0 @@
|
||||||
/****************************************************************************************[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
|
|
||||||
|
|
@ -1,197 +0,0 @@
|
||||||
/***********************************************************************************[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
57
mtl/Alg.h
|
|
@ -1,57 +0,0 @@
|
||||||
/*******************************************************************************************[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
|
|
||||||
|
|
@ -1,98 +0,0 @@
|
||||||
/******************************************************************************************[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
147
mtl/BoxedVec.h
|
|
@ -1,147 +0,0 @@
|
||||||
/*******************************************************************************************[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
169
mtl/Heap.h
|
|
@ -1,169 +0,0 @@
|
||||||
/******************************************************************************************[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
118
mtl/Map.h
|
|
@ -1,118 +0,0 @@
|
||||||
/*******************************************************************************************[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
82
mtl/Queue.h
|
|
@ -1,82 +0,0 @@
|
||||||
/*****************************************************************************************[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
93
mtl/Sort.h
|
|
@ -1,93 +0,0 @@
|
||||||
/******************************************************************************************[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
133
mtl/Vec.h
|
|
@ -1,133 +0,0 @@
|
||||||
/*******************************************************************************************[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
|
|
||||||
|
|
@ -1,90 +0,0 @@
|
||||||
##
|
|
||||||
## 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
415
simp/Main.C
|
|
@ -1,415 +0,0 @@
|
||||||
/******************************************************************************************[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
|
|
||||||
}
|
|
||||||
|
|
||||||
}
|
|
||||||
|
|
@ -1,11 +0,0 @@
|
||||||
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
|
|
||||||
|
|
@ -1,700 +0,0 @@
|
||||||
/************************************************************************************[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);
|
|
||||||
}
|
|
||||||
|
|
@ -1,161 +0,0 @@
|
||||||
/************************************************************************************[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