From: bdemsky Date: Wed, 31 Dec 2014 08:11:17 +0000 (+0900) Subject: Incremental frontend for glucose solver X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satlib.git;a=commitdiff_plain;h=f43befe4da7618bfda6720be15e3804914c38ac7 Incremental frontend for glucose solver --- diff --git a/glucose-syrup/incremental/Main.cc b/glucose-syrup/incremental/Main.cc new file mode 100644 index 0000000..5ea6c13 --- /dev/null +++ b/glucose-syrup/incremental/Main.cc @@ -0,0 +1,281 @@ + +#include "solver_interface.h" +#include + +#include +#include +#include + +#include "utils/System.h" +#include "utils/ParseUtils.h" +#include "utils/Options.h" +#include "core/Dimacs.h" +#include "simp/SimpSolver.h" + +using namespace Glucose; + + +static const char* _certified = "CORE -- CERTIFIED UNSAT"; + +void printStats(Solver& solver) +{ + double cpu_time = cpuTime(); + double mem_used = 0;//memUsedPeak(); + printf("c restarts : %" PRIu64" (%" PRIu64" conflicts in avg)\n", solver.starts,(solver.starts>0 ?solver.conflicts/solver.starts : 0)); + printf("c blocked restarts : %" PRIu64" (multiple: %" PRIu64") \n", solver.nbstopsrestarts,solver.nbstopsrestartssame); + printf("c last block at restart : %" PRIu64"\n",solver.lastblockatrestart); + printf("c nb ReduceDB : %" PRIu64"\n", solver.nbReduceDB); + printf("c nb removed Clauses : %" PRIu64"\n",solver.nbRemovedClauses); + printf("c nb learnts DL2 : %" PRIu64"\n", solver.nbDL2); + printf("c nb learnts size 2 : %" PRIu64"\n", solver.nbBin); + printf("c nb learnts size 1 : %" PRIu64"\n", solver.nbUn); + + printf("c conflicts : %-12" PRIu64" (%.0f /sec)\n", solver.conflicts , solver.conflicts /cpu_time); + printf("c decisions : %-12" PRIu64" (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions /cpu_time); + printf("c propagations : %-12" PRIu64" (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time); + printf("c conflict literals : %-12" PRIu64" (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals); + printf("c nb reduced Clauses : %" PRIu64"\n",solver.nbReducedClauses); + + if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used); + printf("c CPU time : %g s\n", cpu_time); +} + + + +static Solver* solver; +// Terminate by notifying the solver and back out gracefully. This is mainly to have a test-case +// for this feature of the Solver as it may take longer than an immediate call to '_exit()'. +static void SIGINT_interrupt(int signum) { solver->interrupt(); } + +// Note that '_exit()' rather than 'exit()' has to be used. The reason is that 'exit()' calls +// destructors and may cause deadlocks if a malloc/free function happens to be running (these +// functions are guarded by locks for multithreaded use). +static void SIGINT_exit(int signum) { + printf("\n"); printf("*** INTERRUPTED ***\n"); + if (solver->verbosity > 0){ + printStats(*solver); + printf("\n"); printf("*** INTERRUPTED ***\n"); } + _exit(1); } + + +int *buffer; +int length; +int offset; + +int *outbuffer; +int outoffset; + +int getInt() { + if (offset>=length) { + ssize_t ptr; + offset = 0; + do { + ptr=read(0, buffer, sizeof(int)*IS_BUFFERSIZE); + if (ptr == -1) + exit(-1); + } while(ptr==0); + ssize_t bytestoread=(4-(ptr & 3)) & 3; + while(bytestoread != 0) { + ssize_t p=read(0, &((char *)buffer)[ptr], bytestoread); + if (p == -1) + exit(-1); + bytestoread -= p; + ptr += p; + } + length = ptr / 4; + offset = 0; + } + + return buffer[offset++]; +} + +void flushInts() { + ssize_t bytestowrite=sizeof(int)*outoffset; + ssize_t byteswritten=0; + do { + ssize_t n=write(IS_OUT_FD, &((char *)outbuffer)[byteswritten], bytestowrite); + if (n == -1) { + fprintf(stderr, "Write failure\n"); + exit(-1); + } + bytestowrite -= n; + byteswritten += n; + } while(bytestowrite != 0); + outoffset = 0; +} + +void putInt(int value) { + if (outoffset>=IS_BUFFERSIZE) { + flushInts(); + } + outbuffer[outoffset++]=value; +} + +void readClauses(Solver *solver) { + vec clause; + int numvars = solver->nVars(); + bool haveClause = false; + while(true) { + int lit=getInt(); + if (lit!=0) { + int var = abs(lit) - 1; + while (var >= numvars) { + numvars++; + solver->newVar(); + } + clause.push( (lit>0) ? mkLit(var) : ~mkLit(var)); + haveClause = true; + } else { + if (haveClause) { + solver->addClause_(clause); + haveClause = false; + clause.clear(); + } else { + //done with clauses + return; + } + } + } +} + +void processCommands(SimpSolver *solver) { + while(true) { + int command=getInt(); + switch(command) { + case IS_FREEZE: { + int var=getInt()-1; + solver->setFrozen(var, true); + break; + } + case IS_RUNSOLVER: { + vec dummy; + lbool ret = solver->solveLimited(dummy); + if (ret == l_True) { + putInt(IS_SAT); + putInt(solver->nVars()); + for(int i=0;inVars();i++) { + putInt(solver->model[i]==l_True); + } + } else if (ret == l_False) { + putInt(IS_UNSAT); + } else { + putInt(IS_INDETER); + } + flushInts(); + return; + } + default: + fprintf(stderr, "Unreconized command\n"); + exit(-1); + } + } +} + +void processSAT(SimpSolver *solver) { + buffer=(int *) malloc(sizeof(int)*IS_BUFFERSIZE); + offset=0; + length=0; + outbuffer=(int *) malloc(sizeof(int)*IS_BUFFERSIZE); + outoffset=0; + + while(true) { + double initial_time = cpuTime(); + readClauses(solver); + double parse_time = cpuTime(); + processCommands(solver); + double finish_time = cpuTime(); + printf("Parse time: %12.2f s Solve time:%12.2f s\n", parse_time-initial_time, finish_time-parse_time); + } +} + + + +//================================================================================================= +// Main: + +int main(int argc, char** argv) { + try { + printf("c\nc This is glucose 4.0 -- based on MiniSAT (Many thanks to MiniSAT team)\nc\n"); + + + setUsageHelp("c USAGE: %s [options] \n\n where input may be either in plain or gzipped DIMACS.\n"); + + +#if defined(__linux__) + fpu_control_t oldcw, newcw; + _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw); + //printf("c WARNING: for repeatability, setting FPU to use double precision\n"); +#endif + // Extra options: + // + IntOption verb ("MAIN", "verb", "Verbosity level (0=silent, 1=some, 2=more).", 1, IntRange(0, 2)); + BoolOption mod ("MAIN", "model", "show model.", false); + IntOption vv ("MAIN", "vv", "Verbosity every vv conflicts", 10000, IntRange(1,INT32_MAX)); + BoolOption pre ("MAIN", "pre", "Completely turn on/off any preprocessing.", true); + StringOption dimacs ("MAIN", "dimacs", "If given, stop after preprocessing and write the result to this file."); + IntOption cpu_lim("MAIN", "cpu-lim","Limit on CPU time allowed in seconds.\n", INT32_MAX, IntRange(0, INT32_MAX)); + IntOption mem_lim("MAIN", "mem-lim","Limit on memory usage in megabytes.\n", INT32_MAX, IntRange(0, INT32_MAX)); + + BoolOption opt_certified (_certified, "certified", "Certified UNSAT using DRUP format", false); + StringOption opt_certified_file (_certified, "certified-output", "Certified UNSAT output file", "NULL"); + + parseOptions(argc, argv, true); + + SimpSolver S; + S.parsing = 1; + S.verbosity = verb; + S.verbEveryConflicts = vv; + S.showModel = mod; + solver = &S; + // Use signal handlers that forcibly quit until the solver will be + // able to respond to interrupts: + signal(SIGINT, SIGINT_exit); + signal(SIGXCPU,SIGINT_exit); + + + // Set limit on CPU-time: + if (cpu_lim != INT32_MAX){ + rlimit rl; + getrlimit(RLIMIT_CPU, &rl); + if (rl.rlim_max == RLIM_INFINITY || (rlim_t)cpu_lim < rl.rlim_max){ + rl.rlim_cur = cpu_lim; + if (setrlimit(RLIMIT_CPU, &rl) == -1) + printf("c WARNING! Could not set resource limit: CPU-time.\n"); + } } + + // Set limit on virtual memory: + if (mem_lim != INT32_MAX){ + rlim_t new_mem_lim = (rlim_t)mem_lim * 1024*1024; + rlimit rl; + getrlimit(RLIMIT_AS, &rl); + if (rl.rlim_max == RLIM_INFINITY || new_mem_lim < rl.rlim_max){ + rl.rlim_cur = new_mem_lim; + if (setrlimit(RLIMIT_AS, &rl) == -1) + printf("c WARNING! Could not set resource limit: Virtual memory.\n"); + } } + + //do solver stuff here + processSAT(&S); + + printf("c | Number of variables: %12d |\n", S.nVars()); + printf("c | Number of clauses: %12d |\n", S.nClauses()); + + + // Change to signal-handlers that will only notify the solver and allow it to terminate + // voluntarily: + signal(SIGINT, SIGINT_interrupt); + signal(SIGXCPU,SIGINT_interrupt); + + S.parsing = 0; + +#ifdef NDEBUG + exit(0); +#else + return (0); +#endif + } catch (OutOfMemoryException&){ + printf("c =========================================================================================================\n"); + printf("INDETERMINATE\n"); + exit(0); + } +} diff --git a/glucose-syrup/incremental/Main.cc~ b/glucose-syrup/incremental/Main.cc~ new file mode 100644 index 0000000..2996afd --- /dev/null +++ b/glucose-syrup/incremental/Main.cc~ @@ -0,0 +1,260 @@ + +#include "solver_interface.h" +#include + +#include +#include +#include + +#include "utils/System.h" +#include "utils/ParseUtils.h" +#include "utils/Options.h" +#include "core/Dimacs.h" +#include "simp/SimpSolver.h" + +using namespace Glucose; + + +static const char* _certified = "CORE -- CERTIFIED UNSAT"; + +void printStats(Solver& solver) +{ + double cpu_time = cpuTime(); + double mem_used = 0;//memUsedPeak(); + printf("c restarts : %" PRIu64" (%" PRIu64" conflicts in avg)\n", solver.starts,(solver.starts>0 ?solver.conflicts/solver.starts : 0)); + printf("c blocked restarts : %" PRIu64" (multiple: %" PRIu64") \n", solver.nbstopsrestarts,solver.nbstopsrestartssame); + printf("c last block at restart : %" PRIu64"\n",solver.lastblockatrestart); + printf("c nb ReduceDB : %" PRIu64"\n", solver.nbReduceDB); + printf("c nb removed Clauses : %" PRIu64"\n",solver.nbRemovedClauses); + printf("c nb learnts DL2 : %" PRIu64"\n", solver.nbDL2); + printf("c nb learnts size 2 : %" PRIu64"\n", solver.nbBin); + printf("c nb learnts size 1 : %" PRIu64"\n", solver.nbUn); + + printf("c conflicts : %-12" PRIu64" (%.0f /sec)\n", solver.conflicts , solver.conflicts /cpu_time); + printf("c decisions : %-12" PRIu64" (%4.2f %% random) (%.0f /sec)\n", solver.decisions, (float)solver.rnd_decisions*100 / (float)solver.decisions, solver.decisions /cpu_time); + printf("c propagations : %-12" PRIu64" (%.0f /sec)\n", solver.propagations, solver.propagations/cpu_time); + printf("c conflict literals : %-12" PRIu64" (%4.2f %% deleted)\n", solver.tot_literals, (solver.max_literals - solver.tot_literals)*100 / (double)solver.max_literals); + printf("c nb reduced Clauses : %" PRIu64"\n",solver.nbReducedClauses); + + if (mem_used != 0) printf("Memory used : %.2f MB\n", mem_used); + printf("c CPU time : %g s\n", cpu_time); +} + + + +static Solver* solver; +// Terminate by notifying the solver and back out gracefully. This is mainly to have a test-case +// for this feature of the Solver as it may take longer than an immediate call to '_exit()'. +static void SIGINT_interrupt(int signum) { solver->interrupt(); } + +// Note that '_exit()' rather than 'exit()' has to be used. The reason is that 'exit()' calls +// destructors and may cause deadlocks if a malloc/free function happens to be running (these +// functions are guarded by locks for multithreaded use). +static void SIGINT_exit(int signum) { + printf("\n"); printf("*** INTERRUPTED ***\n"); + if (solver->verbosity > 0){ + printStats(*solver); + printf("\n"); printf("*** INTERRUPTED ***\n"); } + _exit(1); } + + +int *buffer; +int length; +int offset; + +int getInt() { + if (offset>=length) { + ssize_t ptr; + offset = 0; + do { + ptr=read(0, buffer, sizeof(int)*IS_BUFFERSIZE); + if (ptr == -1) + exit(-1); + } while(ptr==0); + ssize bytestoread=(4-(ptr & 3)) & 3; + while(bytestoread != 0) { + ssize_t p=read(0, &((char *)buffer)[ptr], bytestoread); + if (p == -1) + exit(-1); + bytestoread -= p; + ptr += p; + } + length = ptr / 4; + offset = 0; + } + + return buffer[offset++]; +} + +void putInt(int value) { +} + +void readClauses(Solver *solver) { + vec clause; + int numvars = solver->nVars(); + bool haveClause = false; + while(true) { + int lit=getInt(); + if (lit!=0) { + int var = abs(lit) - 1; + while (var >= numvars) { + numvars++; + solver->newVar(); + } + clause.push( (lit>0) ? mkLit(var) : ~mkLit(var)); + haveClause = true; + } else { + if (haveClause) { + solver->addClause_(clause); + haveClause = false; + clause.clear(); + } else { + //done with clauses + return; + } + } + } +} + +void processCommands(Solver *solver) { + while(true) { + int command=getInt(); + switch(command) { + case IS_FREEZE: + int var=getInt(); + solver->setFrozen(var, true); + break; + case IS_RUNSOLVER: { + vec dummy; + lbool ret = solver->solveLimited(dummy); + if (ret == l_True) { + putInt(IS_SAT); + putInt(solver->nVars()); + for(int i=0;inVars();i++) { + putInt(solver->model[i]==l_True); + } + } else if (ret == l_False) { + putInt(IS_UNSAT); + } else { + putInt(IS_INDETER); + } + flushInts(); + return; + } + default: + fprintf(stderr, "Unreconized command\n"); + exit(-1); + } + } +} + +void processSAT(Solver *solver) { + buffer=(int *) malloc(sizeof(int)*BUFFERSIZE); + offset=0; + length=0; + + while(true) { + double initial_time = cpuTime(); + readClauses(solver); + double parse_time = cpuTime(); + processCommands(solver); + double finish_time = cpuTime(); + + } +} + + + +//================================================================================================= +// Main: + +int main(int argc, char** argv) { + try { + printf("c\nc This is glucose 4.0 -- based on MiniSAT (Many thanks to MiniSAT team)\nc\n"); + + + setUsageHelp("c USAGE: %s [options] \n\n where input may be either in plain or gzipped DIMACS.\n"); + + +#if defined(__linux__) + fpu_control_t oldcw, newcw; + _FPU_GETCW(oldcw); newcw = (oldcw & ~_FPU_EXTENDED) | _FPU_DOUBLE; _FPU_SETCW(newcw); + //printf("c WARNING: for repeatability, setting FPU to use double precision\n"); +#endif + // Extra options: + // + IntOption verb ("MAIN", "verb", "Verbosity level (0=silent, 1=some, 2=more).", 1, IntRange(0, 2)); + BoolOption mod ("MAIN", "model", "show model.", false); + IntOption vv ("MAIN", "vv", "Verbosity every vv conflicts", 10000, IntRange(1,INT32_MAX)); + BoolOption pre ("MAIN", "pre", "Completely turn on/off any preprocessing.", true); + StringOption dimacs ("MAIN", "dimacs", "If given, stop after preprocessing and write the result to this file."); + IntOption cpu_lim("MAIN", "cpu-lim","Limit on CPU time allowed in seconds.\n", INT32_MAX, IntRange(0, INT32_MAX)); + IntOption mem_lim("MAIN", "mem-lim","Limit on memory usage in megabytes.\n", INT32_MAX, IntRange(0, INT32_MAX)); + + BoolOption opt_certified (_certified, "certified", "Certified UNSAT using DRUP format", false); + StringOption opt_certified_file (_certified, "certified-output", "Certified UNSAT output file", "NULL"); + + parseOptions(argc, argv, true); + + SimpSolver S; + S.parsing = 1; + S.verbosity = verb; + S.verbEveryConflicts = vv; + S.showModel = mod; + solver = &S; + // Use signal handlers that forcibly quit until the solver will be + // able to respond to interrupts: + signal(SIGINT, SIGINT_exit); + signal(SIGXCPU,SIGINT_exit); + + + // Set limit on CPU-time: + if (cpu_lim != INT32_MAX){ + rlimit rl; + getrlimit(RLIMIT_CPU, &rl); + if (rl.rlim_max == RLIM_INFINITY || (rlim_t)cpu_lim < rl.rlim_max){ + rl.rlim_cur = cpu_lim; + if (setrlimit(RLIMIT_CPU, &rl) == -1) + printf("c WARNING! Could not set resource limit: CPU-time.\n"); + } } + + // Set limit on virtual memory: + if (mem_lim != INT32_MAX){ + rlim_t new_mem_lim = (rlim_t)mem_lim * 1024*1024; + rlimit rl; + getrlimit(RLIMIT_AS, &rl); + if (rl.rlim_max == RLIM_INFINITY || new_mem_lim < rl.rlim_max){ + rl.rlim_cur = new_mem_lim; + if (setrlimit(RLIMIT_AS, &rl) == -1) + printf("c WARNING! Could not set resource limit: Virtual memory.\n"); + } } + + //do solver stuff here + processSAT(&S); + + printf("c | Number of variables: %12d |\n", S.nVars()); + printf("c | Number of clauses: %12d |\n", S.nClauses()); + + double parsed_time = cpuTime(); + if (S.verbosity > 0){ + printf("c | Parse time: %12.2f s |\n", parsed_time - initial_time); + printf("c | |\n"); } + + // Change to signal-handlers that will only notify the solver and allow it to terminate + // voluntarily: + signal(SIGINT, SIGINT_interrupt); + signal(SIGXCPU,SIGINT_interrupt); + + S.parsing = 0; + +#ifdef NDEBUG + exit(ret == l_True ? 10 : ret == l_False ? 20 : 0); // (faster than "return", which will invoke the destructor for 'Solver') +#else + return (ret == l_True ? 10 : ret == l_False ? 20 : 0); +#endif + } catch (OutOfMemoryException&){ + printf("c =========================================================================================================\n"); + printf("INDETERMINATE\n"); + exit(0); + } +} diff --git a/glucose-syrup/incremental/Main.o b/glucose-syrup/incremental/Main.o new file mode 100644 index 0000000..093f726 Binary files /dev/null and b/glucose-syrup/incremental/Main.o differ diff --git a/glucose-syrup/incremental/Makefile b/glucose-syrup/incremental/Makefile new file mode 100644 index 0000000..bcb46fa --- /dev/null +++ b/glucose-syrup/incremental/Makefile @@ -0,0 +1,5 @@ +EXEC = glucose +DEPDIR = mtl utils core +MROOT = $(PWD)/.. +CFLAGS = -I ../.. +include $(MROOT)/mtl/template.mk diff --git a/glucose-syrup/incremental/Makefile~ b/glucose-syrup/incremental/Makefile~ new file mode 100644 index 0000000..f5d4481 --- /dev/null +++ b/glucose-syrup/incremental/Makefile~ @@ -0,0 +1,5 @@ +EXEC = glucose +DEPDIR = mtl utils core +MROOT = $(PWD)/.. + +include $(MROOT)/mtl/template.mk diff --git a/glucose-syrup/incremental/SimpSolver.cc b/glucose-syrup/incremental/SimpSolver.cc new file mode 100644 index 0000000..84bc725 --- /dev/null +++ b/glucose-syrup/incremental/SimpSolver.cc @@ -0,0 +1,826 @@ +/***************************************************************************************[SimpSolver.cc] + Glucose -- Copyright (c) 2009-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + LRI - Univ. Paris Sud, France (2009-2013) + Labri - Univ. Bordeaux, France + + Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + Labri - Univ. Bordeaux, France + +Glucose sources are based on MiniSat (see below MiniSat copyrights). Permissions and copyrights of +Glucose (sources until 2013, Glucose 3.0, single core) are exactly the same as Minisat on which it +is based on. (see below). + +Glucose-Syrup sources are based on another copyright. Permissions and copyrights for the parallel +version of Glucose-Syrup (the "Software") are granted, free of charge, to deal with the Software +without restriction, including the rights to use, copy, modify, merge, publish, distribute, +sublicence, 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 and below copyrights notices and this permission notice shall be included in all +copies or substantial portions of the Software; +- The parallel version of Glucose (all files modified since Glucose 3.0 releases, 2013) cannot +be used in any competitive event (sat competitions/evaluations) without the express permission of +the authors (Gilles Audemard / Laurent Simon). This is also the case for any competitive event +using Glucose Parallel as an embedded SAT engine (single core or not). + + +--------------- Original Minisat Copyrights + +Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson +Copyright (c) 2007-2010, Niklas Sorensson + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + **************************************************************************************************/ + +#include "mtl/Sort.h" +#include "simp/SimpSolver.h" +#include "utils/System.h" + +using namespace Glucose; + +//================================================================================================= +// Options: + + +static const char* _cat = "SIMP"; + +static BoolOption opt_use_asymm (_cat, "asymm", "Shrink clauses by asymmetric branching.", false); +static BoolOption opt_use_rcheck (_cat, "rcheck", "Check if a clause is already implied. (costly)", false); +static BoolOption opt_use_elim (_cat, "elim", "Perform variable elimination.", true); +static IntOption opt_grow (_cat, "grow", "Allow a variable elimination step to grow by a number of clauses.", 0); +static IntOption opt_clause_lim (_cat, "cl-lim", "Variables are not eliminated if it produces a resolvent with a length above this limit. -1 means no limit", 20, IntRange(-1, INT32_MAX)); +static IntOption opt_subsumption_lim (_cat, "sub-lim", "Do not check if subsumption against a clause larger than this. -1 means no limit.", 1000, IntRange(-1, INT32_MAX)); +static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of wasted memory allowed before a garbage collection is triggered during simplification.", 0.5, DoubleRange(0, false, HUGE_VAL, false)); + + +//================================================================================================= +// Constructor/Destructor: + + +SimpSolver::SimpSolver() : + Solver() + , grow (opt_grow) + , clause_lim (opt_clause_lim) + , subsumption_lim (opt_subsumption_lim) + , simp_garbage_frac (opt_simp_garbage_frac) + , use_asymm (opt_use_asymm) + , use_rcheck (opt_use_rcheck) + , use_elim (opt_use_elim) + , merges (0) + , asymm_lits (0) + , eliminated_vars (0) + , elimorder (1) + , use_simplification (true) + , occurs (ClauseDeleted(ca)) + , elim_heap (ElimLt(n_occ)) + , bwdsub_assigns (0) + , n_touched (0) +{ + vec dummy(1,lit_Undef); + ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below. + bwdsub_tmpunit = ca.alloc(dummy); + remove_satisfied = false; +} + + +SimpSolver::~SimpSolver() +{ +} + + + +SimpSolver::SimpSolver(const SimpSolver &s) : Solver(s) + , grow (s.grow) + , clause_lim (s.clause_lim) + , subsumption_lim (s.subsumption_lim) + , simp_garbage_frac (s.simp_garbage_frac) + , use_asymm (s.use_asymm) + , use_rcheck (s.use_rcheck) + , use_elim (s.use_elim) + , merges (s.merges) + , asymm_lits (s.asymm_lits) + , eliminated_vars (s.eliminated_vars) + , elimorder (s.elimorder) + , use_simplification (s.use_simplification) + , occurs (ClauseDeleted(ca)) + , elim_heap (ElimLt(n_occ)) + , bwdsub_assigns (s.bwdsub_assigns) + , n_touched (s.n_touched) +{ + // TODO: Copy dummy... what is it??? + vec dummy(1,lit_Undef); + ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below. + bwdsub_tmpunit = ca.alloc(dummy); + remove_satisfied = false; + //End TODO + + + s.elimclauses.memCopyTo(elimclauses); + s.touched.memCopyTo(touched); + s.occurs.copyTo(occurs); + s.n_occ.memCopyTo(n_occ); + s.elim_heap.copyTo(elim_heap); + s.subsumption_queue.copyTo(subsumption_queue); + s.frozen.memCopyTo(frozen); + s.eliminated.memCopyTo(eliminated); + + use_simplification = s.use_simplification; + bwdsub_assigns = s.bwdsub_assigns; + n_touched = s.n_touched; + bwdsub_tmpunit = s.bwdsub_tmpunit; + qhead = s.qhead; + ok = s.ok; +} + + + +Var SimpSolver::newVar(bool sign, bool dvar) { + Var v = Solver::newVar(sign, dvar); + frozen .push((char)false); + eliminated.push((char)false); + + if (use_simplification){ + n_occ .push(0); + n_occ .push(0); + occurs .init(v); + touched .push(0); + elim_heap .insert(v); + } + return v; } + +lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp) +{ + vec extra_frozen; + lbool result = l_True; + do_simp &= use_simplification; + + if (do_simp){ + // Assumptions must be temporarily frozen to run variable elimination: + for (int i = 0; i < assumptions.size(); i++){ + Var v = var(assumptions[i]); + + // If an assumption has been eliminated, remember it. + assert(!isEliminated(v)); + + if (!frozen[v]){ + // Freeze and store. + setFrozen(v, true); + extra_frozen.push(v); + } } + + result = lbool(eliminate(turn_off_simp)); + } + + if (result == l_True) + result = Solver::solve_(); + else if (verbosity >= 1) + printf("===============================================================================\n"); + + if (result == l_True) + extendModel(); + + if (do_simp) + // Unfreeze the assumptions that were frozen: + for (int i = 0; i < extra_frozen.size(); i++) + setFrozen(extra_frozen[i], false); + + + return result; +} + + + +bool SimpSolver::addClause_(vec& ps) +{ +#ifndef NDEBUG + for (int i = 0; i < ps.size(); i++) + assert(!isEliminated(var(ps[i]))); +#endif + int nclauses = clauses.size(); + + if (use_rcheck && implied(ps)) + return true; + + if (!Solver::addClause_(ps)) + return false; + + if(!parsing && certifiedUNSAT) { + for (int i = 0; i < ps.size(); i++) + fprintf(certifiedOutput, "%i " , (var(ps[i]) + 1) * (-2 * sign(ps[i]) + 1) ); + fprintf(certifiedOutput, "0\n"); + } + + if (use_simplification && clauses.size() == nclauses + 1){ + CRef cr = clauses.last(); + const Clause& c = ca[cr]; + + // NOTE: the clause is added to the queue immediately and then + // again during 'gatherTouchedClauses()'. If nothing happens + // in between, it will only be checked once. Otherwise, it may + // be checked twice unnecessarily. This is an unfortunate + // consequence of how backward subsumption is used to mimic + // forward subsumption. + subsumption_queue.insert(cr); + for (int i = 0; i < c.size(); i++){ + occurs[var(c[i])].push(cr); + n_occ[toInt(c[i])]++; + touched[var(c[i])] = 1; + n_touched++; + if (elim_heap.inHeap(var(c[i]))) + elim_heap.increase(var(c[i])); + } + } + + return true; +} + + + +void SimpSolver::removeClause(CRef cr,bool inPurgatory) +{ + const Clause& c = ca[cr]; + + if (use_simplification) + for (int i = 0; i < c.size(); i++){ + n_occ[toInt(c[i])]--; + updateElimHeap(var(c[i])); + occurs.smudge(var(c[i])); + } + + Solver::removeClause(cr,inPurgatory); +} + + +bool SimpSolver::strengthenClause(CRef cr, Lit l) +{ + Clause& c = ca[cr]; + assert(decisionLevel() == 0); + assert(use_simplification); + + // FIX: this is too inefficient but would be nice to have (properly implemented) + // if (!find(subsumption_queue, &c)) + subsumption_queue.insert(cr); + + if (certifiedUNSAT) { + for (int i = 0; i < c.size(); i++) + if (c[i] != l) fprintf(certifiedOutput, "%i " , (var(c[i]) + 1) * (-2 * sign(c[i]) + 1) ); + fprintf(certifiedOutput, "0\n"); + } + + if (c.size() == 2){ + removeClause(cr); + c.strengthen(l); + }else{ + if (certifiedUNSAT) { + fprintf(certifiedOutput, "d "); + for (int i = 0; i < c.size(); i++) + fprintf(certifiedOutput, "%i " , (var(c[i]) + 1) * (-2 * sign(c[i]) + 1) ); + fprintf(certifiedOutput, "0\n"); + } + + detachClause(cr, true); + c.strengthen(l); + attachClause(cr); + remove(occurs[var(l)], cr); + n_occ[toInt(l)]--; + updateElimHeap(var(l)); + } + + return c.size() == 1 ? enqueue(c[0]) && propagate() == CRef_Undef : true; +} + + +// Returns FALSE if clause is always satisfied ('out_clause' should not be used). +bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec& out_clause) +{ + merges++; + out_clause.clear(); + + bool ps_smallest = _ps.size() < _qs.size(); + const Clause& ps = ps_smallest ? _qs : _ps; + const Clause& qs = ps_smallest ? _ps : _qs; + + for (int i = 0; i < qs.size(); i++){ + if (var(qs[i]) != v){ + for (int j = 0; j < ps.size(); j++) + if (var(ps[j]) == var(qs[i])) + if (ps[j] == ~qs[i]) + return false; + else + goto next; + out_clause.push(qs[i]); + } + next:; + } + + for (int i = 0; i < ps.size(); i++) + if (var(ps[i]) != v) + out_clause.push(ps[i]); + + return true; +} + + +// Returns FALSE if clause is always satisfied. +bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size) +{ + merges++; + + bool ps_smallest = _ps.size() < _qs.size(); + const Clause& ps = ps_smallest ? _qs : _ps; + const Clause& qs = ps_smallest ? _ps : _qs; + const Lit* __ps = (const Lit*)ps; + const Lit* __qs = (const Lit*)qs; + + size = ps.size()-1; + + for (int i = 0; i < qs.size(); i++){ + if (var(__qs[i]) != v){ + for (int j = 0; j < ps.size(); j++) + if (var(__ps[j]) == var(__qs[i])) + if (__ps[j] == ~__qs[i]) + return false; + else + goto next; + size++; + } + next:; + } + + return true; +} + + +void SimpSolver::gatherTouchedClauses() +{ + if (n_touched == 0) return; + + int i,j; + for (i = j = 0; i < subsumption_queue.size(); i++) + if (ca[subsumption_queue[i]].mark() == 0) + ca[subsumption_queue[i]].mark(2); + + for (i = 0; i < touched.size(); i++) + if (touched[i]){ + const vec& cs = occurs.lookup(i); + for (j = 0; j < cs.size(); j++) + if (ca[cs[j]].mark() == 0){ + subsumption_queue.insert(cs[j]); + ca[cs[j]].mark(2); + } + touched[i] = 0; + } + + for (i = 0; i < subsumption_queue.size(); i++) + if (ca[subsumption_queue[i]].mark() == 2) + ca[subsumption_queue[i]].mark(0); + + n_touched = 0; +} + + +bool SimpSolver::implied(const vec& c) +{ + assert(decisionLevel() == 0); + + trail_lim.push(trail.size()); + for (int i = 0; i < c.size(); i++) + if (value(c[i]) == l_True){ + cancelUntil(0); + return false; + }else if (value(c[i]) != l_False){ + assert(value(c[i]) == l_Undef); + uncheckedEnqueue(~c[i]); + } + + bool result = propagate() != CRef_Undef; + cancelUntil(0); + return result; +} + + +// Backward subsumption + backward subsumption resolution +bool SimpSolver::backwardSubsumptionCheck(bool verbose) +{ + int cnt = 0; + int subsumed = 0; + int deleted_literals = 0; + assert(decisionLevel() == 0); + + while (subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()){ + + // Empty subsumption queue and return immediately on user-interrupt: + if (asynch_interrupt){ + subsumption_queue.clear(); + bwdsub_assigns = trail.size(); + break; } + + // Check top-level assignments by creating a dummy clause and placing it in the queue: + if (subsumption_queue.size() == 0 && bwdsub_assigns < trail.size()){ + Lit l = trail[bwdsub_assigns++]; + ca[bwdsub_tmpunit][0] = l; + ca[bwdsub_tmpunit].calcAbstraction(); + subsumption_queue.insert(bwdsub_tmpunit); } + + CRef cr = subsumption_queue.peek(); subsumption_queue.pop(); + Clause& c = ca[cr]; + + if (c.mark()) continue; + + if (verbose && verbosity >= 2 && cnt++ % 1000 == 0) + printf("subsumption left: %10d (%10d subsumed, %10d deleted literals)\r", subsumption_queue.size(), subsumed, deleted_literals); + + assert(c.size() > 1 || value(c[0]) == l_True); // Unit-clauses should have been propagated before this point. + + // Find best variable to scan: + Var best = var(c[0]); + for (int i = 1; i < c.size(); i++) + if (occurs[var(c[i])].size() < occurs[best].size()) + best = var(c[i]); + + // Search all candidates: + vec& _cs = occurs.lookup(best); + CRef* cs = (CRef*)_cs; + + for (int j = 0; j < _cs.size(); j++) + if (c.mark()) + break; + else if (!ca[cs[j]].mark() && cs[j] != cr && (subsumption_lim == -1 || ca[cs[j]].size() < subsumption_lim)){ + Lit l = c.subsumes(ca[cs[j]]); + + if (l == lit_Undef) + subsumed++, removeClause(cs[j]); + else if (l != lit_Error){ + deleted_literals++; + + if (!strengthenClause(cs[j], ~l)) + return false; + + // Did current candidate get deleted from cs? Then check candidate at index j again: + if (var(l) == best) + j--; + } + } + } + + return true; +} + + +bool SimpSolver::asymm(Var v, CRef cr) +{ + Clause& c = ca[cr]; + assert(decisionLevel() == 0); + + if (c.mark() || satisfied(c)) return true; + + trail_lim.push(trail.size()); + Lit l = lit_Undef; + for (int i = 0; i < c.size(); i++) + if (var(c[i]) != v && value(c[i]) != l_False) + uncheckedEnqueue(~c[i]); + else + l = c[i]; + + if (propagate() != CRef_Undef){ + cancelUntil(0); + asymm_lits++; + if (!strengthenClause(cr, l)) + return false; + }else + cancelUntil(0); + + return true; +} + + +bool SimpSolver::asymmVar(Var v) +{ + assert(use_simplification); + + const vec& cls = occurs.lookup(v); + + if (value(v) != l_Undef || cls.size() == 0) + return true; + + for (int i = 0; i < cls.size(); i++) + if (!asymm(v, cls[i])) + return false; + + return backwardSubsumptionCheck(); +} + + +static void mkElimClause(vec& elimclauses, Lit x) +{ + elimclauses.push(toInt(x)); + elimclauses.push(1); +} + + +static void mkElimClause(vec& elimclauses, Var v, Clause& c) +{ + int first = elimclauses.size(); + int v_pos = -1; + + // Copy clause to elimclauses-vector. Remember position where the + // variable 'v' occurs: + for (int i = 0; i < c.size(); i++){ + elimclauses.push(toInt(c[i])); + if (var(c[i]) == v) + v_pos = i + first; + } + assert(v_pos != -1); + + // Swap the first literal with the 'v' literal, so that the literal + // containing 'v' will occur first in the clause: + uint32_t tmp = elimclauses[v_pos]; + elimclauses[v_pos] = elimclauses[first]; + elimclauses[first] = tmp; + + // Store the length of the clause last: + elimclauses.push(c.size()); +} + + + +bool SimpSolver::eliminateVar(Var v) +{ + assert(!frozen[v]); + assert(!isEliminated(v)); + assert(value(v) == l_Undef); + + // Split the occurrences into positive and negative: + // + const vec& cls = occurs.lookup(v); + vec pos, neg; + for (int i = 0; i < cls.size(); i++) + (find(ca[cls[i]], mkLit(v)) ? pos : neg).push(cls[i]); + + // Check wether the increase in number of clauses stays within the allowed ('grow'). Moreover, no + // clause must exceed the limit on the maximal clause size (if it is set): + // + int cnt = 0; + int clause_size = 0; + + for (int i = 0; i < pos.size(); i++) + for (int j = 0; j < neg.size(); j++) + if (merge(ca[pos[i]], ca[neg[j]], v, clause_size) && + (++cnt > cls.size() + grow || (clause_lim != -1 && clause_size > clause_lim))) + return true; + + // Delete and store old clauses: + eliminated[v] = true; + setDecisionVar(v, false); + eliminated_vars++; + + if (pos.size() > neg.size()){ + for (int i = 0; i < neg.size(); i++) + mkElimClause(elimclauses, v, ca[neg[i]]); + mkElimClause(elimclauses, mkLit(v)); + }else{ + for (int i = 0; i < pos.size(); i++) + mkElimClause(elimclauses, v, ca[pos[i]]); + mkElimClause(elimclauses, ~mkLit(v)); + } + + + // Produce clauses in cross product: + vec& resolvent = add_tmp; + for (int i = 0; i < pos.size(); i++) + for (int j = 0; j < neg.size(); j++) + if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent)) + return false; + + for (int i = 0; i < cls.size(); i++) + removeClause(cls[i]); + + // Free occurs list for this variable: + occurs[v].clear(true); + + // Free watchers lists for this variable, if possible: + if (watches[ mkLit(v)].size() == 0) watches[ mkLit(v)].clear(true); + if (watches[~mkLit(v)].size() == 0) watches[~mkLit(v)].clear(true); + + return backwardSubsumptionCheck(); +} + + +bool SimpSolver::substitute(Var v, Lit x) +{ + assert(!frozen[v]); + assert(!isEliminated(v)); + assert(value(v) == l_Undef); + + if (!ok) return false; + + eliminated[v] = true; + setDecisionVar(v, false); + const vec& cls = occurs.lookup(v); + + vec& subst_clause = add_tmp; + for (int i = 0; i < cls.size(); i++){ + Clause& c = ca[cls[i]]; + + subst_clause.clear(); + for (int j = 0; j < c.size(); j++){ + Lit p = c[j]; + subst_clause.push(var(p) == v ? x ^ sign(p) : p); + } + + + if (!addClause_(subst_clause)) + return ok = false; + + removeClause(cls[i]); + + } + + return true; +} + + +void SimpSolver::extendModel() +{ + int i, j; + Lit x; + + if(model.size()==0) model.growTo(nVars()); + + for (i = elimclauses.size()-1; i > 0; i -= j){ + for (j = elimclauses[i--]; j > 1; j--, i--) + if (modelValue(toLit(elimclauses[i])) != l_False) + goto next; + + x = toLit(elimclauses[i]); + model[var(x)] = lbool(!sign(x)); + next:; + } +} + + +bool SimpSolver::eliminate(bool turn_off_elim) +{ + if (!simplify()) { + ok = false; + return false; + } + else if (!use_simplification) + return true; + + // Main simplification loop: + // + + int toPerform = clauses.size()<=4800000; + + if(!toPerform) { + printf("c Too many clauses... No preprocessing\n"); + } + + while (toPerform && (n_touched > 0 || bwdsub_assigns < trail.size() || elim_heap.size() > 0)){ + + gatherTouchedClauses(); + // printf(" ## (time = %6.2f s) BWD-SUB: queue = %d, trail = %d\n", cpuTime(), subsumption_queue.size(), trail.size() - bwdsub_assigns); + if ((subsumption_queue.size() > 0 || bwdsub_assigns < trail.size()) && + !backwardSubsumptionCheck(true)){ + ok = false; goto cleanup; } + + // Empty elim_heap and return immediately on user-interrupt: + if (asynch_interrupt){ + assert(bwdsub_assigns == trail.size()); + assert(subsumption_queue.size() == 0); + assert(n_touched == 0); + elim_heap.clear(); + goto cleanup; } + + // printf(" ## (time = %6.2f s) ELIM: vars = %d\n", cpuTime(), elim_heap.size()); + for (int cnt = 0; !elim_heap.empty(); cnt++){ + Var elim = elim_heap.removeMin(); + + if (asynch_interrupt) break; + + if (isEliminated(elim) || value(elim) != l_Undef) continue; + + if (verbosity >= 2 && cnt % 100 == 0) + printf("elimination left: %10d\r", elim_heap.size()); + + if (use_asymm){ + // Temporarily freeze variable. Otherwise, it would immediately end up on the queue again: + bool was_frozen = frozen[elim]; + frozen[elim] = true; + if (!asymmVar(elim)){ + ok = false; goto cleanup; } + frozen[elim] = was_frozen; } + + // At this point, the variable may have been set by assymetric branching, so check it + // again. Also, don't eliminate frozen variables: + if (use_elim && value(elim) == l_Undef && !frozen[elim] && !eliminateVar(elim)){ + ok = false; goto cleanup; } + + checkGarbage(simp_garbage_frac); + } + + assert(subsumption_queue.size() == 0); + } + cleanup: + + // If no more simplification is needed, free all simplification-related data structures: + if (turn_off_elim){ + touched .clear(true); + occurs .clear(true); + n_occ .clear(true); + elim_heap.clear(true); + subsumption_queue.clear(true); + + use_simplification = false; + remove_satisfied = true; + ca.extra_clause_field = false; + + // Force full cleanup (this is safe and desirable since it only happens once): + rebuildOrderHeap(); + garbageCollect(); + }else{ + // Cheaper cleanup: + cleanUpClauses(); // TODO: can we make 'cleanUpClauses()' not be linear in the problem size somehow? + checkGarbage(); + } + + if (verbosity >= 0 && elimclauses.size() > 0) + printf("c | Eliminated clauses: %10.2f Mb |\n", + double(elimclauses.size() * sizeof(uint32_t)) / (1024*1024)); + + + return ok; + + +} + + +void SimpSolver::cleanUpClauses() +{ + occurs.cleanAll(); + int i,j; + for (i = j = 0; i < clauses.size(); i++) + if (ca[clauses[i]].mark() == 0) + clauses[j++] = clauses[i]; + clauses.shrink(i - j); +} + + +//================================================================================================= +// Garbage Collection methods: + + +void SimpSolver::relocAll(ClauseAllocator& to) +{ + if (!use_simplification) return; + + // All occurs lists: + // + for (int i = 0; i < nVars(); i++){ + vec& cs = occurs[i]; + for (int j = 0; j < cs.size(); j++) + ca.reloc(cs[j], to); + } + + // Subsumption queue: + // + for (int i = 0; i < subsumption_queue.size(); i++) + ca.reloc(subsumption_queue[i], to); + + // Temporary clause: + // + ca.reloc(bwdsub_tmpunit, to); +} + + +void SimpSolver::garbageCollect() +{ + // Initialize the next region to a size corresponding to the estimated utilization degree. This + // is not precise but should avoid some unnecessary reallocations for the new region: + ClauseAllocator to(ca.size() - ca.wasted()); + + cleanUpClauses(); + to.extra_clause_field = ca.extra_clause_field; // NOTE: this is important to keep (or lose) the extra fields. + relocAll(to); + Solver::relocAll(to); + if (verbosity >= 2) + printf("| Garbage collection: %12d bytes => %12d bytes |\n", + ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size); + to.moveTo(ca); +} diff --git a/glucose-syrup/incremental/SimpSolver.h b/glucose-syrup/incremental/SimpSolver.h new file mode 100644 index 0000000..5f457a8 --- /dev/null +++ b/glucose-syrup/incremental/SimpSolver.h @@ -0,0 +1,237 @@ +/***************************************************************************************[SimpSolver.h] + Glucose -- Copyright (c) 2009-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + LRI - Univ. Paris Sud, France (2009-2013) + Labri - Univ. Bordeaux, France + + Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon + CRIL - Univ. Artois, France + Labri - Univ. Bordeaux, France + +Glucose sources are based on MiniSat (see below MiniSat copyrights). Permissions and copyrights of +Glucose (sources until 2013, Glucose 3.0, single core) are exactly the same as Minisat on which it +is based on. (see below). + +Glucose-Syrup sources are based on another copyright. Permissions and copyrights for the parallel +version of Glucose-Syrup (the "Software") are granted, free of charge, to deal with the Software +without restriction, including the rights to use, copy, modify, merge, publish, distribute, +sublicence, 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 and below copyrights notices and this permission notice shall be included in all +copies or substantial portions of the Software; +- The parallel version of Glucose (all files modified since Glucose 3.0 releases, 2013) cannot +be used in any competitive event (sat competitions/evaluations) without the express permission of +the authors (Gilles Audemard / Laurent Simon). This is also the case for any competitive event +using Glucose Parallel as an embedded SAT engine (single core or not). + + +--------------- Original Minisat Copyrights + +Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson +Copyright (c) 2007-2010, Niklas Sorensson + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. + **************************************************************************************************/ + +#ifndef Glucose_SimpSolver_h +#define Glucose_SimpSolver_h + +#include "mtl/Queue.h" +#include "core/Solver.h" +#include "mtl/Clone.h" + +namespace Glucose { + +//================================================================================================= + + +class SimpSolver : public Solver { + public: + // Constructor/Destructor: + // + SimpSolver(); + ~SimpSolver(); + + SimpSolver(const SimpSolver &s); + + + /** + * Clone function + */ + virtual Clone* clone() const { + return new SimpSolver(*this); + } + + + // Problem specification: + // + virtual Var newVar (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode. + bool addClause (const vec& ps); + bool addEmptyClause(); // Add the empty clause to the solver. + bool addClause (Lit p); // Add a unit clause to the solver. + bool addClause (Lit p, Lit q); // Add a binary clause to the solver. + bool addClause (Lit p, Lit q, Lit r); // Add a ternary clause to the solver. + virtual bool addClause_( vec& ps); + bool substitute(Var v, Lit x); // Replace all occurences of v with x (may cause a contradiction). + + // Variable mode: + // + void setFrozen (Var v, bool b); // If a variable is frozen it will not be eliminated. + bool isEliminated(Var v) const; + + // Solving: + // + bool solve (const vec& assumps, bool do_simp = true, bool turn_off_simp = false); + lbool solveLimited(const vec& assumps, bool do_simp = true, bool turn_off_simp = false); + bool solve ( bool do_simp = true, bool turn_off_simp = false); + bool solve (Lit p , bool do_simp = true, bool turn_off_simp = false); + bool solve (Lit p, Lit q, bool do_simp = true, bool turn_off_simp = false); + bool solve (Lit p, Lit q, Lit r, bool do_simp = true, bool turn_off_simp = false); + bool eliminate (bool turn_off_elim = false); // Perform variable elimination based simplification. + + // Memory managment: + // + virtual void garbageCollect(); + + + // Generate a (possibly simplified) DIMACS file: + // +#if 0 + void toDimacs (const char* file, const vec& assumps); + void toDimacs (const char* file); + void toDimacs (const char* file, Lit p); + void toDimacs (const char* file, Lit p, Lit q); + void toDimacs (const char* file, Lit p, Lit q, Lit r); +#endif + + // Mode of operation: + // + int parsing; + int grow; // Allow a variable elimination step to grow by a number of clauses (default to zero). + int clause_lim; // Variables are not eliminated if it produces a resolvent with a length above this limit. + // -1 means no limit. + int subsumption_lim; // Do not check if subsumption against a clause larger than this. -1 means no limit. + double simp_garbage_frac; // A different limit for when to issue a GC during simplification (Also see 'garbage_frac'). + + bool use_asymm; // Shrink clauses by asymmetric branching. + bool use_rcheck; // Check if a clause is already implied. Prett costly, and subsumes subsumptions :) + bool use_elim; // Perform variable elimination. + // Statistics: + // + int merges; + int asymm_lits; + int eliminated_vars; + + protected: + + // Helper structures: + // + struct ElimLt { + const vec& n_occ; + explicit ElimLt(const vec& no) : n_occ(no) {} + + // TODO: are 64-bit operations here noticably bad on 32-bit platforms? Could use a saturating + // 32-bit implementation instead then, but this will have to do for now. + uint64_t cost (Var x) const { return (uint64_t)n_occ[toInt(mkLit(x))] * (uint64_t)n_occ[toInt(~mkLit(x))]; } + bool operator()(Var x, Var y) const { return cost(x) < cost(y); } + + // TODO: investigate this order alternative more. + // bool operator()(Var x, Var y) const { + // int c_x = cost(x); + // int c_y = cost(y); + // return c_x < c_y || c_x == c_y && x < y; } + }; + + struct ClauseDeleted { + const ClauseAllocator& ca; + explicit ClauseDeleted(const ClauseAllocator& _ca) : ca(_ca) {} + bool operator()(const CRef& cr) const { return ca[cr].mark() == 1; } }; + + // Solver state: + // + int elimorder; + bool use_simplification; + vec elimclauses; + vec touched; + OccLists, ClauseDeleted> + occurs; + vec n_occ; + Heap elim_heap; + Queue subsumption_queue; + vec frozen; + vec eliminated; + int bwdsub_assigns; + int n_touched; + + // Temporaries: + // + CRef bwdsub_tmpunit; + + // Main internal methods: + // + virtual lbool solve_ (bool do_simp = true, bool turn_off_simp = false); + bool asymm (Var v, CRef cr); + bool asymmVar (Var v); + void updateElimHeap (Var v); + void gatherTouchedClauses (); + bool merge (const Clause& _ps, const Clause& _qs, Var v, vec& out_clause); + bool merge (const Clause& _ps, const Clause& _qs, Var v, int& size); + bool backwardSubsumptionCheck (bool verbose = false); + bool eliminateVar (Var v); + void extendModel (); + + void removeClause (CRef cr,bool inPurgatory=false); + bool strengthenClause (CRef cr, Lit l); + void cleanUpClauses (); + bool implied (const vec& c); + virtual void relocAll (ClauseAllocator& to); +}; + + +//================================================================================================= +// Implementation of inline methods: + + +inline bool SimpSolver::isEliminated (Var v) const { return eliminated[v]; } +inline void SimpSolver::updateElimHeap(Var v) { + assert(use_simplification); + // if (!frozen[v] && !isEliminated(v) && value(v) == l_Undef) + if (elim_heap.inHeap(v) || (!frozen[v] && !isEliminated(v) && value(v) == l_Undef)) + elim_heap.update(v); } + + +inline bool SimpSolver::addClause (const vec& ps) { ps.copyTo(add_tmp); return addClause_(add_tmp); } +inline bool SimpSolver::addEmptyClause() { add_tmp.clear(); return addClause_(add_tmp); } +inline bool SimpSolver::addClause (Lit p) { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp); } +inline bool SimpSolver::addClause (Lit p, Lit q) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); } +inline bool SimpSolver::addClause (Lit p, Lit q, Lit r) { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); } +inline void SimpSolver::setFrozen (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } } + +inline bool SimpSolver::solve ( bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); return solve_(do_simp, turn_off_simp) == l_True; } +inline bool SimpSolver::solve (Lit p , bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); assumptions.push(p); return solve_(do_simp, turn_off_simp) == l_True; } +inline bool SimpSolver::solve (Lit p, Lit q, bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); return solve_(do_simp, turn_off_simp) == l_True; } +inline bool SimpSolver::solve (Lit p, Lit q, Lit r, bool do_simp, bool turn_off_simp) { budgetOff(); assumptions.clear(); assumptions.push(p); assumptions.push(q); assumptions.push(r); return solve_(do_simp, turn_off_simp) == l_True; } +inline bool SimpSolver::solve (const vec& assumps, bool do_simp, bool turn_off_simp){ + budgetOff(); assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp) == l_True; } + +inline lbool SimpSolver::solveLimited (const vec& assumps, bool do_simp, bool turn_off_simp){ + assumps.copyTo(assumptions); return solve_(do_simp, turn_off_simp); } + +//================================================================================================= +} + +#endif diff --git a/glucose-syrup/incremental/SimpSolver.o b/glucose-syrup/incremental/SimpSolver.o new file mode 100644 index 0000000..3cab11f Binary files /dev/null and b/glucose-syrup/incremental/SimpSolver.o differ diff --git a/glucose-syrup/incremental/depend.mk b/glucose-syrup/incremental/depend.mk new file mode 100644 index 0000000..c3f3df8 --- /dev/null +++ b/glucose-syrup/incremental/depend.mk @@ -0,0 +1,41 @@ +/Users/briandemsky/research/model/sat/glucose-syrup/incremental/Main.o /Users/briandemsky/research/model/sat/glucose-syrup/incremental/Main.or /Users/briandemsky/research/model/sat/glucose-syrup/incremental/Main.od /Users/briandemsky/research/model/sat/glucose-syrup/incremental/Main.op: \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/Main.cc \ + ../../solver_interface.h \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../utils/System.h \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/IntTypes.h \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../utils/ParseUtils.h \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../utils/Options.h \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/Vec.h \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/XAlloc.h \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../core/Dimacs.h \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../core/SolverTypes.h \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/Alg.h \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/Map.h \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/Alloc.h \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../simp/SimpSolver.h \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/Queue.h \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../core/Solver.h \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/Heap.h \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../core/BoundedQueue.h \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../core/Constants.h \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/Clone.h +/Users/briandemsky/research/model/sat/glucose-syrup/incremental/SimpSolver.o /Users/briandemsky/research/model/sat/glucose-syrup/incremental/SimpSolver.or /Users/briandemsky/research/model/sat/glucose-syrup/incremental/SimpSolver.od /Users/briandemsky/research/model/sat/glucose-syrup/incremental/SimpSolver.op: \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/SimpSolver.cc \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/Sort.h \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/Vec.h \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/IntTypes.h \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/XAlloc.h \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../simp/SimpSolver.h \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/Queue.h \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../core/Solver.h \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/Heap.h \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/Alg.h \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../utils/Options.h \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../utils/ParseUtils.h \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../core/SolverTypes.h \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/Map.h \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/Alloc.h \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../core/BoundedQueue.h \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../core/Constants.h \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../mtl/Clone.h \ + /Users/briandemsky/research/model/sat/glucose-syrup/incremental/../utils/System.h diff --git a/glucose-syrup/incremental/glucose b/glucose-syrup/incremental/glucose new file mode 100755 index 0000000..d8e04ab Binary files /dev/null and b/glucose-syrup/incremental/glucose differ