QA_SAT/qubo_lab
2
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

sync

Browse Source
This commit is contained in:
Tom
2019-04-02 13:16:26 +02:00
parent 05451ccbcd
commit d5982763f8
41 changed files with 2850 additions and 124 deletions
Download Patch File Download Diff File Expand all files Collapse all files

27
src/SConscript
View File

@@ -4,16 +4,24 @@ Import('globalEnv')
env = globalEnv.Clone()
files = Glob(os.path.join(".","*.cpp"))
files.append(Glob(os.path.join("util", "*.cpp")))
utilFiles = Glob(os.path.join("util","*.cpp"))
## runMinisat ##
targetName = 'runMinisat'
libs = ["mongocxx", "bsoncxx", "inihcpp", "minisat"]
libs = ["mongocxx", "bsoncxx", "inihcpp", "minisat", "qbsolv"]
env.Append(CPPPATH=os.path.join(env["ROOTPATH"], "src"))
env.Program(target=targetName, source=files, LIBS=libs)
env.Program(target=targetName,
source=[utilFiles, "runMinisat.cpp"],
LIBS=libs)
## runMinisat ##
env.Program(target="runQbsolv",
source=[utilFiles, "runQbsolv.cpp"],
LIBS=libs)
## create start script
#
@@ -27,6 +35,17 @@ with open(startScriptName, "w") as startScript:
.format(os.path.join(env["MONGOCXX_LIB_PATH"], "lib")))
startScript.write("{}\n".format(os.path.join(env["BUILDPATH"], targetName)))
startScriptName = "{}.sh".format("runQbsolv")
with open(startScriptName, "w") as startScript:
startScript.write("#!/bin/bash\n")
startScript.write("export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:{}\n"
.format(os.path.join(env["MONGOCXX_LIB_PATH"], "lib")))
startScript.write("{}\n".format(os.path.join(env["BUILDPATH"], "runQbsolv")))
#env.Install(env["BUILDPATH"], [startScriptName])

5
src/runMinisat.cpp
View File

@@ -36,15 +36,14 @@ int main(int argc, char** argv)
mongocxx::collection instances = db["instances"];
bsoncxx::builder::stream::document result;
for(auto sat : satlab::MongoDBExperimentScope(db, getScopeName()))
{
satlab::MinisatSolver solver(sat);
solver.solve();
auto result = satlab::convert<bsoncxx::builder::stream::document>(
solver.getResult()
);
satlab::convert<>(result, solver.getResult());
db["minisat_runs"].insert_one(result.view());
}

161
src/runQbsolv.cpp Normal file
View File

