https://github.com/ASchidler/coloring
Tip revision: dd03517187447fd44cfd9f03db6ab7313a21a64a authored by Andre Schidler on 14 March 2022, 12:24:58 UTC
Initial commit
Initial commit
Tip revision: dd03517
sat_encode.h
//
// Createdhidler on 10/15/21.
//
#ifndef CPP_SAT_ENCODE_H
#define CPP_SAT_ENCODE_H
#include "conflict_graph.h"
#include "glucose30/core/Solver.h"
#include "glucose30/core/SolverTypes.h"
#include <boost/thread/thread.hpp>
#include <memory>
#include <queue>
#include "heuristics.h"
using namespace std;
namespace planarity {
class SatEncode {
private:
friend class Clique;
/**
* Encodes the graph part.
*/
inline static void encode_graph(Glucose30::Solver &solver, const ConflictGraph &g,
vector<vector<Glucose30::Var>> &variables, const unordered_map<node_t, dynamic_bitset<>>& exceptions, const unsigned int ub, bool encode_edges=true) {
for (int n = 0; n < g.getNumNodes(); n++) {
bool has_nbs = g.adjacency[n].any();
auto it = exceptions.find(n);
for (int k = 0; k < ub; k++) {
if ((has_nbs || k == 0) && (it == exceptions.end() || !it->second.test(k)))
variables[n][k] = solver.newVar();
else
variables[n][k] = var_Undef;
}
}
Glucose30::vec<Glucose30::Lit> clause;
clause.growTo(static_cast<int>(ub));
// Each node needs a color
for (int n = 0; n < g.getNumNodes(); n++) {
clause.clear();
for (int k = 0; k < ub; k++) {
if (variables[n][k] != var_Undef) {
clause.push(Glucose30::mkLit(variables[n][k]));
// for (int k2 = k + 1; k2 < ub; k2++) {
// if (variables[n][k2] != var_Undef) {
// solver.addClause(Glucose30::mkLit(variables[n][k], true),
// Glucose30::mkLit(variables[n][k2], true));
// }
// }
}
}
assert(clause.size() > 0);
solver.addClause(clause);
}
if (!solver.okay())
cout << "Before" << endl;
if (encode_edges) {
node_t edge_cnt = 0;
// Edges must be colored differently
for (int n = 0; n < g.getNumNodes(); n++) {
for (auto n2 = g.adjacency[n].find_next(n); n2 != dynamic_bitset<>::npos; n2 = g.adjacency[n].find_next(n2)) {
for (int k = 0; k < ub; k++) {
if (variables[n][k] != var_Undef && variables[n2][k] != var_Undef) {
solver.addClause(Glucose30::mkLit(variables[n][k], true),
Glucose30::mkLit(variables[n2][k], true));
edge_cnt++;
}
}
}
}
cout << "Encoded " << edge_cnt << " edges." << endl;
}
}
/**
* Extracts the coloring from a SAT solver model.
*/
inline static void extract_color(const Glucose30::Solver &solver, vector<color_t> &coloring,
const vector<vector<Glucose30::Var>> &variables) {
coloring.clear();
for (const auto &variable: variables) {
bool found = false;
for (auto k = 0; k < variable.size(); k++) {
if (variable[k] != var_Undef && solver.model[variable[k]] == g3l_True) {
found = true;
coloring.push_back(k);
break;
}
}
assert(found);
}
}
static void AmoCommander(Glucose30::Solver& slv, const vector<Glucose30::Var>& variables, const unsigned int m) {
if (variables.size() <= m) {
for(auto i=0; i < variables.size(); i++) {
for(auto j=i+1; j < variables.size(); j++) {
slv.addClause(Glucose30::mkLit(variables[i], true), Glucose30::mkLit(variables[j], true));
}
}
} else {
vector<Glucose30::Var> new_variables;
new_variables.reserve(variables.size()/m + 1);
for(auto cc=0; cc < m; cc++) {
auto nv = slv.newVar();
new_variables.push_back(nv);
for(auto i=cc * m; i < variables.size() && i < (cc+1)*m; i++) {
slv.addClause(Glucose30::mkLit(nv), Glucose30::mkLit(variables[i], true));
}
for(auto i=cc * m; i < variables.size() && i < (cc+1)*m; i++) {
for(auto j=i+1; j < variables.size() && j < (cc+1)*m; j++) {
slv.addClause(Glucose30::mkLit(variables[j], true), Glucose30::mkLit(variables[i], true));
}
}
}
AmoCommander(slv, new_variables, m);
}
}
static std::shared_ptr<vector<Glucose30::Lit>>
createTotalizer(Glucose30::Solver &slv, const vector<Glucose30::Lit> &literals, const unsigned int ub) {
queue<std::unique_ptr<vector<Glucose30::Lit>>> currentVars;
for (const auto &clit: literals) {
currentVars.push(std::move(std::make_unique<vector<Glucose30::Lit>>()));
currentVars.back()->push_back(clit);
}
while (currentVars.size() > 1) {
auto l = std::move(currentVars.front());
currentVars.pop();
auto r = std::move(currentVars.front());
currentVars.pop();
auto minub = min(ub + 1, static_cast<unsigned int>(l->size() + r->size()));
auto newVars = make_unique<vector<Glucose30::Lit>>();
newVars->reserve(minub);
for (unsigned int i = 0; i < minub; i++) {
newVars->push_back(Glucose30::mkLit(slv.newVar()));
}
auto minub2 = min(minub, static_cast<unsigned int>(r->size()));
for (unsigned int j = 0; j < minub2; ++j) {
slv.addClause(Glucose30::mkLit(r->at(j).x / 2, true), newVars->at(j));
}
minub2 = min(minub, static_cast<unsigned int>(l->size()));
for (int i = 0; i < minub2; ++i) {
slv.addClause(Glucose30::mkLit(l->at(i).x / 2, true), newVars->at(i));
}
for (int i = 1; i <= minub2; ++i) {
auto minj = min(minub - i, static_cast<unsigned int>(r->size()));
for (int j = 1; j <= minj; ++j) {
slv.addClause(
Glucose30::mkLit(l->at(i - 1).x / 2, true),
Glucose30::mkLit(r->at(j - 1).x / 2, true),
newVars->at(i + j - 1)
);
}
}
currentVars.push(std::move(newVars));
}
return {std::move(currentVars.front())};
}
public:
/**
* Tries to find a graph coloring of decreasing size for the given graph, using a SAT solver.
* @param g The graph to color.
* @param clique A clique in the graph for symmetry breaking, can be empty.
* @param ub A starting bound on how many colors are required.
* @param timeout Optional: a timeout for the SAT solver call. Even if the coloring is not (certified) optimal, the SAT call will be terminated after the timeout, 0 means no timeout.
* @return A graph coloring for the graph. The coloring is empty, if no coloring could be found (invalid upper bound, or timeout exceeded without result).
*/
static Coloring
encode_full(const ConflictGraph &g, const vector<node_t> &clique, color_t ub, unsigned int timeout = 0, const string &filename = "", bool optimize=true, bool timeout_for_first=true) {
vector<vector<Glucose30::Var>> variables(g.getNumNodes(), vector<Glucose30::Var>(ub));
vector<color_t> coloring;
unordered_map<node_t, dynamic_bitset<>> exceptions;
exceptions.reserve(g.getNumNodes());
coloring.reserve(g.getNumNodes());
for (int i = 0; i < clique.size(); i++) {
auto n = clique[i];
auto it = exceptions.find(n);
if (it == exceptions.end())
it = get<0>(exceptions.emplace(n, ub));
for(color_t k=0; k < ub; k++) {
if (k != i)
it->second.set(k);
}
for (auto n2=g.adjacency[n].find_first(); n2 != dynamic_bitset<>::npos; n2 = g.adjacency[n].find_next(n2)) {
auto it2 = exceptions.find(n2);
if (it2 == exceptions.end())
it2 = get<0>(exceptions.emplace(n2, ub));
it2->second.set(i);
}
}
auto slv = Glucose30::Solver();
//slv.setIncrementalMode();
encode_graph(slv, g, variables, exceptions, ub);
cout << "Finished encoding" << endl;
bool solved = true;
unsigned int counter = 0;
while (solved) {
if (timeout > 0 && (counter > 0 || timeout_for_first)) {
// TODO: Fix many threads, use boost threads with interrupt?
auto th = boost::thread([&]() {
boost::this_thread::sleep(boost::posix_time::seconds(timeout));
slv.interrupt();
});
slv.clearInterrupt();
solved = slv.solve();
th.interrupt();
} else {
slv.verbosity = 0;
solved = slv.solve();
slv.printIncrementalStats();
}
counter++;
if (solved) {
extract_color(slv, coloring, variables);
assert(g.verify(coloring));
if (!filename.empty()) {
Coloring::store(filename, g, coloring);
}
cout << "Found " << ub << " colors" << endl;
ub--;
if (! optimize)
break;
// Remove option for color k
for (int n = 0; n < g.getNumNodes(); n++) {
if (variables[n][ub] != var_Undef)
slv.addClause(Glucose30::mkLit(variables[n][ub], true));
}
} else if (timeout == 0) {
cout << "Result is optimal" << endl;
}
}
cout << "Finished solving" << endl;
return {coloring, ++ub, vector<tuple<int, node_t>>()};
}
/**
* Tries to find a coloring of decreasing size for the graph using a SAT solver. This method assumes that
* some colorings outside the graph already exist.
* @param g The graph to color.
* @param exceptions The colors that are not allowed for some nodes, i.e. existing colors outside g or tabu search.
* @param num_colors The number of colors currently used, will be used as an upper bound.
* @param timeout The timeout used for each SAT call. 0 means no timeout.
* @param timeout_for_first Flag that states if the timeout is used for the first call. Set to true if a result is required.
* @param limit_cnt Flag that states if the number of colors is minimized.
* @param limit_color If set to > -1 will try to minimize color assignments to this color.
* @param limit_color_ub The upper bound for color assignments to the limit_color.
* @return A graph coloring for the graph. The coloring is empty, if no coloring could be found (invalid upper bound, or timeout exceeded without result).
*/
static pair<Coloring, bool>
encode_partial(const SubGraph& g, color_t num_colors,
const unsigned int timeout = 0,
const bool timeout_for_first = true, const bool limit_cnt = true, const color_t limit_color = INVALID_COLOR,
color_t limit_color_ub = 0, const bool optimize=true, color_t suggested_color = INVALID_COLOR, const dynamic_bitset<>& suggested_nodes=dynamic_bitset<>()) {
vector<vector<Glucose30::Var>> variables(g.sub_g.getNumNodes(), vector<Glucose30::Var>(num_colors));
vector<color_t> coloring;
coloring.reserve(g.sub_g.getNumNodes());
std::shared_ptr<vector<Glucose30::Lit>> cardVarsSingleColor = nullptr;
std::shared_ptr<vector<Glucose30::Lit>> cardVarsColors = nullptr;
auto slv = Glucose30::Solver();
slv.setIncrementalMode();
unordered_map<node_t, dynamic_bitset<>> exceptions;
exceptions.reserve(g.exceptions.size());
// Encode Exceptions
for (const auto &cEx: g.exceptions) {
exceptions.emplace(cEx.node, cEx.colors);
}
encode_graph(slv, g.sub_g, variables, exceptions, num_colors, true);
Glucose30::vec<Glucose30::Lit> assps;
if (suggested_color != INVALID_COLOR) {
for(auto cn = suggested_nodes.find_first(); cn != dynamic_bitset<>::npos; cn = suggested_nodes.find_next(cn)) {
assps.push(Glucose30::mkLit(variables[cn][suggested_color]));
}
}
// int options = 0;
// for(node_t cn=0; cn < g.sub_g.getNumNodes(); cn++) {
// for(color_t k=0; k < num_colors; k++) {
// if (variables[cn][k] != var_Undef)
// options++;
// }
// }
// cout << "Options " << options << endl;
if (limit_cnt) {
vector<Glucose30::Lit> literals;
literals.reserve(num_colors);
for (int k = 0; k < num_colors; k++) {
auto c_var = slv.newVar();
literals.push_back(Glucose30::mkLit(c_var));
for (int n = 0; n < g.sub_g.getNumNodes(); n++) {
slv.addClause(Glucose30::mkLit(variables[n][k], true), Glucose30::mkLit(c_var));
}
}
cardVarsColors = createTotalizer(slv, literals, literals.size());
}
if (limit_color != INVALID_COLOR) {
vector<Glucose30::Lit> literals;
literals.reserve(g.sub_g.getNumNodes());
for (int n = 0; n < g.sub_g.getNumNodes(); n++) {
if (variables[n][limit_color] != var_Undef) {
literals.push_back(Glucose30::mkLit(variables[n][limit_color]));
}
}
limit_color_ub = limit_color_ub < literals.size() ? limit_color_ub : literals.size() - 1;
if (limit_color_ub > 0) {
cardVarsSingleColor = createTotalizer(slv, literals, limit_color_ub + 1);
slv.addClause(Glucose30::mkLit(cardVarsSingleColor->at(limit_color_ub).x / 2, true));
} else
cardVarsSingleColor = createTotalizer(slv, literals, literals.size());
}
//cout << "Finished encoding" << endl;
bool solved = true;
unsigned int counter = 0;
bool is_unsat = true;
while (solved) {
if (timeout > 0 and (counter > 0 or timeout_for_first)) {
auto th = boost::thread([&]() {
boost::this_thread::sleep(boost::posix_time::seconds(timeout));
slv.interrupt();
is_unsat = false;
});
slv.clearInterrupt();
if (counter == 0 && suggested_color != INVALID_COLOR)
solved = slv.solve(assps);
else
solved = slv.solve();
th.interrupt();
} else {
if (counter == 0 && suggested_color != INVALID_COLOR)
solved = slv.solve(assps);
else
solved = slv.solve();
}
counter++;
if (solved) {
is_unsat = false;
extract_color(slv, coloring, variables);
//
// cout << "Found " << num_colors << " colors, " << limit_color_ub << " for color " << limit_color
// << endl;
if (! optimize)
break;
if (limit_cnt) {
num_colors--;
slv.addClause(Glucose30::mkLit(cardVarsColors->at(num_colors).x / 2, true));
}
// if (! limit_cnt && limit_color_ub == 0) {
// num_colors--;
//
// // Remove option for color k
// for (int n = 0; n < g.sub_g.getNumNodes(); n++) {
// if (variables[n][num_colors] != var_Undef)
// slv.addClause(Glucose30::mkLit(variables[n][num_colors], true));
// }
// }
if (limit_color != INVALID_COLOR && limit_color_ub > 0) {
limit_color_ub--;
slv.addClause(Glucose30::mkLit(cardVarsSingleColor->at(limit_color_ub).x / 2, true));
} else if (limit_color != INVALID_COLOR && limit_color_ub == 0) {
break;
}
}
}
//cout << "Finished solving" << endl;
return pair<Coloring, bool>(Coloring(coloring, num_colors, vector<tuple<int, node_t>>()), is_unsat);
}
//
// static void ind_set_heuristic(const ConflictGraph &g, const vector<node_t>& clique, const string &filename = "", const int timeout = 60) {
// vector<Glucose30::Var> variables;
// variables.reserve(g.getNumNodes());
// dynamic_bitset<> done(g.getNumNodes());
// vector<Glucose30::Lit> literals;
// literals.reserve(g.getNumNodes());
// color_t colors = 0;
// vector<color_t> coloring(g.getNumNodes());
//
// while (done.count() < g.getNumNodes()) {
// colors += 1;
// Glucose30::Solver solver;
// solver.setIncrementalMode();
// variables.clear();
// literals.clear();
//
// for (auto i = 0; i < g.getNumNodes(); i++) {
// if (!done[i]) {
// variables.push_back(solver.newVar());
// literals.push_back(Glucose30::mkLit(variables.back()));
// } else {
// variables.push_back(0);
// }
// }
//
// for (auto n = 0; n < g.getNumNodes(); n++) {
// if (! done[n]) {
// auto cNb = g.adjacency[n] - done;
// for (auto n2 = cNb.find_first(); n2 != dynamic_bitset<>::npos and n2 < n; n2 = cNb.find_next(n2)) {
// solver.addClause(Glucose30::mkLit(variables[n]), Glucose30::mkLit(variables[n2]));
// }
// }
// }
//
// if (colors <= clique.size())
// solver.addClause(Glucose30::mkLit(variables[clique[colors-1]], true));
//
// auto rhs = SatEncode::createTotalizer(solver, literals, literals.size());
//
// cout << "Encoded Independent set" << endl;
//
// bool solved = true;
// dynamic_bitset<> current_is(g.getNumNodes());
// while (solved) {
// if (timeout > 0) {
// bool running = true;
// auto th = boost::thread([&]() {
// boost::this_thread::sleep(boost::posix_time::seconds(timeout));
// solver.interrupt();
// });
// solver.clearInterrupt();
// solved = solver.solve();
// th.interrupt();
// } else {
// solved = solver.solve();
// }
//
// if (solved) {
// unsigned int issize = 0;
// current_is.reset();
// for (int i = 0; i < variables.size(); i++) {
// if (! done[i] && solver.model[variables[i]] == g3l_False) {
// current_is[i] = true;
// issize++;
// }
// }
//
// cout << "Found independent set of size " << issize << endl;
// if (issize < literals.size()) {
// solver.addClause(Glucose30::mkLit(rhs->at(literals.size() - 1 - issize).x / 2, true));
// } else {
// solved = false;
// }
// }
// }
// done |= current_is;
// for (auto n = current_is.find_first(); n != dynamic_bitset<>::npos; n = current_is.find_next(n)) {
// coloring[n] = colors - 1;
// }
// }
// cout << colors << " Required" << endl;
//
// Coloring result(coloring, colors, vector<tuple<int, node_t>>());
// tabuSearch(g, result, result.numColors);
// }
};
}
#endif //CPP_SAT_ENCODE_H