From: vijay_ganesh Date: Thu, 29 Oct 2009 17:26:51 +0000 (+0000) Subject: added cryptominisat code. compiles/links and runs correctly. Currently, STP does... X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=c3bfda146d27c4a7592255446eaf0abdefd90a17;p=francis%2Fstp.git added cryptominisat code. compiles/links and runs correctly. Currently, STP does not add xor-clauses, i.e., CryptoMiniSAT runs just like MiniSAT and has the same performance. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@357 e59a4935-1847-0410-ae03-e826735625c1 --- diff --git a/scripts/Makefile.common b/scripts/Makefile.common index 0e3a07f..1a25311 100644 --- a/scripts/Makefile.common +++ b/scripts/Makefile.common @@ -13,8 +13,8 @@ OPTIMIZE = -g # Debugging OPTIMIZE = -O3 -DNDEBUG # Maximum optimization #OPTIMIZE = -O3 -DNDEBUG -DLESSBYTES_PERNODE CFLAGS_BASE = $(OPTIMIZE) -#CFLAGS_BASE = $(OPTIMIZE) -DCRYPTOMINISAT -#CRYPTOMINISAT = true +CFLAGS_BASE = $(OPTIMIZE) -DCRYPTOMINISAT +CRYPTOMINISAT = true #CFLAGS_M32 = -m32 SHELL=/bin/bash diff --git a/src/sat/Makefile b/src/sat/Makefile index 356331f..f7f96f2 100644 --- a/src/sat/Makefile +++ b/src/sat/Makefile @@ -15,9 +15,7 @@ unsound: .PHONY: cryptominisat cryptominisat: - $(MAKE) -C cryptominisat - cp cryptominisat/libminisat.a . - cp cryptominisat/CMakeFiles/minisat.dir/Solver/*.o . + $(MAKE) -C cryptominisat lib all .PHONY: clean clean: @@ -25,6 +23,5 @@ clean: $(MAKE) -C core clean $(MAKE) -C simp clean $(MAKE) -C unsound clean -ifdef CRYPTOMINISAT $(MAKE) -C cryptominisat clean -endif + diff --git a/src/sat/cryptominisat/AUTHORS b/src/sat/cryptominisat/AUTHORS new file mode 100644 index 0000000..98599fa --- /dev/null +++ b/src/sat/cryptominisat/AUTHORS @@ -0,0 +1,10 @@ +Niklas Eén +Niklas Sörensson +Mate SOOS +Karsten Nohl + +thanks to: +- the authors' professors for their trust in their PhD students' capabilities +- the gcc compiler team for the excellent C++ compiler +- libstdc team for the excellent standard library +- Bjarne Stroustrup for the excellent C++ diff --git a/src/sat/cryptominisat/LICENSE b/src/sat/cryptominisat/LICENSE new file mode 100644 index 0000000..beb0799 --- /dev/null +++ b/src/sat/cryptominisat/LICENSE @@ -0,0 +1,21 @@ +MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +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. diff --git a/src/sat/cryptominisat/Logger.C b/src/sat/cryptominisat/Logger.C new file mode 100644 index 0000000..2bb52d0 --- /dev/null +++ b/src/sat/cryptominisat/Logger.C @@ -0,0 +1,748 @@ +/*********************************************************************************** +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ +#include +#include +#include +#include +#include +#include +#include +#include +using std::cout; +using std::endl; +using std::ofstream; + +#include "Logger.h" +#include "fcopy.h" +#include "SolverTypes.h" + +namespace MINISAT +{ + +#define MAX_VAR 1000000 + +#define FST_WIDTH 10 +#define SND_WIDTH 35 +#define TRD_WIDTH 10 + +Logger::Logger(int& _verbosity) : + proof_graph_on(false), + statistics_on(false), + + max_print_lines(20), + uniqueid(1), + level(0), + begin_level(0), + max_group(0), + + proof(NULL), + proof_num(0), + + sum_conflict_depths(0), + no_conflicts(0), + no_decisions(0), + no_propagations(0), + sum_decisions_on_branches(0), + sum_propagations_on_branches(0), + + verbosity(_verbosity) +{ + runid /= 10; + runid=time(NULL)%10000; + if (verbosity >= 1) printf("RunID is: #%d\n",runid); + + sprintf(filename0,"proofs/%d-proof0.dot", runid); +} + +// Adds a new variable to the knowledge of the logger +void Logger::new_var(const Var var) +{ + assert(var < MAX_VAR); + + if (varnames.size() <= var) { + varnames.resize(var+1); + times_var_propagated.resize(var+1); + times_var_guessed.resize(var+1); + depths_of_assigns_for_var.resize(var+1); + } +} + +// Resizes the groupnames and other, related vectors to accomodate for a new group +void Logger::new_group(const uint group) +{ + if (groupnames.size() <= group) { + uint old_size = times_group_caused_propagation.size(); + groupnames.resize(group+1, "Noname"); + times_group_caused_conflict.resize(group+1); + times_group_caused_propagation.resize(group+1); + depths_of_propagations_for_group.resize(group+1); + depths_of_conflicts_for_group.resize(group+1); + for (uint i = old_size; i < times_group_caused_propagation.size(); i++) { + times_group_caused_propagation[i] = 0; + times_group_caused_conflict[i] = 0; + } + } + + max_group = std::max(group, max_group); +} + +// Adds the new clause group's name to the information stored +void Logger::set_group_name(const uint group, const char* name) +{ + new_group(group); + + if (strlen(name) > SND_WIDTH-2) { + cout << "A clause group name cannot have more than " << SND_WIDTH-2 << " number of characters. You gave '" << name << "', which is " << strlen(name) << " long." << endl; + exit(-1); + } + + if (groupnames[group].empty() || groupnames[group] == "Noname") { + groupnames[group] = name; + } else if (name != '\0' && groupnames[group] != name) { + printf("Error! Group no. %d has been named twice. First, as '%s', then second as '%s'. Name the same group the same always, or don't give a name to the second iteration of the same group (i.e just write 'c g groupnumber' on the line\n", group, groupnames[group].c_str(), name); + exit(-1); + } +} + +// sets the variable's name +void Logger::set_variable_name(const uint var, const char* name) +{ + if (!proof_graph_on && !statistics_on) return; + + if (strlen(name) > SND_WIDTH-2) { + cout << "A variable name cannot have more than " << SND_WIDTH-2 << " number of characters. You gave '" << name << "', which is " << strlen(name) << " long." << endl; + exit(-1); + } + + new_var(var); + varnames[var] = name; +} + +void Logger::begin() +{ + char filename[80]; + sprintf(filename, "proofs/%d-proof%d.dot", runid, proof_num); + + if (proof_num > 0) { + if (proof_graph_on) { + FileCopy(filename0, filename); + proof = fopen(filename,"a"); + if (!proof) printf("Couldn't open proof file '%s' for writing\n", filename), exit(-1); + } + } else { + history.growTo(10); + history[level] = uniqueid; + + if (proof_graph_on) { + proof = fopen(filename,"w"); + if (!proof) printf("Couldn't open proof file '%s' for writing\n", filename), exit(-1); + fprintf(proof, "digraph G {\n"); + fprintf(proof,"node%d [shape=circle, label=\"BEGIN\", root];\n", uniqueid); + } + } + + if (statistics_on) + reset_statistics(); + + level = begin_level; +} + +// For noting conflicts. Updates the proof graph and the statistics. +void Logger::conflict(const confl_type type, uint goback, const uint group, const vec& learnt_clause) +{ + assert(!(proof == NULL && proof_graph_on)); + assert(goback < level); + + goback += begin_level; + uniqueid++; + + if (proof_graph_on) { + fprintf(proof,"node%d [shape=polygon,sides=5,label=\"",uniqueid); + for (int i = 0; i < learnt_clause.size(); i++) { + if (learnt_clause[i].sign()) fprintf(proof,"-"); + int myvar = learnt_clause[i].var(); + if (varnames.size() <= myvar || varnames[myvar].empty()) + fprintf(proof,"%d\\n",myvar+1); + else fprintf(proof,"%s\\n",varnames[myvar].c_str()); + } + + fprintf(proof,"\"];\n"); + + fprintf(proof,"node%d -> node%d [label=\"",history[level],uniqueid); + + if (type == gauss_confl_type) { + fprintf(proof,"Gauss\",style=bold"); + } else if (group > max_group) fprintf(proof,"**%d\"",group); + else { + if (groupnames.size() <= group || groupnames[group].empty()) + fprintf(proof,"%d\"", group); + else fprintf(proof,"%s\"", groupnames[group].c_str()); + } + + fprintf(proof,"];\n"); + fprintf(proof,"node%d -> node%d [style=bold];\n",uniqueid,history[goback]); + } + + if (statistics_on) { + const uint depth = level - begin_level; + + if (group < max_group) { //TODO make work for learnt clauses + times_group_caused_conflict[group]++; + depths_of_conflicts_for_group[group].push_back(depth); + } + no_conflicts++; + sum_conflict_depths += depth; + sum_decisions_on_branches += decisions[depth]; + sum_propagations_on_branches += propagations[depth]; + branch_depth_distrib[depth]++; + } + + level = goback; +} + +// For the really strange event that the solver is given an empty clause +void Logger::empty_clause(const uint group) +{ + assert(!(proof == NULL && proof_graph_on)); + + if (proof_graph_on) { + fprintf(proof,"node%d -> node%d [label=\"emtpy clause:",history[level],uniqueid+1); + if (group > max_group) fprintf(proof,"**%d\\n",group); + else { + if (groupnames.size() <= group || groupnames[group].empty()) + fprintf(proof,"%d\\n", group); + else fprintf(proof,"%s\\n", groupnames[group].c_str()); + } + + fprintf(proof,"\"];\n"); + } +} + +// Propagating a literal. Type of literal and the (learned clause's)/(propagating clause's)/(etc) group must be given. Updates the proof graph and the statistics. note: the meaning of the variable 'group' depends on the type +void Logger::propagation(const Lit lit, const prop_type type, const uint group) +{ + assert(!(proof == NULL && proof_graph_on)); + uniqueid++; + + //graph + if (proof_graph_on) { + fprintf(proof,"node%d [shape=box, label=\"",uniqueid);; + if (lit.sign()) fprintf(proof,"-"); + if (varnames.size() <= lit.var() || varnames[lit.var()].empty()) + fprintf(proof,"%d\"];\n",lit.var()+1); + else fprintf(proof,"%s\"];\n",varnames[lit.var()].c_str()); + + fprintf(proof,"node%d -> node%d [label=\"",history[level],uniqueid); + switch (type) { + + case revert_guess_type: + case simple_propagation_type: + assert(group != UINT_MAX); + if (group > max_group) fprintf(proof,"**%d\\n",group); + else { + if (groupnames.size() <= group || groupnames[group].empty()) + fprintf(proof,"%d\\n", group); + else fprintf(proof,"%s\\n", groupnames[group].c_str()); + } + + fprintf(proof,"\"];\n"); + break; + + case gauss_propagation_type: + fprintf(proof,"Gauss\",style=bold];\n"); + break; + + case learnt_unit_clause_type: + fprintf(proof,"learnt unit clause\",style=bold];\n"); + break; + + case assumption_type: + fprintf(proof,"assumption\"];\n"); + break; + + case guess_type: + fprintf(proof,"guess\",style=dotted];\n"); + break; + + case addclause_type: + assert(group != UINT_MAX); + if (groupnames.size() <= group || groupnames[group].empty()) + fprintf(proof,"red. from %d\"];\n",group); + else fprintf(proof,"red. from %s\"];\n",groupnames[group].c_str()); + break; + } + } + + if (statistics_on && proof_num > 0) switch (type) { + case gauss_propagation_type: + case simple_propagation_type: + no_propagations++; + times_var_propagated[lit.var()]++; + if (group < max_group) { //TODO make work for learnt clauses + depths_of_propagations_for_group[group].push_back(level - begin_level); + times_group_caused_propagation[group]++; + } + depths_of_assigns_for_var[lit.var()].push_back(level - begin_level); + break; + + case learnt_unit_clause_type: //when learning unit clause + case revert_guess_type: //when, after conflict, a guess gets reverted + if (group < max_group) { //TODO make work for learnt clauses + times_group_caused_propagation[group]++; + depths_of_propagations_for_group[group].push_back(level - begin_level); + } + depths_of_assigns_for_var[lit.var()].push_back(level - begin_level); + case guess_type: + times_var_guessed[lit.var()]++; + depths_of_assigns_for_var[lit.var()].push_back(level - begin_level); + no_decisions++; + break; + + case addclause_type: + case assumption_type: + assert(false); + } + + level++; + + if (proof_num > 0) { + decisions.growTo(level-begin_level+1); + propagations.growTo(level-begin_level+1); + if (level-begin_level == 1) { + decisions[0] = 0; + propagations[0] = 0; + //note: we might reach this place TWICE in the same restart. This is because the first assignement might get reverted + } + if (type == simple_propagation_type) { + decisions[level-begin_level] = decisions[level-begin_level-1]; + propagations[level-begin_level] = propagations[level-begin_level-1]+1; + } else { + decisions[level-begin_level] = decisions[level-begin_level-1]+1; + propagations[level-begin_level] = propagations[level-begin_level-1]; + } + } + + if (history.size() < level+1) history.growTo(level+10); + history[level] = uniqueid; +} + +// Ending of a restart iteration. Also called when ending S.simplify(); +void Logger::end(const finish_type finish) +{ + assert(!(proof == NULL && proof_graph_on)); + + switch (finish) { + case model_found: { + uniqueid++; + if (proof_graph_on) fprintf(proof,"node%d [shape=doublecircle, label=\"MODEL\"];\n",uniqueid); + break; + } + case unsat_model_found: { + uniqueid++; + if (proof_graph_on) fprintf(proof,"node%d [shape=doublecircle, label=\"UNSAT\"];\n",uniqueid); + break; + } + case restarting: { + uniqueid++; + if (proof_graph_on) fprintf(proof,"node%d [shape=doublecircle, label=\"Re-starting\\nsearch\"];\n",uniqueid); + break; + } + case done_adding_clauses: { + begin_level = level; + break; + } + } + + if (proof_graph_on) { + if (proof_num > 0) { + fprintf(proof,"node%d -> node%d;\n",history[level],uniqueid); + fprintf(proof,"}\n"); + } else proof0_lastid = uniqueid; + + proof = (FILE*)fclose(proof); + assert(proof == NULL); + + if (finish == model_found || finish == unsat_model_found) { + proof = fopen(filename0,"a"); + fprintf(proof,"node%d [shape=doublecircle, label=\"Done adding\\nclauses\"];\n",proof0_lastid+1); + fprintf(proof,"node%d -> node%d;\n",proof0_lastid,proof0_lastid+1); + fprintf(proof,"}\n"); + proof = (FILE*)fclose(proof); + assert(proof == NULL); + } + } + + if (statistics_on) printstats(); + + proof_num++; +} + +void Logger::print_footer() const +{ + cout << "+" << std::setfill('-') << std::setw(FST_WIDTH+SND_WIDTH+TRD_WIDTH+4) << "-" << std::setfill(' ') << "+" << endl; +} + +void Logger::print_assign_var_order() const +{ + vector > prop_ordered; + for (uint i = 0; i < depths_of_assigns_for_var.size(); i++) { + double avg = 0.0; + for (vector::const_iterator it = depths_of_assigns_for_var[i].begin(); it != depths_of_assigns_for_var[i].end(); it++) + avg += *it; + if (depths_of_assigns_for_var[i].size() > 0) { + avg /= (double) depths_of_assigns_for_var[i].size(); + prop_ordered.push_back(std::make_pair(avg, i)); + } + } + + if (!prop_ordered.empty()) { + print_footer(); + print_simple_line(" Variables are assigned in the following order"); + print_header("var", "var name", "avg order"); + std::sort(prop_ordered.begin(), prop_ordered.end()); + print_vars(prop_ordered); + } +} + +void Logger::print_prop_order() const +{ + vector > prop_ordered; + for (uint i = 0; i < depths_of_propagations_for_group.size(); i++) { + double avg = 0.0; + for (vector::const_iterator it = depths_of_propagations_for_group[i].begin(); it != depths_of_propagations_for_group[i].end(); it++) + avg += *it; + if (depths_of_propagations_for_group[i].size() > 0) { + avg /= (double) depths_of_propagations_for_group[i].size(); + prop_ordered.push_back(std::make_pair(avg, i)); + } + } + + if (!prop_ordered.empty()) { + print_footer(); + print_simple_line(" Propagation depth order of clause groups"); + print_header("group", "group name", "avg order"); + std::sort(prop_ordered.begin(), prop_ordered.end()); + print_groups(prop_ordered); + } +} + +void Logger::print_confl_order() const +{ + vector > confl_ordered; + for (uint i = 0; i < depths_of_conflicts_for_group.size(); i++) { + double avg = 0.0; + for (vector::const_iterator it = depths_of_conflicts_for_group[i].begin(); it != depths_of_conflicts_for_group[i].end(); it++) + avg += *it; + if (depths_of_conflicts_for_group[i].size() > 0) { + avg /= (double) depths_of_conflicts_for_group[i].size(); + confl_ordered.push_back(std::make_pair(avg, i)); + } + } + + if (!confl_ordered.empty()) { + print_footer(); + print_simple_line(" Avg. conflict depth order of clause groups"); + print_header("groupno", "group name", "avg. depth"); + std::sort(confl_ordered.begin(), confl_ordered.end()); + print_groups(confl_ordered); + } +} + + +void Logger::print_times_var_guessed() const +{ + vector > times_var_ordered; + for (int i = 0; i < varnames.size(); i++) if (times_var_guessed[i] > 0) + times_var_ordered.push_back(std::make_pair(times_var_guessed[i], i)); + + if (!times_var_ordered.empty()) { + print_footer(); + print_simple_line(" No. times variable branched on"); + print_header("var", "var name", "no. times"); + std::sort(times_var_ordered.rbegin(), times_var_ordered.rend()); + print_vars(times_var_ordered); + } +} + +void Logger::print_times_group_caused_propagation() const +{ + vector > props_group_ordered; + for (uint i = 0; i < times_group_caused_propagation.size(); i++) + if (times_group_caused_propagation[i] > 0) + props_group_ordered.push_back(std::make_pair(times_group_caused_propagation[i], i)); + + if (!props_group_ordered.empty()) { + print_footer(); + print_simple_line(" No. propagations made by clause groups"); + print_header("group", "group name", "no. props"); + std::sort(props_group_ordered.rbegin(),props_group_ordered.rend()); + print_groups(props_group_ordered); + } +} + +void Logger::print_times_group_caused_conflict() const +{ + vector > confls_group_ordered; + for (uint i = 0; i < times_group_caused_conflict.size(); i++) + if (times_group_caused_conflict[i] > 0) + confls_group_ordered.push_back(std::make_pair(times_group_caused_conflict[i], i)); + + if (!confls_group_ordered.empty()) { + print_footer(); + print_simple_line(" No. conflicts made by clause groups"); + print_header("group", "group name", "no. confl"); + std::sort(confls_group_ordered.rbegin(), confls_group_ordered.rend()); + print_groups(confls_group_ordered); + } +} + +template +inline void Logger::print_line(const uint& number, const string& name, const T& value) const +{ + cout << "|" << std::setw(FST_WIDTH) << number << " " << std::setw(SND_WIDTH) << name << " " << std::setw(TRD_WIDTH) << value << "|" << endl; +} + +void Logger::print_header(const string& first, const string& second, const string& third) const +{ + cout << "|" << std::setw(FST_WIDTH) << first << " " << std::setw(SND_WIDTH) << second << " " << std::setw(TRD_WIDTH) << third << "|" << endl; + print_footer(); +} + +void Logger::print_groups(const vector >& to_print) const +{ + uint i = 0; + typedef vector >::const_iterator myiterator; + for (myiterator it = to_print.begin(); it != to_print.end() && i < max_print_lines; it++, i++) { + string name; + + if (it->second > max_group) + name = "learnt clause"; + else + name = groupnames[it->second]; + + print_line(it->second+1, name, it->first); + } + print_footer(); +} + +void Logger::print_groups(const vector >& to_print) const +{ + uint i = 0; + typedef vector >::const_iterator myiterator; + for (myiterator it = to_print.begin(); it != to_print.end() && i < max_print_lines; it++, i++) { + string name; + + if (it->second > max_group) + name = "learnt clause"; + else + name = groupnames[it->second]; + + print_line(it->second+1, name, it->first); + } + print_footer(); +} + +void Logger::print_vars(const vector >& to_print) const +{ + uint i = 0; + for (vector >::const_iterator it = to_print.begin(); it != to_print.end() && i < max_print_lines; it++, i++) + print_line(it->second+1, varnames[it->second], it->first); + + print_footer(); +} + +void Logger::print_vars(const vector >& to_print) const +{ + uint i = 0; + for (vector >::const_iterator it = to_print.begin(); it != to_print.end() && i < max_print_lines; it++, i++) { + print_line(it->second+1, varnames[it->second], it->first); + } + + print_footer(); +} + +template +void Logger::print_line(const string& str, const T& num) const +{ + cout << "|" << std::setw(FST_WIDTH+SND_WIDTH+4) << str << std::setw(TRD_WIDTH) << num << "|" << endl; +} + +void Logger::print_simple_line(const string& str) const +{ + cout << "|" << std::setw(FST_WIDTH+SND_WIDTH+TRD_WIDTH+4) << str << "|" << endl; +} + +void Logger::print_branch_depth_distrib() const +{ + //cout << "--- Branch depth stats ---" << endl; + + const uint range = 20; + map range_stat; + + for (map::const_iterator it = branch_depth_distrib.begin(); it != branch_depth_distrib.end(); it++) { + //cout << it->first << " : " << it->second << endl; + range_stat[it->first/range] += it->second; + } + //cout << endl; + + print_footer(); + print_simple_line(" No. search branches with branch depth between"); + print_line("Branch depth between", "no. br.-s"); + print_footer(); + + std::stringstream ss; + ss << "branch_depths/branch_depth_file" << runid << "-" << proof_num << ".txt"; + ofstream branch_depth_file; + branch_depth_file.open(ss.str().c_str()); + uint i = 0; + + for (map::iterator it = range_stat.begin(); it != range_stat.end(); it++) { + std::stringstream ss2; + ss2 << it->first*range << " - " << it->first*range + range-1; + print_line(ss2.str(), it->second); + + if (branch_depth_file.is_open()) { + branch_depth_file << i << "\t" << it->second << "\t"; + if (i % 5 == 0) + branch_depth_file << "\"" << it->first*range << "\""; + else + branch_depth_file << "\"\""; + branch_depth_file << endl; + } + i++; + } + if (branch_depth_file.is_open()) + branch_depth_file.close(); + print_footer(); + +} + +void Logger::print_general_stats(uint restarts, uint64_t conflicts, int vars, int noClauses, uint64_t clauses_Literals, int noLearnts, double litsPerLearntCl, double progressEstimate) const +{ + print_footer(); + print_simple_line(" Standard MiniSat restart statistics"); + print_footer(); + print_line("Restart number", restarts); + print_line("Number of conflicts", conflicts); + print_line("Number of variables", vars); + print_line("Number of clauses", noClauses); + print_line("Number of literals in clauses",clauses_Literals); + print_line("Avg. literals per learnt clause",litsPerLearntCl); + print_line("Progress estimate (%):", progressEstimate); + print_footer(); +} + + +// Prints statistics on the console +void Logger::printstats() const +{ + assert(statistics_on); + assert(varnames.size() == times_var_guessed.size()); + assert(varnames.size() == times_var_propagated.size()); + + printf("\n"); + cout << "+" << std::setfill('=') << std::setw(FST_WIDTH+SND_WIDTH+TRD_WIDTH+4) << "=" << "+" << endl; + cout << "||" << std::setfill('*') << std::setw(FST_WIDTH+SND_WIDTH+TRD_WIDTH+2) << "********* STATS FOR THIS RESTART BEGIN " << "||" << endl; + cout << "+" << std::setfill('=') << std::setw(FST_WIDTH+SND_WIDTH+TRD_WIDTH+4) << "=" << std::setfill(' ') << "+" << endl; + cout.setf(std::ios_base::left); + cout.precision(4); + print_times_var_guessed(); + print_times_group_caused_propagation(); + print_times_group_caused_conflict(); + print_prop_order(); + print_confl_order(); + print_assign_var_order(); + print_branch_depth_distrib(); + + print_footer(); + print_simple_line(" Advanced statistics"); + print_footer(); + print_line("No. branches visited", no_conflicts); + print_line("Avg. branch depth", (double)sum_conflict_depths/(double)no_conflicts); + print_line("No. decisions", no_decisions); + print_line("No. propagations",no_propagations); + + //printf("no progatations/no decisions (i.e. one decision gives how many propagations on average *for the whole search graph*): %f\n", (double)no_propagations/(double)no_decisions); + //printf("no propagations/sum decisions on branches (if you look at one specific branch, what is the average number of propagations you will find?): %f\n", (double)no_propagations/(double)sum_decisions_on_branches); + + print_simple_line("sum decisions on branches/no. branches"); + print_simple_line(" (in a given branch, what is the avg."); + print_line(" no. of decisions?)",(double)sum_decisions_on_branches/(double)no_conflicts); + + print_simple_line("sum propagations on branches/no. branches"); + print_simple_line(" (in a given branch, what is the"); + print_line(" avg. no. of propagations?)",(double)sum_propagations_on_branches/(double)no_conflicts); + print_footer(); + + print_footer(); + print_simple_line("Statistics note: If you used CryptoMiniSat as"); + print_simple_line("a library then vars are all shifted by 1 here"); + print_simple_line("and in every printed output of the solver."); + print_simple_line("This does not apply when you use CryptoMiniSat"); + print_simple_line("as a stand-alone program."); + print_footer(); +} + +// resets all stored statistics. Might be useful, to generate statistics for each restart and not for the whole search in general +void Logger::reset_statistics() +{ + assert(times_var_guessed.size() == times_var_propagated.size()); + assert(times_group_caused_conflict.size() == times_group_caused_propagation.size()); + + typedef vector::iterator vecit; + for (vecit it = times_var_guessed.begin(); it != times_var_guessed.end(); it++) + *it = 0; + + for (vecit it = times_var_propagated.begin(); it != times_var_propagated.end(); it++) + *it = 0; + + for (vecit it = times_group_caused_conflict.begin(); it != times_group_caused_conflict.end(); it++) + *it = 0; + + for (vecit it = times_group_caused_propagation.begin(); it != times_group_caused_propagation.end(); it++) + *it = 0; + + for (vecit it = confls_by_group.begin(); it != confls_by_group.end(); it++) + *it = 0; + + for (vecit it = props_by_group.begin(); it != props_by_group.end(); it++) + *it = 0; + + typedef vector >::iterator vecvecit; + + for (vecvecit it = depths_of_propagations_for_group.begin(); it != depths_of_propagations_for_group.end(); it++) + it->clear(); + + for (vecvecit it = depths_of_conflicts_for_group.begin(); it != depths_of_conflicts_for_group.end(); it++) + it->clear(); + + for (vecvecit it = depths_of_assigns_for_var.begin(); it != depths_of_assigns_for_var.end(); it++) + it->clear(); + + sum_conflict_depths = 0; + no_conflicts = 0; + no_decisions = 0; + no_propagations = 0; + decisions.clear(); + propagations.clear(); + sum_decisions_on_branches = 0; + sum_propagations_on_branches = 0; + branch_depth_distrib.clear(); +} +}; diff --git a/src/sat/cryptominisat/Logger.h b/src/sat/cryptominisat/Logger.h new file mode 100644 index 0000000..1fae9a7 --- /dev/null +++ b/src/sat/cryptominisat/Logger.h @@ -0,0 +1,159 @@ +/*********************************************************************************** +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +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 __LOGGER_H__ +#define __LOGGER_H__ + +#include +#include +//#include +#include + +#include "mtl/Vec.h" +#include "mtl/Heap.h" +#include "mtl/Alg.h" +#include "Logger.h" +#include "SolverTypes.h" +#include +#include +#include "stdint.h" +#include "limits.h" + +using std::vector; +using std::pair; +using std::string; +using std::map; + + +namespace MINISAT +{ +#ifndef uint +#define uint unsigned int +#endif + +class Logger +{ +public: + Logger(int& vebosity); + + //types of props, confl, and finish + enum prop_type { revert_guess_type, learnt_unit_clause_type, assumption_type, guess_type, addclause_type, simple_propagation_type, gauss_propagation_type }; + enum confl_type { simple_confl_type, gauss_confl_type }; + enum finish_type { model_found, unsat_model_found, restarting, done_adding_clauses }; + + //Conflict and propagation(guess is also a proapgation...) + void conflict(const confl_type type, uint goback, const uint group, const vec& learnt_clause); + void propagation(const Lit lit, const prop_type type, const uint group = UINT_MAX); + void empty_clause(const uint group); + + //functions to add/name variables + void new_var(const Var var); + void set_variable_name(const uint var, const char* name); + + //functions to add/name clause groups + void new_group(const uint group); + void set_group_name(const uint group, const char* name); + + void begin(); + void end(const finish_type finish); + void print_general_stats(uint restarts, uint64_t conflicts, int vars, int noClauses, uint64_t clauses_Literals, int noLearnts, double litsPerLearntCl, double progressEstimate) const; + + void newclause(const vec& ps, const bool xor_clause, const uint group); + + bool proof_graph_on; + bool statistics_on; +private: + void print_groups(const vector >& to_print) const; + void print_groups(const vector >& to_print) const; + void print_vars(const vector >& to_print) const; + void print_vars(const vector >& to_print) const; + void print_times_var_guessed() const; + void print_times_group_caused_propagation() const; + void print_times_group_caused_conflict() const; + void print_branch_depth_distrib() const; + + uint max_print_lines; + template + void print_line(const uint& number, const string& name, const T& value) const; + void print_header(const string& first, const string& second, const string& third) const; + void print_footer() const; + template + void print_line(const string& str, const T& num) const; + void print_simple_line(const string& str) const; + void print_confl_order() const; + void print_prop_order() const; + void print_assign_var_order() const; + void printstats() const; + void reset_statistics(); + + //internal data structures + uint uniqueid; //used to store the last unique ID given to a node + vec history; //stores the node uniqueIDs + uint level; //used to know the current level + uint begin_level; + uint max_group; + + //graph drawing + FILE* proof; //The file to store the proof + uint proof_num; + char filename0[80]; + uint runid; + uint proof0_lastid; + + //--------------------- + //statistics collection + //--------------------- + + //group and var names + vector groupnames; + vector varnames; + + //confls and props grouped by clause groups + vector confls_by_group; + vector props_by_group; + + //props and guesses grouped by vars + vector times_var_guessed; + vector times_var_propagated; + + vector times_group_caused_conflict; + vector times_group_caused_propagation; + + vector > depths_of_propagations_for_group; + vector > depths_of_conflicts_for_group; + vector > depths_of_assigns_for_var; + + //the distribution of branch depths. first = depth, second = number of occurances + map branch_depth_distrib; + + uint sum_conflict_depths; + uint no_conflicts; + uint no_decisions; + uint no_propagations; + vec decisions; + vec propagations; + uint sum_decisions_on_branches; + uint sum_propagations_on_branches; + + //message display properties + const int& verbosity; +}; + +}; +#endif //__LOGGER_H__ diff --git a/src/sat/cryptominisat/Makefile b/src/sat/cryptominisat/Makefile new file mode 100644 index 0000000..c68ce40 --- /dev/null +++ b/src/sat/cryptominisat/Makefile @@ -0,0 +1,12 @@ +include ../../../scripts/Makefile.common +MTL = mtl +CHDRS = $(wildcard *.h) $(wildcard $(MTL)/*.h) +EXEC = minisat +CFLAGS += -I$(MTL) -Wall -DEXT_HASH_MAP -ffloat-store $(CFLAGS_M32) +LFLAGS = -lz + +include mtl/template.mk +all: libminisat.a + ranlib libminisat.a + cp *.o ../ + cp libminisat.a ../ diff --git a/src/sat/cryptominisat/Solver.C b/src/sat/cryptominisat/Solver.C new file mode 100644 index 0000000..5559d75 --- /dev/null +++ b/src/sat/cryptominisat/Solver.C @@ -0,0 +1,1264 @@ +/****************************************************************************************[Solver.C] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +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 +#include +#include +#include +#include +#include "clause.h" + +namespace MINISAT +{ + +//================================================================================================= +// 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_user) + , verbosity (0) + , restrictedPickBranch(0) + , useRealUnknowns(false) + + // 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)) + , progress_estimate(0) + , remove_satisfied (true) + , mtrand((unsigned long int)0) + , logger(verbosity) + , dynamic_behaviour_analysis(false) //do not document the proof as default + , maxRestarts(UINT_MAX) + , learnt_clause_group(0) +{ +} + + +Solver::~Solver() +{ + for (int i = 0; i < learnts.size(); i++) free(learnts[i]); + for (int i = 0; i < unitary_learnts.size(); i++) free(unitary_learnts[i]); + for (int i = 0; i < clauses.size(); i++) free(clauses[i]); + for (int i = 0; i < xorclauses.size(); i++) free(xorclauses[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) + xorwatches.push(); // (list for variables in xors) + reason .push(NULL); + assigns .push(l_Undef); + level .push(-1); + activity .push(0); + seen .push(0); + polarity .push((char)sign); + + polarity .push((char)sign); + decision_var.push((char)dvar); + + insertVarOrder(v); + logger.new_var(v); + + return v; +} + +bool Solver::addXorClause(vec& ps, bool xor_clause_inverted, const uint group, const char* group_name) +{ + assert(decisionLevel() == 0); + + if (dynamic_behaviour_analysis) logger.set_group_name(group, group_name); + + if (!ok) + return false; + + // 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++) { + while (ps[i].var() >= nVars()) newVar(); + xor_clause_inverted ^= ps[i].sign(); + ps[i] ^= ps[i].sign(); + + if (ps[i] == p) { + //added, but easily removed + j--; + p = lit_Undef; + if (!assigns[ps[i].var()].isUndef()) + xor_clause_inverted ^= assigns[ps[i].var()].getBool(); + } else if (value(ps[i]) == l_Undef) //just add + ps[j++] = p = ps[i]; + else xor_clause_inverted ^= (value(ps[i]) == l_True); //modify xor_clause_inverted instead of adding + } + ps.shrink(i - j); + + if (ps.size() == 0) { + if (xor_clause_inverted) + return true; + + if (dynamic_behaviour_analysis) logger.empty_clause(group); + return ok = false; + } else if (ps.size() == 1) { + assert(value(ps[0]) == l_Undef); + uncheckedEnqueue( (xor_clause_inverted) ? ~ps[0] : ps[0]); + if (dynamic_behaviour_analysis) + logger.propagation((xor_clause_inverted) ? ~ps[0] : ps[0], Logger::addclause_type, group); + return ok = (propagate() == NULL); + } else { + learnt_clause_group = std::max(group+1, learnt_clause_group); + + XorClause* c = XorClause_new(ps, xor_clause_inverted, group); + + xorclauses.push(c); + attachClause(*c); + } + + return true; +} + +bool Solver::addClause(vec& ps, const uint group, const char* group_name) +{ + assert(decisionLevel() == 0); + + if (dynamic_behaviour_analysis) + logger.set_group_name(group, group_name); + + if (!ok) + return false; + + // 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++) { + while (ps[i].var() >= nVars()) newVar(); + + 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) { + if (dynamic_behaviour_analysis) logger.empty_clause(group); + return ok = false; + } else if (ps.size() == 1) { + assert(value(ps[0]) == l_Undef); + uncheckedEnqueue(ps[0]); + if (dynamic_behaviour_analysis) + logger.propagation(ps[0], Logger::addclause_type, group); + return ok = (propagate() == NULL); + } else { + learnt_clause_group = std::max(group+1, learnt_clause_group); + + Clause* c = Clause_new(ps, group); + + clauses.push(c); + attachClause(*c); + } + + return true; +} + +void Solver::attachClause(XorClause& c) +{ + assert(c.size() > 1); + + xorwatches[c[0].var()].push(&c); + xorwatches[c[1].var()].push(&c); + + if (c.learnt()) learnts_literals += c.size(); + else clauses_literals += c.size(); +} + +void Solver::attachClause(Clause& c) +{ + assert(c.size() > 1); + + watches[(~c[0]).toInt()].push(&c); + watches[(~c[1]).toInt()].push(&c); + + if (c.learnt()) learnts_literals += c.size(); + else clauses_literals += c.size(); +} + + +void Solver::detachClause(const XorClause& c) +{ + assert(c.size() > 1); + assert(find(xorwatches[c[0].var()], &c)); + assert(find(xorwatches[c[1].var()], &c)); + remove(xorwatches[c[0].var()], &c); + remove(xorwatches[c[1].var()], &c); + + if (c.learnt()) learnts_literals -= c.size(); + else clauses_literals -= c.size(); +} + +void Solver::detachClause(const Clause& c) +{ + assert(c.size() > 1); + assert(find(watches[(~c[0]).toInt()], &c)); + assert(find(watches[(~c[1]).toInt()], &c)); + remove(watches[(~c[0]).toInt()], &c); + remove(watches[(~c[1]).toInt()], &c); + if (c.learnt()) learnts_literals -= c.size(); + else clauses_literals -= c.size(); +} + +template +void Solver::removeClause(T& c) +{ + detachClause(c); + free(&c); +} + + +bool Solver::satisfied(const Clause& c) const +{ + for (uint i = 0; i < c.size(); i++) + if (value(c[i]) == l_True) + return true; + return false; +} + +bool Solver::satisfied(const XorClause& c) const +{ + bool final = c.xor_clause_inverted(); + for (uint k = 0; k < c.size(); k++ ) { + const lbool& val = assigns[c[k].var()]; + if (val.isUndef()) return false; + final ^= val.getBool(); + } + return final; +} + + +// Revert to the state at given level (keeping all assignment at 'level' but not beyond). +// +void Solver::cancelUntil(int level) +{ + #ifdef VERBOSE_DEBUG + cout << "Canceling until level " << level; + if (level > 0) cout << " sublevel: " << trail_lim[level]; + cout << endl; + #endif + + if (decisionLevel() > level) { + for (int c = trail.size()-1; c >= trail_lim[level]; c--) { + Var x = trail[c].var(); + #ifdef VERBOSE_DEBUG + cout << "Canceling var " << x+1 << " sublevel:" << c << endl; + #endif + assigns[x] = l_Undef; + insertVarOrder(x); + } + qhead = trail_lim[level]; + trail.shrink(trail.size() - trail_lim[level]); + trail_lim.shrink(trail_lim.size() - level); + } + + #ifdef VERBOSE_DEBUG + cout << "Canceling finished. (now at level: " << decisionLevel() << " sublevel:" << trail.size()-1 << ")" << endl; + #endif +} + +//Permutates the clauses in the solver. Very useful to calcuate the average time it takes the solver to solve the prolbem +void Solver::permutateClauses() +{ + for (int i = 0; i < clauses.size(); i++) { + int j = mtrand.randInt(i); + Clause* tmp = clauses[i]; + clauses[i] = clauses[j]; + clauses[j] = tmp; + } + + for (int i = 0; i < xorclauses.size(); i++) { + int j = mtrand.randInt(i); + XorClause* tmp = xorclauses[i]; + xorclauses[i] = xorclauses[j]; + xorclauses[j] = tmp; + } +} + +void Solver::setRealUnknown(const uint var) +{ + if (realUnknowns.size() < var+1) + realUnknowns.resize(var+1, false); + realUnknowns[var] = true; +} + +void Solver::printLit(const Lit l) const +{ + printf("%s%d:%c", l.sign() ? "-" : "", l.var()+1, value(l) == l_True ? '1' : (value(l) == l_False ? '0' : 'X')); +} + + +void Solver::printClause(const Clause& c) const +{ + printf("(group: %d) ", c.group); + for (uint i = 0; i < c.size();) { + printLit(c[i]); + i++; + if (i < c.size()) printf(" "); + } +} + +void Solver::printClause(const XorClause& c) const +{ + printf("(group: %d) ", c.group); + if (c.xor_clause_inverted()) printf(" /inverted/ "); + for (uint i = 0; i < c.size();) { + printLit(c[i].unsign()); + i++; + if (i < c.size()) printf(" + "); + } +} + +//================================================================================================= +// Major methods: + + +Lit Solver::pickBranchLit(int polarity_mode) +{ + #ifdef VERBOSE_DEBUG + cout << "decision level:" << decisionLevel() << " "; + #endif + + Var next = var_Undef; + + // Random decision: + if (mtrand.randDblExc() < random_var_freq && !order_heap.empty()) { + if (restrictedPickBranch == 0) next = order_heap[mtrand.randInt(order_heap.size()-1)]; + else next = order_heap[mtrand.randInt(std::min((uint32_t)order_heap.size()-1, restrictedPickBranch))]; + + if (assigns[next] == l_Undef && decision_var[next]) + rnd_decisions++; + } + + // Activity based decision: + //bool dont_do_bad_decision = false; + //if (restrictedPickBranch != 0) dont_do_bad_decision = (mtrand.randInt(100) != 0); + while (next == var_Undef || 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: + if (next != var_Undef) + sign = polarity[next]; + break; + case polarity_rnd: + sign = mtrand.randInt(1); + break; + default: + assert(false); + } + + assert(next == var_Undef || value(next) == l_Undef); + + if (next == var_Undef) { + #ifdef VERBOSE_DEBUG + cout << "SAT!" << endl; + #endif + return lit_Undef; + } else { + Lit lit(next,sign); + #ifdef VERBOSE_DEBUG + cout << "decided on: " << lit.var()+1 << " to set:" << !lit.sign() << endl; + #endif + return lit; + } +} + + +/*_________________________________________________________________________________________________ +| +| analyze : (confl : Clause*) (out_learnt : vec&) (out_btlevel : int&) -> [void] +| +| Description: +| Analyze conflict and produce a reason clause. +| +| Pre-conditions: +| * 'out_learnt' is assumed to be cleared. +| * Current decision level must be greater than root level. +| +| Post-conditions: +| * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'. +| +| Effect: +| Will undo part of the trail, upto but not beyond the assumption of the current decision level. +|________________________________________________________________________________________________@*/ +void Solver::analyze(Clause* confl, vec& out_learnt, int& out_btlevel) +{ + int pathC = 0; + Lit p = lit_Undef; + + // Generate conflict clause: + // + out_learnt.push(); // (leave room for the asserting literal) + int index = trail.size() - 1; + out_btlevel = 0; + + do { + assert(confl != NULL); // (otherwise should be UIP) + Clause& c = *confl; + + if (c.learnt()) + claBumpActivity(c); + + for (uint j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++) { + const Lit& q = c[j]; + const uint my_var = q.var(); + + if (!seen[my_var] && level[my_var] > 0) { + if (!useRealUnknowns || (my_var < realUnknowns.size() && realUnknowns[my_var])) + varBumpActivity(my_var); + seen[my_var] = 1; + if (level[my_var] >= decisionLevel()) + pathC++; + else { + out_learnt.push(q); + if (level[my_var] > out_btlevel) + out_btlevel = level[my_var]; + } + } + } + + // Select next clause to look at: + while (!seen[trail[index--].var()]); + p = trail[index+1]; + confl = reason[p.var()]; + seen[p.var()] = 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(out_learnt[i].var()); // (maintain an abstraction of levels involved in conflict) + + out_learnt.copyTo(analyze_toclear); + for (i = j = 1; i < out_learnt.size(); i++) + if (reason[out_learnt[i].var()] == 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++) { + const Clause& c = *reason[out_learnt[i].var()]; + for (uint k = 1; k < c.size(); k++) + if (!seen[c[k].var()] && level[c[k].var()] > 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[out_learnt[i].var()] > level[out_learnt[max_i].var()]) + max_i = i; + Lit p = out_learnt[max_i]; + out_learnt[max_i] = out_learnt[1]; + out_learnt[1] = p; + out_btlevel = level[p.var()]; + } + + + for (int j = 0; j < analyze_toclear.size(); j++) seen[analyze_toclear[j].var()] = 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[analyze_stack.last().var()] != NULL); + const Clause& c = *reason[analyze_stack.last().var()]; + analyze_stack.pop(); + + for (uint i = 1; i < c.size(); i++) { + Lit p = c[i]; + if (!seen[p.var()] && level[p.var()] > 0) { + if (reason[p.var()] != NULL && (abstractLevel(p.var()) & abstract_levels) != 0) { + seen[p.var()] = 1; + analyze_stack.push(p); + analyze_toclear.push(p); + } else { + for (int j = top; j < analyze_toclear.size(); j++) + seen[analyze_toclear[j].var()] = 0; + analyze_toclear.shrink(analyze_toclear.size() - top); + return false; + } + } + } + } + + return true; +} + + +/*_________________________________________________________________________________________________ +| +| analyzeFinal : (p : Lit) -> [void] +| +| Description: +| Specialized analysis procedure to express the final conflict in terms of assumptions. +| Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and +| stores the result in 'out_conflict'. +|________________________________________________________________________________________________@*/ +void Solver::analyzeFinal(Lit p, vec& out_conflict) +{ + out_conflict.clear(); + out_conflict.push(p); + + if (decisionLevel() == 0) + return; + + seen[p.var()] = 1; + + for (int i = trail.size()-1; i >= trail_lim[0]; i--) { + Var x = trail[i].var(); + if (seen[x]) { + if (reason[x] == NULL) { + assert(level[x] > 0); + out_conflict.push(~trail[i]); + } else { + const Clause& c = *reason[x]; + for (uint j = 1; j < c.size(); j++) + if (level[c[j].var()] > 0) + seen[c[j].var()] = 1; + } + seen[x] = 0; + } + } + + seen[p.var()] = 0; +} + + +void Solver::uncheckedEnqueue(Lit p, Clause* from) +{ + #ifdef VERBOSE_DEBUG + cout << "uncheckedEnqueue var " << p.var()+1 << " to " << !p.sign() << " level: " << decisionLevel() << " sublevel:" << trail.size() << endl; + #endif + + assert(value(p) == l_Undef); + const Var v = p.var(); + assigns [v] = boolToLBool(!p.sign());//lbool(!sign(p)); // <<== abstract but not uttermost effecient + level [v] = decisionLevel(); + reason [v] = from; + polarity[p.var()] = p.sign(); + 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(const bool xor_as_well) +{ + Clause* confl = NULL; + int num_props = 0; + + #ifdef VERBOSE_DEBUG + cout << "Propagation started" << endl; + #endif + + while (qhead < trail.size()) { + Lit p = trail[qhead++]; // 'p' is enqueued fact to propagate. + vec& ws = watches[p.toInt()]; + Clause **i, **j, **end; + num_props++; + + #ifdef VERBOSE_DEBUG + cout << "Propagating lit " << (p.sign() ? '-' : ' ') << p.var()+1 << endl; + #endif + + for (i = j = ws.getData(), end = i + ws.size(); i != end;) { + Clause& c = **i++; + + // Make sure the false literal is data[1]: + const 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. + const Lit& first = c[0]; + if (value(first) == l_True) { + *j++ = &c; + } else { + // Look for new watch: + for (uint k = 2; k < c.size(); k++) + if (value(c[k]) != l_False) { + c[1] = c[k]; + c[k] = false_lit; + watches[(~c[1]).toInt()].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); + if (dynamic_behaviour_analysis) + logger.propagation(first,Logger::simple_propagation_type,c.group); + } + } +FoundWatch: + ; + } + ws.shrink(i - j); + + if (xor_as_well && !confl) confl = propagate_xors(p); + } + propagations += num_props; + simpDB_props -= num_props; + + #ifdef VERBOSE_DEBUG + cout << "Propagation ended." << endl; + #endif + + return confl; +} + +Clause* Solver::propagate_xors(const Lit& p) +{ + #ifdef VERBOSE_DEBUG_XOR + cout << "Xor-Propagating variable " << p.var()+1 << endl; + #endif + + Clause* confl = NULL; + + vec& ws = xorwatches[p.var()]; + XorClause **i, **j, **end; + for (i = j = ws.getData(), end = i + ws.size(); i != end;) { + XorClause& c = **i++; + + // Make sure the false literal is data[1]: + if (c[0].var() == p.var()) { + Lit tmp(c[0]); + c[0] = c[1]; + c[1] = tmp; + } + assert(c[1].var() == p.var()); + + #ifdef VERBOSE_DEBUG_XOR + cout << "--> xor thing -- " << endl; + printClause(c); + cout << endl; + #endif + bool final = c.xor_clause_inverted(); + for (int k = 0, size = c.size(); k < size; k++ ) { + const lbool& val = assigns[c[k].var()]; + if (val.isUndef() && k >= 2) { + Lit tmp(c[1]); + c[1] = c[k]; + c[k] = tmp; + #ifdef VERBOSE_DEBUG_XOR + cout << "new watch set" << endl << endl; + #endif + xorwatches[c[1].var()].push(&c); + goto FoundWatch; + } + + c[k] = c[k].unsign() ^ val.getBool(); + final ^= val.getBool(); + } + + + { + // Did not find watch -- clause is unit under assignment: + *j++ = &c; + + #ifdef VERBOSE_DEBUG_XOR + cout << "final: " << std::boolalpha << final << " - "; + #endif + if (assigns[c[0].var()].isUndef()) { + c[0] = c[0].unsign()^final; + + #ifdef VERBOSE_DEBUG_XOR + cout << "propagating "; + printLit(c[0]); + cout << endl; + cout << "propagation clause -- "; + printClause(*(Clause*)&c); + cout << endl << endl; + #endif + + uncheckedEnqueue(c[0], (Clause*)&c); + if (dynamic_behaviour_analysis) + logger.propagation(c[0], Logger::simple_propagation_type, c.group); + } else if (!final) { + + #ifdef VERBOSE_DEBUG_XOR + printf("conflict clause -- "); + printClause(*(Clause*)&c); + cout << endl << endl; + #endif + + confl = (Clause*)&c; + qhead = trail.size(); + // Copy the remaining watches: + while (i < end) + *j++ = *i++; + } else { + #ifdef VERBOSE_DEBUG_XOR + printf("xor satisfied\n"); + #endif + + Lit tmp(c[0]); + c[0] = c[1]; + c[1] = tmp; + } + } +FoundWatch: + ; + } + ws.shrink(i - j); + + 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); +} + +const vec& Solver::get_sorted_learnts() +{ + sort(learnts, reduceDB_lt()); + return learnts; +} + +const vec& Solver::get_unitary_learnts() const +{ + return unitary_learnts; +} + +void Solver::setMaxRestarts(const uint num) +{ + maxRestarts = num; +} + +template +void Solver::removeSatisfied(vec& cs) +{ + int i,j; + for (i = j = 0; i < cs.size(); i++) { + if (satisfied(*cs[i])) + removeClause(*cs[i]); + else + cs[j++] = cs[i]; + } + cs.shrink(i - j); +} + +void Solver::cleanClauses(vec& cs) +{ + uint useful = 0; + for (int s = 0; s < cs.size(); s++) { + Clause& c = *cs[s]; + Lit *i, *j, *end; + uint at = 0; + for (i = j = c.getData(), end = i + c.size(); i != end; i++, at++) { + if (value(*i) == l_Undef) { + *j = *i; + j++; + } else assert(at > 1); + assert(value(*i) != l_True); + } + c.shrink(i-j); + if (i-j > 0) useful++; + } + #ifdef VERBOSE_DEBUG + cout << "cleanClauses(Clause) useful:" << useful << endl; + #endif +} + +void Solver::cleanClauses(vec& cs) +{ + uint useful = 0; + for (int s = 0; s < cs.size(); s++) { + XorClause& c = *cs[s]; + Lit *i, *j, *end; + uint at = 0; + for (i = j = c.getData(), end = i + c.size(); i != end; i++, at++) { + const lbool& val = assigns[i->var()]; + if (val.isUndef()) { + *j = *i; + j++; + } else /*assert(at>1),*/ c.invert(val.getBool()); + } + c.shrink(i-j); + if (i-j > 0) useful++; + } + #ifdef VERBOSE_DEBUG + cout << "cleanClauses(XorClause) useful:" << useful << endl; + #endif +} + +/*_________________________________________________________________________________________________ +| +| 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. +|________________________________________________________________________________________________@*/ +lbool Solver::simplify() +{ + assert(decisionLevel() == 0); + + if (!ok || propagate() != NULL) { + if (dynamic_behaviour_analysis) { + logger.end(Logger::unsat_model_found); + logger.print_general_stats(starts, conflicts, order_heap.size(), nClauses(), clauses_literals, nLearnts(), (double)learnts_literals/nLearnts(), progress_estimate*100); + } + ok = false; + return l_False; + } + + if (nAssigns() == simpDB_assigns || (simpDB_props > 0)) { + return l_Undef; + } + + // Remove satisfied clauses: + removeSatisfied(learnts); + if (remove_satisfied) { // Can be turned off. + removeSatisfied(clauses); + removeSatisfied(xorclauses); + } + + // 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) + + //cleanClauses(clauses); + cleanClauses(xorclauses); + //cleanClauses(learnts); + + return l_Undef; +} + + +/*_________________________________________________________________________________________________ +| +| 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 conflictC = 0; + vec learnt_clause; + llbool ret; + + starts++; + + if (dynamic_behaviour_analysis) logger.begin(); + + for (;;) { + Clause* confl = propagate(); + + if (confl != NULL) { + ret = handle_conflict(learnt_clause, confl, conflictC); + if (ret != l_Nothing) return ret; + } else { + ret = new_decision(nof_conflicts, nof_learnts, conflictC); + if (ret != l_Nothing) return ret; + } + } +} + +llbool Solver::new_decision(int& nof_conflicts, int& nof_learnts, int& conflictC) +{ + if (nof_conflicts >= 0 && conflictC >= nof_conflicts) { + // Reached bound on number of conflicts: + progress_estimate = progressEstimate(); + cancelUntil(0); + if (dynamic_behaviour_analysis) { + logger.end(Logger::restarting); + logger.print_general_stats(starts, conflicts, order_heap.size(), nClauses(), clauses_literals, nLearnts(), (double)learnts_literals/nLearnts(), progress_estimate*100); + } + return l_Undef; + } + + // Simplify the set of problem clauses: + if (decisionLevel() == 0 && simplify() == l_False) { + if (dynamic_behaviour_analysis) { + logger.end(Logger::unsat_model_found); + logger.print_general_stats(starts, conflicts, order_heap.size(), nClauses(), clauses_literals, nLearnts(), (double)learnts_literals/nLearnts(), progress_estimate*100); + } + 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(); + if (dynamic_behaviour_analysis) logger.propagation(p, Logger::assumption_type); + } else if (value(p) == l_False) { + analyzeFinal(~p, conflict); + if (dynamic_behaviour_analysis) { + logger.end(Logger::unsat_model_found); + logger.print_general_stats(starts, conflicts, order_heap.size(), nClauses(), clauses_literals, nLearnts(), (double)learnts_literals/nLearnts(), progress_estimate*100); + } + return l_False; + } else { + next = p; + break; + } + } + + if (next == lit_Undef) { + // New variable decision: + decisions++; + next = pickBranchLit(polarity_mode); + + if (next == lit_Undef) { + // Model found: + if (dynamic_behaviour_analysis) { + logger.end(Logger::model_found); + logger.print_general_stats(starts, conflicts, order_heap.size(), nClauses(), clauses_literals, nLearnts(), (double)learnts_literals/nLearnts(), progress_estimate*100); + } + return l_True; + } + } + + // Increase decision level and enqueue 'next' + assert(value(next) == l_Undef); + newDecisionLevel(); + uncheckedEnqueue(next); + if (dynamic_behaviour_analysis) logger.propagation(next, Logger::guess_type); + + return l_Nothing; +} + +llbool Solver::handle_conflict(vec& learnt_clause, Clause* confl, int& conflictC) +{ + #ifdef VERBOSE_DEBUG + cout << "Handling conflict: "; + for (uint i = 0; i < learnt_clause.size(); i++) + cout << learnt_clause[i].var()+1 << ","; + cout << endl; + #endif + + int backtrack_level; + + conflicts++; + conflictC++; + if (decisionLevel() == 0) { + if (dynamic_behaviour_analysis) { + logger.end(Logger::unsat_model_found); + logger.print_general_stats(starts, conflicts, order_heap.size(), nClauses(), clauses_literals, nLearnts(), (double)learnts_literals/nLearnts(), progress_estimate*100); + } + return l_False; + } + learnt_clause.clear(); + analyze(confl, learnt_clause, backtrack_level); + cancelUntil(backtrack_level); + if (dynamic_behaviour_analysis) + logger.conflict(Logger::simple_confl_type, backtrack_level, confl->group, learnt_clause); + + #ifdef VERBOSE_DEBUG + cout << "Learning:"; + for (uint i = 0; i < learnt_clause.size(); i++) printLit(learnt_clause[i]), cout << " "; + cout << endl; + cout << "reverting var " << learnt_clause[0].var()+1 << " to " << !learnt_clause[0].sign() << endl; + #endif + + assert(value(learnt_clause[0]) == l_Undef); + //Unitary learnt + if (learnt_clause.size() == 1) { + Clause* c = Clause_new(learnt_clause, learnt_clause_group++, true); + unitary_learnts.push(c); + uncheckedEnqueue(learnt_clause[0]); + if (dynamic_behaviour_analysis) + logger.propagation(learnt_clause[0], Logger::learnt_unit_clause_type); + assert(backtrack_level == 0 && "Unit clause learnt, so must cancel until level 0, right?"); + + #ifdef VERBOSE_DEBUG + cout << "Unit clause learnt." << endl; + #endif + //Normal learnt + } else { + Clause* c = Clause_new(learnt_clause, learnt_clause_group++, true); + learnts.push(c); + attachClause(*c); + claBumpActivity(*c); + uncheckedEnqueue(learnt_clause[0], c); + + if (dynamic_behaviour_analysis) { + logger.propagation(learnt_clause[0], Logger::revert_guess_type, c->group); + logger.new_group(c->group); + logger.set_group_name(c->group, "learnt clause"); + } + } + + varDecayActivity(); + claDecayActivity(); + + return l_Nothing; +} + + +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(); +} + + +lbool Solver::solve(const vec& assumps) +{ + model.clear(); + conflict.clear(); + + if (!ok) return l_False; + + assumps.copyTo(assumptions); + + double nof_conflicts = restart_first; + double nof_learnts = nClauses() * learntsize_factor; + lbool status = l_Undef; + + if (verbosity >= 1) { + printf("============================[ Search Statistics ]==============================\n"); + printf("| Conflicts | ORIGINAL | LEARNT | Progress |\n"); + printf("| | Vars Clauses Literals | Limit Clauses Lit/Cl | |\n"); + printf("===============================================================================\n"); + } + + // Search: + while (status == l_Undef && starts < maxRestarts) { + if (verbosity >= 1 && !(dynamic_behaviour_analysis && logger.statistics_on)) { + printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |", (int)conflicts, order_heap.size(), nClauses(), (int)clauses_literals, (int)nof_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progress_estimate*100), fflush(stdout); + printf("\n"); + } + status = search((int)nof_conflicts, (int)nof_learnts); + nof_conflicts *= restart_inc; + nof_learnts *= learntsize_inc; + } + + if (verbosity >= 1) { + printf("==============================================================================="); + printf("\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 + } if (status == l_False) { + if (conflict.size() == 0) + ok = false; + } + + cancelUntil(0); + return status; +} + +//================================================================================================= +// Debug methods: + + +void Solver::verifyModel() +{ + bool failed = false; + for (int i = 0; i < clauses.size(); i++) { + Clause& c = *clauses[i]; + for (uint j = 0; j < c.size(); j++) + if (modelValue(c[j]) == l_True) + goto next; + + printf("unsatisfied clause: "); + printClause(*clauses[i]); + printf("\n"); + failed = true; +next: + ; + } + + for (int i = 0; i < xorclauses.size(); i++) { + XorClause& c = *xorclauses[i]; + bool final = c.xor_clause_inverted(); + for (uint j = 0; j < c.size(); j++) + final ^= (modelValue(c[j].unsign()) == l_True); + if (!final) { + printf("unsatisfied clause: "); + printClause(*xorclauses[i]); + printf("\n"); + failed = true; + } + } + + assert(!failed); + + printf("Verified %d original clauses.\n", clauses.size() + xorclauses.size()); +} + + +void Solver::checkLiteralCount() +{ + // Check that sizes are calculated correctly: + int cnt = 0; + for (int i = 0; i < clauses.size(); i++) + cnt += clauses[i]->size(); + + for (int i = 0; i < xorclauses.size(); i++) + cnt += xorclauses[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); + } +} +}; diff --git a/src/sat/cryptominisat/Solver.h b/src/sat/cryptominisat/Solver.h new file mode 100644 index 0000000..b5a2d78 --- /dev/null +++ b/src/sat/cryptominisat/Solver.h @@ -0,0 +1,431 @@ +/****************************************************************************************[Solver.h] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ + +#ifndef Solver_h +#define Solver_h + +#include +#include "mtl/Vec.h" +#include "mtl/Heap.h" +#include "mtl/Alg.h" +#include "Logger.h" +#include "MTRand/MersenneTwister.h" +#include "SolverTypes.h" +#include "clause.h" +#include + +#ifdef _MSC_VER + #include +#else + #include + #include + #include +#endif + +namespace MINISAT +{ + +//#define VERBOSE_DEBUG_XOR +//#define VERBOSE_DEBUG + +//================================================================================================= +// Solver -- the main class: + + +class Solver +{ +public: + + // Constructor/Destructor: + // + Solver(); + ~Solver(); + + // Problem specification: + // + Var newVar (bool polarity = true, bool dvar = true); // Add a new variable with parameters specifying variable mode. + bool addClause (vec& ps, const uint group, const char* group_name); // Add a clause to the solver. NOTE! 'ps' may be shrunk by this method! + bool addXorClause (vec& ps, bool xor_clause_inverted, const uint group, const char* group_name); // Add a xor-clause to the solver. NOTE! 'ps' may be shrunk by this method! + + // Solving: + // + lbool simplify (); // Removes already satisfied clauses. + lbool solve (const vec& assumps); // Search for a model that respects a given set of assumptions. + lbool 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. + void setSeed (const uint32_t seed); // Sets the seed to be the given number + void permutateClauses(); // Permutates the clauses using the seed. It updates the seed in mtrand + void needRealUnknowns(); // Uses the "real unknowns" set by setRealUnknown + void setRealUnknown(const uint var); //sets a variable to be 'real', i.e. to preferentially branch on it during solving (when useRealUnknown it turned on) + void setMaxRestarts(const uint num); //sets the maximum number of restarts to given value + + // Read state: + // + lbool value (const Var& x) const; // The current value of a variable. + lbool value (const Lit& p) const; // The current value of a literal. + lbool modelValue (const Lit& p) const; // The value of a literal in the last model. The last call to solve must have been satisfiable. + int nAssigns () const; // The current number of assigned literals. + int nClauses () const; // The current number of original clauses. + int nLearnts () const; // The current number of learnt clauses. + int nVars () const; // The current number of variables. + + // Extra results: (read-only member variable) + // + vec model; // If problem is satisfiable, this vector contains the model (if any). + vec conflict; // If problem is unsatisfiable (possibly under assumptions), + // this vector represent the final conflict clause expressed in the assumptions. + + // Mode of operation: + // + double var_decay; // Inverse of the variable activity decay factor. (default 1 / 0.95) + double clause_decay; // Inverse of the clause activity decay factor. (1 / 0.999) + double random_var_freq; // The frequency with which the decision heuristic tries to choose a random variable. (default 0.02) + int restart_first; // The initial restart limit. (default 100) + double restart_inc; // The factor with which the restart limit is multiplied in each restart. (default 1.5) + double learntsize_factor; // The intitial limit for learnt clauses is a factor of the original clauses. (default 1 / 3) + double learntsize_inc; // The limit for learnt clauses is multiplied with this factor each restart. (default 1.1) + bool expensive_ccmin; // Controls conflict clause minimization. (default TRUE) + int polarity_mode; // Controls which polarity the decision heuristic chooses. See enum below for allowed modes. (default polarity_false) + int verbosity; // Verbosity level. 0=silent, 1=some progress report (default 0) + uint restrictedPickBranch; // Pick variables to branch on preferentally from the highest [0, restrictedPickBranch]. If set to 0, preferentiality is turned off (i.e. picked randomly between [0, all]) + bool useRealUnknowns; // Whether 'real unknown' optimization should be used. If turned on, VarActivity is only bumped for variables for which the real_unknowns[var] == true + vector realUnknowns; // The important variables. This vector stores 'false' at realUnknowns[var] if the var is not a real unknown, and stores a 'true' if it is a real unkown. If var is larger than realUnkowns.size(), then it is not an important variable + + 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; + + //Logging + void needStats(); // Prepares the solver to output statistics + void needProofGraph(); // Prepares the solver to output proof graphs during solving + void setVariableName(int var, const char* name); // Sets the name of the variable 'var' to 'name'. Useful for statistics and proof logs (i.e. used by 'logger') + void startClauseAdding(); // Before adding clauses, but after setting up the Solver (need* functions, verbosity), this should be called + void endFirstSimplify(); // After the clauses are added, and the first simplify() is called, this must be called + const vec& get_sorted_learnts(); //return the set of learned clauses + const vec& get_unitary_learnts() const; //return the set of unitary learned clauses + +protected: + // Helper structures: + // + struct VarOrderLt { + const vec& activity; + bool operator () (Var x, Var y) const { + return activity[x] > activity[y]; + } + VarOrderLt(const vec& act) : activity(act) { } + }; + + friend class VarFilter; + struct VarFilter { + const Solver& s; + VarFilter(const Solver& _s) : s(_s) {} + bool operator()(Var v) const { + return s.assigns[v].isUndef() && s.decision_var[v]; + } + }; + + // Solver state: + // + bool ok; // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used! + vec clauses; // List of problem clauses. + vec xorclauses; // List of problem xor-clauses. + vec learnts; // List of learnt clauses. + vec unitary_learnts; // List of learnt clauses. + double cla_inc; // Amount to bump next clause with. + vec activity; // A heuristic measurement of the activity of a variable. + double var_inc; // Amount to bump next variable with. + vec > watches; // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true). + vec > xorwatches; // 'xorwatches[var]' is a list of constraints watching var in XOR clauses. + vec assigns; // The current assignments + vec polarity; // The preferred polarity of each variable. + vec decision_var; // Declares if a variable is eligible for selection in the decision heuristic. + vec trail; // Assignment stack; stores all assigments made in the order they were made. + vec trail_lim; // Separator indices for different decision levels in 'trail'. + vec reason; // 'reason[var]' is the clause that implied the variables current value, or 'NULL' if none. + vec level; // 'level[var]' contains the level at which the assignment was made. + int qhead; // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat). + int simpDB_assigns; // Number of top-level assignments since last execution of 'simplify()'. + int64_t simpDB_props; // Remaining number of propagations that must be made before next execution of 'simplify()'. + vec assumptions; // Current set of assumptions provided to solve by the user. + Heap order_heap; // A priority queue of variables ordered with respect to the variable activity. + double progress_estimate;// Set by 'search()'. + bool remove_satisfied; // Indicates whether possibly inefficient linear scan for satisfied clauses should be performed in 'simplify'. + MTRand mtrand; // random number generator + Logger logger; // dynamic logging, statistics + bool dynamic_behaviour_analysis; //should 'logger' be called whenever a propagation/conflict/decision is made? + uint maxRestarts; // More than this number of restarts will not be performed + + // Temporaries (to reduce allocation overhead). Each variable is prefixed by the method in which it is + // used, exept 'seen' wich is used in several places. + // + vec seen; + vec analyze_stack; + vec analyze_toclear; + vec add_tmp; + + //Logging + uint learnt_clause_group; //the group number of learnt clauses. Incremented at each added learnt clause + + // Main internal methods: + // + void insertVarOrder (Var x); // Insert a variable in the decision order priority queue. + Lit pickBranchLit (int polarity_mode); // 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 (const bool xor_as_well = true); // Perform unit propagation. Returns possibly conflicting clause. + Clause* propagate_xors (const Lit& p); + void cancelUntil (int level); // Backtrack until a certain level. + void analyze (Clause* confl, vec& out_learnt, int& out_btlevel); // (bt = backtrack) + void analyzeFinal (Lit p, vec& out_conflict); // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION? + bool litRedundant (Lit p, uint32_t abstract_levels); // (helper method for 'analyze()') + lbool search (int nof_conflicts, int nof_learnts); // Search for a given number of conflicts. + void reduceDB (); // Reduce the set of learnt clauses. + template + void removeSatisfied (vec& cs); // Shrink 'cs' to contain only non-satisfied clauses. + void cleanClauses (vec& cs); + void cleanClauses (vec& cs); // Remove TRUE or FALSE variables from the xor clauses and remove the FALSE variables from the normal clauses + llbool handle_conflict (vec& learnt_clause, Clause* confl, int& conflictC);// Handles the conflict clause + llbool new_decision (int& nof_conflicts, int& nof_learnts, int& conflictC); // Handles the case when all propagations have been made, and now a decision must be made + + // 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 (XorClause& c); + void attachClause (Clause& c); // Attach a clause to watcher lists. + void detachClause (const XorClause& c); + void detachClause (const Clause& c); // Detach a clause to watcher lists. + template + void removeClause(T& 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 XorClause& c) const; // Returns TRUE if the clause is satisfied in the current state + bool satisfied (const Clause& c) const; // Returns TRUE if the clause is satisfied in the current state. + + // Misc: + // + int decisionLevel () const; // Gives the current decisionlevel. + uint32_t abstractLevel (const 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 (const Lit l) const; + void printClause (const Clause& c) const; + void printClause (const XorClause& c) const; + void verifyModel (); + void checkLiteralCount(); +}; + + +//================================================================================================= +// 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[c[0].var()] == &c && value(c[0]) == l_True; +} +inline void Solver::newDecisionLevel() +{ + trail_lim.push(trail.size()); + #ifdef VERBOSE_DEBUG + std::cout << "New decision level:" << trail_lim.size() << std::endl; + #endif +} +inline int Solver::decisionLevel () const +{ + return trail_lim.size(); +} +inline uint32_t Solver::abstractLevel (const Var& x) const +{ + return 1 << (level[x] & 31); +} +inline lbool Solver::value (const Var& x) const +{ + return assigns[x]; +} +inline lbool Solver::value (const Lit& p) const +{ + return assigns[p.var()] ^ p.sign(); +} +inline lbool Solver::modelValue (const Lit& p) const +{ + return model[p.var()] ^ p.sign(); +} +inline int Solver::nAssigns () const +{ + return trail.size(); +} +inline int Solver::nClauses () const +{ + return clauses.size() + xorclauses.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 lbool Solver::solve () +{ + vec tmp; + return solve(tmp); +} +inline bool Solver::okay () const +{ + return ok; +} +inline void Solver::setSeed (const uint32_t seed) +{ + mtrand.seed(seed); // Set seed of the variable-selection and clause-permutation(if applicable) +} +inline void Solver::needStats() +{ + dynamic_behaviour_analysis = true; // Sets the solver and the logger up to generate statistics + logger.statistics_on = true; +} +inline void Solver::needProofGraph() +{ + dynamic_behaviour_analysis = true; // Sets the solver and the logger up to generate proof graphs during solving + logger.proof_graph_on = true; +} +inline void Solver::setVariableName(int var, const char* name) +{ + while (var >= nVars()) newVar(); + logger.set_variable_name(var, name); +} // Sets the varible 'var'-s name to 'name' in the logger +inline void Solver::startClauseAdding() +{ + if (dynamic_behaviour_analysis) logger.begin(); // Needs to be called before adding any clause +} +inline void Solver::endFirstSimplify() +{ + if (dynamic_behaviour_analysis) logger.end(Logger::done_adding_clauses); // Needs to be called before adding any clause +} +inline void Solver::needRealUnknowns() +{ + useRealUnknowns = true; +} + + +//================================================================================================= +// Debug + etc: + +static inline void logLit(FILE* f, Lit l) +{ + fprintf(f, "%sx%d", l.sign() ? "~" : "", l.var()+1); +} + +static inline void logLits(FILE* f, const vec& ls) +{ + fprintf(f, "[ "); + if (ls.size() > 0) { + logLit(f, ls[0]); + for (int i = 1; i < ls.size(); i++) { + fprintf(f, ", "); + logLit(f, ls[i]); + } + } + fprintf(f, "] "); +} + +static inline const char* showBool(bool b) +{ + return b ? "true" : "false"; +} + + +// Just like 'assert()' but expression will be evaluated in the release version as well. +static inline void check(bool expr) +{ + assert(expr); +} + +}; + +//================================================================================================= +#endif diff --git a/src/sat/cryptominisat/SolverTypes.h b/src/sat/cryptominisat/SolverTypes.h new file mode 100644 index 0000000..7031e8c --- /dev/null +++ b/src/sat/cryptominisat/SolverTypes.h @@ -0,0 +1,166 @@ +/***********************************************************************************[SolverTypes.h] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +Permission is hereby granted, free of charge, to any person obtaining a copy of this software and +associated documentation files (the "Software"), to deal in the Software without restriction, +including without limitation the rights to use, copy, modify, merge, publish, distribute, +sublicense, and/or sell copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all copies or +substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR IMPLIED, INCLUDING BUT +NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND +NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, +DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT +OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. +**************************************************************************************************/ +#ifndef SolverTypes_h +#define SolverTypes_h + +#include +#include +#include "mtl/Alg.h" + + +namespace MINISAT +{ +//================================================================================================= +// 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 uint32_t Var; +#define var_Undef (0xffffffffU >>1) + +class Lit +{ + uint32_t x; + explicit Lit(uint32_t i) : x(i) { }; +public: + Lit() : x(2*var_Undef) {} // (lit_Undef) + explicit Lit(Var var, bool sign) : x((var+var) + (int)sign) { } + + const uint32_t& toInt() const { // Guarantees small, positive integers suitable for array indexing. + return x; + } + Lit operator~() const { + return Lit(x ^ 1); + } + Lit operator^(const bool b) const { + return Lit(x ^ b); + } + Lit& operator^=(const bool b) { + x ^= b; + return *this; + } + bool sign() const { + return x & 1; + } + Var var() const { + return x >> 1; + } + Lit unsign() const { + return Lit(x & ~1); + } + bool operator==(const Lit& p) const { + return x == p.x; + } + bool operator!= (const Lit& p) const { + return x != p.x; + } + bool operator < (const Lit& p) const { + return x < p.x; // '<' guarantees that p, ~p are adjacent in the ordering. + } +}; + +const Lit lit_Undef(var_Undef, false); // }- Useful special constants. +const Lit lit_Error(var_Undef, true ); // } + +//================================================================================================= +// Lifted booleans: + +class llbool; + +class lbool +{ + char value; + explicit lbool(char v) : value(v) { } + +public: + lbool() : value(0) { }; + inline char getchar() const { + return value; + } + inline lbool(llbool b); + + inline const bool isUndef() const { + return !value; + } + inline const bool isDef() const { + return value; + } + inline const bool getBool() const { + return (value+1) >> 1; + } + inline const bool operator==(lbool b) const { + return value == b.value; + } + inline const bool operator!=(lbool b) const { + return value != b.value; + } + lbool operator^(const bool b) const { + return lbool(value - value*2*b); + } + //lbool operator ^ (const bool b) const { return b ? lbool(-value) : lbool(value); } + + friend lbool toLbool(const char v); + friend lbool boolToLBool(const bool b); + friend class llbool; +}; +inline lbool toLbool(const char v) +{ + return lbool(v); +} +inline lbool boolToLBool(const bool b) +{ + return lbool(2*b-1); +} + +const lbool l_True = toLbool( 1); +const lbool l_False = toLbool(-1); +const lbool l_Undef = toLbool( 0); + + +class llbool +{ + char value; + +public: + llbool(): value(0) {}; + llbool(lbool v) : + value(v.value) {}; + llbool(char a) : + value(a) {} + + inline const bool operator!=(const llbool& v) const { + return (v.value != value); + } + + inline const bool operator==(const llbool& v) const { + return (v.value == value); + } + + friend class lbool; +}; +const llbool l_Nothing = toLbool(2); +const llbool l_Continue = toLbool(3); + +lbool::lbool(llbool b) : value(b.value) {}; +}; + +#endif diff --git a/src/sat/cryptominisat/clause.cpp b/src/sat/cryptominisat/clause.cpp new file mode 100644 index 0000000..23a699e --- /dev/null +++ b/src/sat/cryptominisat/clause.cpp @@ -0,0 +1,47 @@ +/***********************************************************************************[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. +**************************************************************************************************/ + +#include "clause.h" + +namespace MINISAT +{ + +Clause* Clause_new(const vec& ps, const uint group, const bool learnt) +{ + void* mem = malloc(sizeof(Clause) + sizeof(Lit)*(ps.size())); + Clause* real= new (mem) Clause(ps, group, learnt); + return real; +} + +Clause* Clause_new(const vector& ps, const uint group, const bool learnt) +{ + void* mem = malloc(sizeof(Clause) + sizeof(Lit)*(ps.size())); + Clause* real= new (mem) Clause(ps, group, learnt); + return real; +} + +#ifdef USE_GAUSS +Clause* Clause_new(const mpz_class& ps, const vec& assigns, const vector& col_to_var_original, const uint group, const bool learnt) +{ + void* mem = malloc(sizeof(Clause) + sizeof(Lit)*(ps.size())); + Clause* real= new (mem) Clause(ps, assigns, col_to_var_original, group, learnt); + return real; +} +#endif +} diff --git a/src/sat/cryptominisat/clause.h b/src/sat/cryptominisat/clause.h new file mode 100644 index 0000000..c7abb7b --- /dev/null +++ b/src/sat/cryptominisat/clause.h @@ -0,0 +1,160 @@ +/***********************************************************************************[SolverTypes.h] +MiniSat -- Copyright (c) 2003-2006, Niklas Een, Niklas Sorensson +CryptoMiniSat -- Copyright (c) 2009 Mate Soos + +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 __clause_h__ +#define __clause_h__ + +#include +#include +#include +#include +#include "mtl/Vec.h" +#include "SolverTypes.h" + +namespace MINISAT +{ + +#ifndef uint +#define uint unsigned int +#endif + +using std::vector; + + +//================================================================================================= +// Clause -- a simple class for representing a clause: + + +class Clause +{ +public: + const uint group; +protected: + uint32_t size_etc; + float act; + Lit data[0]; + +public: + Clause(const vec& ps, const uint _group, const bool learnt) : + group(_group) { + size_etc = (ps.size() << 4) | (uint32_t)learnt ; + for (int i = 0; i < ps.size(); i++) data[i] = ps[i]; + if (learnt) act = 0; + } + + Clause(const vector& ps, const uint _group, const bool learnt) : + group(_group) { + size_etc = (ps.size() << 4) | (uint32_t)learnt ; + for (uint i = 0; i < ps.size(); i++) data[i] = ps[i]; + if (learnt) act = 0; + } + + // -- use this function instead: + friend Clause* Clause_new(const vec& ps, const uint group, const bool learnt = false); + friend Clause* Clause_new(const vector& ps, const uint group, const bool learnt = false); + + uint size () const { + return size_etc >> 4; + } + void shrink (uint i) { + assert(i <= size()); + size_etc = (((size_etc >> 4) - i) << 4) | (size_etc & 15); + } + 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); + } + + Lit& operator [] (uint32_t i) { + return data[i]; + } + const Lit& operator [] (uint32_t i) const { + return data[i]; + } + + float& activity () { + return act; + } + + Lit* getData () { + return data; + } + void print() { + Clause& c = *this; + printf("group: %d, size: %d, learnt:%d, lits:\"", c.group, c.size(), c.learnt()); + for (uint i = 0; i < c.size(); i++) { + if (c[i].sign()) printf("-"); + printf("%d ", c[i].var()); + } + printf("\"\n"); + } +}; + +class XorClause : public Clause +{ +public: + // NOTE: This constructor cannot be used directly (doesn't allocate enough memory). + template + XorClause(const V& ps, const bool _xor_clause_inverted, const uint _group, const bool learnt) : + Clause(ps, _group, learnt) { + size_etc |= (((uint32_t)_xor_clause_inverted) << 3); + } + + // -- use this function instead: + template + friend XorClause* XorClause_new(const V& ps, const bool xor_clause_inverted, const uint group, const bool learnt = false) { + void* mem = malloc(sizeof(XorClause) + sizeof(Lit)*(ps.size())); + XorClause* real= new (mem) XorClause(ps, xor_clause_inverted, group, learnt); + return real; + } + + inline bool xor_clause_inverted() const { + return size_etc & 8; + } + inline void invert (bool b) { + size_etc ^= (uint32_t)b << 3; + } + + void print() { + Clause& c = *this; + printf("group: %d, size: %d, learnt:%d, lits:\"", c.group, c.size(), c.learnt()); + for (uint i = 0; i < c.size();) { + assert(!c[i].sign()); + printf("%d", c[i].var()); + i++; + if (i < c.size()) printf(" + "); + } + printf("\"\n"); + } +}; + +Clause* Clause_new(const vec& ps, const uint group, const bool learnt); +Clause* Clause_new(const vector& ps, const uint group, const bool learnt); +}; + +#endif diff --git a/src/sat/cryptominisat/fcopy.cpp b/src/sat/cryptominisat/fcopy.cpp new file mode 100644 index 0000000..79fd312 --- /dev/null +++ b/src/sat/cryptominisat/fcopy.cpp @@ -0,0 +1,51 @@ + +#include +#include +#include "fcopy.h" + + +namespace MINISAT +{ +#define BUFSZ 16000 + +int FileCopy ( const char *src, const char *dst ) +{ + char *buf; + FILE *fi; + FILE *fo; + unsigned amount; + unsigned written; + int result; + + buf = new char[BUFSZ]; + + fi = fopen( src, "rb" ); + fo = fopen( dst, "wb" ); + + result = COPY_OK; + if ((fi == NULL) || (fo == NULL) ) { + result = COPY_ERROR; + if (fi != NULL) fclose(fi); + if (fo != NULL) fclose(fo); + } + + if (result == COPY_OK) { + do { + amount = fread( buf, sizeof(char), BUFSZ, fi ); + if (amount) { + written = fwrite( buf, sizeof(char), amount, fo ); + if (written != amount) + result = COPY_ERROR; // out of disk space or some other disk err? + } + } // when amount read is < BUFSZ, copy + while ((result == COPY_OK) && (amount == BUFSZ)); + fclose(fi); + fclose(fo); + } + + delete[] buf; + + return(result); +} + +}; diff --git a/src/sat/cryptominisat/fcopy.h b/src/sat/cryptominisat/fcopy.h new file mode 100644 index 0000000..a1958eb --- /dev/null +++ b/src/sat/cryptominisat/fcopy.h @@ -0,0 +1,14 @@ +#ifndef __FCOPY_H__ +#define __FCOPY_H__ + +namespace MINISAT +{ + +#define COPY_ERROR -1 +#define COPY_OK 0 + +int FileCopy( const char *src, const char *dst ); + +}; + +#endif diff --git a/src/sat/sat.h b/src/sat/sat.h index f9a6bfe..12b8033 100644 --- a/src/sat/sat.h +++ b/src/sat/sat.h @@ -2,8 +2,8 @@ #define SAT_H_ #ifdef CRYPTOMINISAT -#include "cryptominisat/Solver/Solver.h" -#include "cryptominisat/Solver/SolverTypes.h" +#include "cryptominisat/Solver.h" +#include "cryptominisat/SolverTypes.h" #else #include "core/Solver.h" #include "core/SolverTypes.h"