@@ -0,0 +1,161 @@
#include <iostream>
#include "solver_cxx.h"
#include "util/conversions.h"
#include "mongocxx/instance.hpp"
#include "mongocxx/client.hpp"
#include "mongocxx/database.hpp"
#include "mongocxx/collection.hpp"
#include "mongocxx/cursor.hpp"
#include "INIReader.h"
#include "util/wmis_qubo.h"
std::string getDbConfigFilePath();
std::string getScopeName();
std::string getDBUrl();
mongocxx::client connectToDatabase();
void print(const qbscxx::SOLUTION& solution, const satlab::wmis_qubo& qubo);
int main(int argc, char** argv)
{
mongocxx::instance inst{};
mongocxx::client conn = connectToDatabase();
mongocxx::database db = conn["experiments"];
mongocxx::collection wmis_qubos = db["wmis_qubos"];
std::cout << "runQbsolv" << std::endl;
satlab::wmis_qubo wmis_qubo;
for(auto& el : wmis_qubos.find({}))
{
satlab::types::convert(wmis_qubo, el);
qbscxx::Solver solver(wmis_qubo.get_qubo());
solver.set_goal(qbscxx::Solver::GOAL::MAXIMUM);
solver.set_verbosity(-1);
solver.solve();
print(solver.get_solution(), wmis_qubo);
std::cout << std::endl;
}
return 0;
}
mongocxx::client connectToDatabase()
{
mongocxx::options::ssl sslOptions;
sslOptions.allow_invalid_certificates(true);
mongocxx::options::client clientOptions{};
clientOptions.ssl_opts(sslOptions);
return mongocxx::client{mongocxx::uri{getDBUrl()}, clientOptions};
}
std::string getDBUrl()
{
INIReader iniReader(getDbConfigFilePath());
std::string connUrl("mongodb://");
connUrl.append(iniReader.Get("CONNECTION", "user", "NA") + ":");
connUrl.append(iniReader.Get("CONNECTION", "pw", "NA") + "@");
connUrl.append(iniReader.Get("CONNECTION", "url", "NA") + ":");
connUrl.append(iniReader.Get("CONNECTION", "port", "NA") + "/");
connUrl.append(iniReader.Get("CONNECTION", "database", "NA"));
connUrl.append("?ssl=true");
return connUrl;
}
std::string getDbConfigFilePath()
{
std::cout << "Database config file: ";
std::string path;
std::cin >> path;
return path;
}
std::string getScopeName()
{
std::cout << "Experiment scope: ";
std::string scope;
std::cin >> scope;
return scope;
}
void print(const qbscxx::SOLUTION& solution, const satlab::wmis_qubo& qubo)
{
qbscxx::ENERGY_T resulution_energy = 0;
for(int val : solution)
{
resulution_energy += val;
std::cout << val;
}
std::cout << " " << resulution_energy << std::endl;
std::vector<bool> model;
int conflicts = 0;
for(int i = 0; i < solution.size(); i++)
{
auto node = qubo.node_at(i);
int lit = std::get<1>(node);
size_t var = std::abs(lit);
bool newVar = false;
if(model.size() < var)
{
newVar = true;
model.resize(var);
}
bool binding;
if(solution[i] == 0)
{
binding = lit < 0 ? true : false;
}
else
{
binding = lit < 0 ? false : true;
}
if(!newVar && binding != model[var - 1])
{
conflicts++;
}
model[var - 1] = binding;
}
for(int i=0; i < model.size(); i++)
{
int var = i + 1;
std::cout << (model[i] ? var : -1 * var) << " ";
}
std::cout << std::endl;
}

6
src/util/bson2ksatClauseConverter.h
View File

@@ -16,16 +16,14 @@ namespace types
{
template<typename = KSATinstance::CLAUSE, typename = bsoncxx::array::element>
KSATinstance::CLAUSE convert(const bsoncxx::array::element& docView)
void convert(KSATinstance::CLAUSE& clause, const bsoncxx::array::element& docView)
{
KSATinstance::CLAUSE clause;
clause = KSATinstance::CLAUSE();
for(auto lit : static_cast<bsoncxx::array::view>(docView.get_array()))
{
clause.push_back(lit.get_int32());
}
return clause;
}
}

13
src/util/bson2ksatConverter.h
View File

@@ -16,23 +16,24 @@ namespace types
{
template<typename = KSATinstance, typename = bsoncxx::document::view>
KSATinstance convert(const bsoncxx::document::view& docView)
void convert(KSATinstance& ksat, const bsoncxx::document::view& docView)
{
using CLAUSE = KSATinstance::CLAUSE;
using CLAUSE_DOC = const bsoncxx::array::element&;
KSATinstance ksat;
ksat = KSATinstance();
bsoncxx::array::view clauses = docView["clauses"].get_array();
for(auto clause : clauses)
KSATinstance::CLAUSE clause;
for(auto clauseDoc : clauses)
{
ksat.addClause(convert<CLAUSE, CLAUSE_DOC>(clause));
convert<>(clause, clauseDoc);
ksat.addClause(clause);
}
ksat.setId(docView["_id"].get_oid().value.to_string());
return ksat;
}
}

85
src/util/bson2quboMtrx.h Normal file
View File

@@ -0,0 +1,85 @@
#ifndef BSON2QBUO_MTRX_H
#define BSON2QBUO_MTRX_H
#include "bsoncxx/document/view.hpp"
#include "bsoncxx/array/view.hpp"
#include "bsoncxx/types.hpp"
#include "util/convert.h"
#include "solver_cxx.h"
#include <iostream>
#include "bsoncxx/json.hpp"
#include <map>
#include <unordered_map>
#include <tuple>
namespace satlab
{
namespace types
{
template<typename = qbscxx::QUBO, typename = bsoncxx::document::view>
void convert(qbscxx::QUBO& qubo, const bsoncxx::document::view& docView)
{
using NODE = std::tuple<int, int>;
using NODE_INDEX_DICT = std::map<NODE, size_t>;
//qubo = qbscxx::QUBO();
NODE_INDEX_DICT nodeIndexDict;
NODE node1;
size_t nodeIndex = 0;
for(auto& entry : docView["qubo"].get_array().value)
{
for(auto& nodeView : entry[0].get_array().value)
{
node1 = NODE(nodeView[0].get_int32().value,
nodeView[1].get_int32().value);
if(nodeIndexDict.find( node1 ) == nodeIndexDict.end())
{
nodeIndexDict.emplace(node1, nodeIndex);
nodeIndex++;
}
}
}
qubo.resize(nodeIndexDict.size());
for(int i=0; i < nodeIndexDict.size(); i++)
{
qubo[i].resize(nodeIndexDict.size());
}
NODE node2;
for(auto& entry : docView["qubo"].get_array().value)
{
auto coupler = entry[0];
auto node1doc = coupler[0];
auto node2doc = coupler[1];
node1 = NODE(node1doc[0].get_int32().value,
node1doc[1].get_int32().value);
node2 = NODE(node2doc[0].get_int32().value,
node2doc[1].get_int32().value);
size_t nodeIndex1 = nodeIndexDict.at(node1);
size_t nodeIndex2 = nodeIndexDict.at(node2);
qbscxx::ENERGY_T energy = entry[1].get_double().value;
qubo[nodeIndex1][nodeIndex2] = energy;
}
nodeIndexDict.clear();
}
}
}
#endif // BSON2QBUO_MTRX_H

43
src/util/bson_2_qubo_coupler.h Normal file
View File

@@ -0,0 +1,43 @@
#ifndef BSON_2_QUBO_COUPLER_H
#define BSON_2_QUBO_COUPLER_H
#include "bsoncxx/document/view.hpp"
#include "bsoncxx/array/view.hpp"
#include "bsoncxx/types.hpp"
#include "util/convert.h"
#include <map>
#include <unordered_map>
#include <tuple>
#include "util/wmis_qubo.h"
namespace satlab
{
namespace types
{
template<typename = wmis_qubo::COUPLER, typename = bsoncxx::array::view>
void convert(wmis_qubo::COUPLER& coupler, const bsoncxx::array::view& docView)
{
auto nodes = docView[0].get_array().value;
wmis_qubo::NODE node1(nodes[0][0].get_int32().value,
nodes[0][1].get_int32().value);
wmis_qubo::NODE node2(nodes[1][0].get_int32().value,
nodes[1][1].get_int32().value);
qbscxx::ENERGY_T energy = docView[1].get_double().value;
coupler = wmis_qubo::COUPLER(node1, node2, energy);
}
}
}
#endif // BSON_2_QUBO_COUPLER_H

47
src/util/bson_2_wmis_qubo.h Normal file
View File

@@ -0,0 +1,47 @@
#ifndef BSON_2_WMIS_QUBO_H
#define BSON_2_WMIS_QUBO_H
#include "bsoncxx/document/view.hpp"
#include "bsoncxx/array/view.hpp"
#include "bsoncxx/types.hpp"
#include "util/convert.h"
#include <iostream>
#include "bsoncxx/json.hpp"
#include <map>
#include <unordered_map>
#include <tuple>
#include "util/wmis_qubo.h"
#include "util/bson_2_qubo_coupler.h"
namespace satlab
{
namespace types
{
template<typename = wmis_qubo, typename = bsoncxx::document::view>
void convert(wmis_qubo& qubo, const bsoncxx::document::view& docView)
{
qubo = wmis_qubo();
for(auto& entry : docView["qubo"].get_array().value)
{
wmis_qubo::COUPLER coupler;
convert(coupler, entry.get_array().value);
qubo.add(coupler);
}
}
}
}
#endif // BSON_2_WMIS_QUBO_H

2
src/util/conversions.h
View File

@@ -7,5 +7,7 @@
#include "util/minisatStats2bson.h"
#include "util/minisatResult2bson.h"
#include "util/ksatModel2bson.h"
#include "util/bson2quboMtrx.h"
#include "util/bson_2_wmis_qubo.h"
#endif //CONVERSIONS_H

6
src/util/convert.h
View File

@@ -7,11 +7,11 @@ namespace satlab
namespace types
{
template<typename TARGET_T, typename SOURCE_T>
TARGET_T convert(const SOURCE_T& source);
// template<typename TARGET_T, typename SOURCE_T>
// TARGET_T convert(const SOURCE_T& source);
template<typename TARGET_T, typename SOURCE_T>
void convertRef(TARGET_T&, const SOURCE_T& source);
void convert(TARGET_T&, const SOURCE_T& source);
}
}

4
src/util/ksatClause2ministaClause.h
View File

@@ -14,8 +14,8 @@ namespace types
{
template<typename = Minisat::vec<Minisat::Lit>, typename = KSATinstance::CLAUSE>
void convertRef(Minisat::vec<Minisat::Lit>& clauseVec,
const KSATinstance::CLAUSE& clause)
void convert(Minisat::vec<Minisat::Lit>& clauseVec,
const KSATinstance::CLAUSE& clause)
{
clauseVec.clear();

6
src/util/ksatModel2bson.h
View File

@@ -11,16 +11,14 @@ namespace satlab
{
template<typename = bsoncxx::builder::stream::array, typename = KSATinstance::MODEL>
bsoncxx::builder::stream::array convert(const KSATinstance::MODEL& model)
void convert(bsoncxx::builder::stream::array& builder, const KSATinstance::MODEL& model)
{
bsoncxx::builder::stream::array builder;
builder = bsoncxx::builder::stream::array();
for(auto& lit : model)
{
builder << lit;
}
return builder;
}
}

16
src/util/minisatResult2bson.h
View File

@@ -13,19 +13,23 @@ namespace satlab
{
template<typename = bsoncxx::builder::stream::document, typename = MinisatResult>
bsoncxx::builder::stream::document convert(const MinisatResult& result)
void convert(bsoncxx::builder::stream::document& builder, const MinisatResult& result)
{
using ARRAY_BUILDER = bsoncxx::builder::stream::array;
using DOCUMENT_BUILDER = bsoncxx::builder::stream::document;
DOCUMENT_BUILDER builder;
builder = DOCUMENT_BUILDER();
ARRAY_BUILDER model;
DOCUMENT_BUILDER stats;
convert<>(model, result.getModel());
convert<>(stats, result.getStats());
builder << "satisfiable" << result.getSatisfiable()
<< "model" << convert<ARRAY_BUILDER>(result.getModel()).view()
<< "stats" << convert<DOCUMENT_BUILDER>(result.getStats()).view()
<< "model" << model.view()
<< "stats" << stats.view()
<< "instance" << bsoncxx::oid(result.getInstanceId());
return builder;
}

6
src/util/minisatStats2bson.h
View File

@@ -11,9 +11,9 @@ namespace satlab
{
template<typename = bsoncxx::builder::stream::document, typename = MinisatStats>
bsoncxx::builder::stream::document convert(const MinisatStats& stats)
void convert(bsoncxx::builder::stream::document& builder, const MinisatStats& stats)
{
bsoncxx::builder::stream::document builder;
builder = bsoncxx::builder::stream::document();
builder << "solves" << static_cast<int>(stats.getSolves())
<< "starts" << static_cast<int>(stats.getStarts())
@@ -26,8 +26,6 @@ bsoncxx::builder::stream::document convert(const MinisatStats& stats)
<< "learnts_literals" << static_cast<int>(stats.getLearntsLiterals())
<< "max_literals" << static_cast<int>(stats.getMaxLiterals())
<< "tot_literals" << static_cast<int>(stats.getTotLiterals());
return builder;
}

2
src/util/minisatsolver.cpp
View File

@@ -38,7 +38,7 @@ void MinisatSolver::addClause(const KSATinstance::CLAUSE& clause)
{
Minisat::vec<Minisat::Lit> clauseVec;
types::convertRef<>(clauseVec, clause);
types::convert<>(clauseVec, clause);
addMissingVars(clauseVec);

2
src/util/mongodbexperimentscope.cpp
View File

@@ -35,7 +35,7 @@ void MongoDBExperimentScope::InstanceIncrementer::updateInstance()
return;
}
instance = KSATinstance(types::convert(*cursorIt));
types::convert(instance, *cursorIt);
instanceIsUpdated = true;
}

79
src/util/wmis_qubo.cpp Normal file
View File

@@ -0,0 +1,79 @@
#include "util/wmis_qubo.h"
#include <algorithm>
namespace satlab
{
void wmis_qubo::add(const COUPLER& coupler)
{
const NODE& node1 = std::get<0>(coupler);
const NODE& node2 = std::get<1>(coupler);
qbscxx::ENERGY_T energy = std::get<2>(coupler);
size_t index_node1 = add(node1);
size_t index_node2 = add(node2);
fit_qubo(std::max(index_node1, index_node2));
qubo[index_node1][index_node2] = energy;
qubo[index_node2][index_node1] = energy;
}
size_t wmis_qubo::add(const NODE& node)
{
size_t index;
if(node_to_index.find(node) == node_to_index.end())
{
index_to_node.push_back(node);
index = index_to_node.size() - 1;
node_to_index.emplace(node, index);
}
else
{
index = index_of(node);
}
return index;
}
void wmis_qubo::fit_qubo(const size_t node_index)
{
size_t required_size = node_index + 1;
if(qubo.size() >= required_size)
{
return;
}
size_t old_size = qubo.size();
qubo.resize(required_size);
for(size_t i=0; i < required_size; i++)
{
qubo[i].resize(required_size);
std::fill(qubo[i].begin() + old_size, qubo[i].end(), 0.0);
}
}
size_t wmis_qubo::index_of(const NODE& node) const
{
return node_to_index.at(node);
}
const satlab::wmis_qubo::NODE& wmis_qubo::node_at(size_t index) const
{
return index_to_node.at(index);
}
const qbscxx::QUBO& wmis_qubo::get_qubo() const
{
return qubo;
}
}

52
src/util/wmis_qubo.h Normal file
View File

@@ -0,0 +1,52 @@
#ifndef WMIS_QUBO_H
#define WMIS_QUBO_H
#include "types.h"
#include <map>
#include <tuple>
#include <vector>
namespace satlab
{
/**
* @todo write docs
*/
class wmis_qubo
{
public:
using NODE = std::tuple<int, int>;
using COUPLER = std::tuple<NODE, NODE, qbscxx::ENERGY_T>;
using INDEX_TO_NODE = std::vector<NODE>;
using NODE_TO_INDEX = std::map<NODE, size_t>;
wmis_qubo() = default;
virtual ~wmis_qubo() = default;
wmis_qubo(const wmis_qubo& other) = default;
wmis_qubo(wmis_qubo&& other) = default;
wmis_qubo& operator=(const wmis_qubo& other) = default;
wmis_qubo& operator=(wmis_qubo&& other) = default;
void add(const COUPLER& coupler);
const NODE& node_at(size_t index) const;
size_t index_of(const NODE& node) const;
const qbscxx::QUBO& get_qubo() const;
private:
size_t add(const NODE& node);
void fit_qubo(const size_t node_index);
qbscxx::QUBO qubo;
INDEX_TO_NODE index_to_node;
NODE_TO_INDEX node_to_index;
};
}
#endif // WMIS_QUBO_H