Browse Source

randomSAT: fixed random sat generation; satlabcxx: fixed *2bson converters

master
Tom 5 years ago
parent
commit
9a8c908eae
6 changed files with 13 additions and 10 deletions
  1. +1
    -1
      src/util/ksatModel2bson.h
  2. +1
    -1
      src/util/minisatResult2bson.h
  3. +1
    -1
      src/util/minisatStats2bson.h
  4. +5
    -5
      test_data_extraction.py
  5. +1
    -1
      test_sat_to_qubo_workflow.py
  6. +4
    -1
      util/randomSAT.py

+ 1
- 1
src/util/ksatModel2bson.h View File

@ -13,7 +13,7 @@ namespace satlab
template<typename = bsoncxx::builder::stream::array, typename = KSATinstance::MODEL> template<typename = bsoncxx::builder::stream::array, typename = KSATinstance::MODEL>
void convert(bsoncxx::builder::stream::array& builder, const KSATinstance::MODEL& model) void convert(bsoncxx::builder::stream::array& builder, const KSATinstance::MODEL& model)
{ {
builder = bsoncxx::builder::stream::array();
builder.clear();
for(auto& lit : model) for(auto& lit : model)
{ {


+ 1
- 1
src/util/minisatResult2bson.h View File

@ -18,7 +18,7 @@ void convert(bsoncxx::builder::stream::document& builder, const MinisatResult& r
using ARRAY_BUILDER = bsoncxx::builder::stream::array; using ARRAY_BUILDER = bsoncxx::builder::stream::array;
using DOCUMENT_BUILDER = bsoncxx::builder::stream::document; using DOCUMENT_BUILDER = bsoncxx::builder::stream::document;
builder = DOCUMENT_BUILDER();
builder.clear();
ARRAY_BUILDER model; ARRAY_BUILDER model;
DOCUMENT_BUILDER stats; DOCUMENT_BUILDER stats;


+ 1
- 1
src/util/minisatStats2bson.h View File

@ -13,7 +13,7 @@ namespace satlab
template<typename = bsoncxx::builder::stream::document, typename = MinisatStats> template<typename = bsoncxx::builder::stream::document, typename = MinisatStats>
void convert(bsoncxx::builder::stream::document& builder, const MinisatStats& stats) void convert(bsoncxx::builder::stream::document& builder, const MinisatStats& stats)
{ {
builder = bsoncxx::builder::stream::document();
builder.clear();
builder << "solves" << static_cast<int>(stats.getSolves()) builder << "solves" << static_cast<int>(stats.getSolves())
<< "starts" << static_cast<int>(stats.getStarts()) << "starts" << static_cast<int>(stats.getStarts())


+ 5
- 5
test_data_extraction.py View File

@ -4,6 +4,8 @@ import util.script as script
import util.queries as queries import util.queries as queries
import dimod import dimod
from tqdm import tqdm
def main(): def main():
wmis_siman_results_alpha_num_of_assignments() wmis_siman_results_alpha_num_of_assignments()
#wmis_siman_results() #wmis_siman_results()
@ -30,9 +32,9 @@ def wmis_siman_results_alpha_num_of_assignments():
idb = script.connect_to_instance_pool() idb = script.connect_to_instance_pool()
q = queries.WMIS_result_scope_query_raw(idb) q = queries.WMIS_result_scope_query_raw(idb)
q.query("c42_v[5-42]_1", "wmis_siman_results")
q.query("c42_v[5-84]_1", "wmis_siman_results")
insert_row = ("INSERT INTO c42_v5to42_1_wmis_results "
insert_row = ("INSERT INTO c42_v5to84_1_wmis_results "
"(result_id, " "(result_id, "
" number_of_clauses, " " number_of_clauses, "
" number_of_variables, " " number_of_variables, "
@ -42,7 +44,7 @@ def wmis_siman_results_alpha_num_of_assignments():
" energy) " " energy) "
"VALUES (%s, %s, %s, %s, %s, %s, %s) ") "VALUES (%s, %s, %s, %s, %s, %s, %s) ")
for result in q:
for result in tqdm(q):
sample_set = queries.read_raw_wmis_sample_set(result["data"]) sample_set = queries.read_raw_wmis_sample_set(result["data"])
data = script.analyze_wmis_sample(sample_set.first) data = script.analyze_wmis_sample(sample_set.first)
@ -57,8 +59,6 @@ def wmis_siman_results_alpha_num_of_assignments():
int(data["num_occurrences"]), int(data["num_occurrences"]),
int(data["energy"]))) int(data["energy"])))
print(data)
edb.commit() edb.commit()
edb_cursor.close() edb_cursor.close()
edb.close() edb.close()


+ 1
- 1
test_sat_to_qubo_workflow.py View File

@ -63,7 +63,7 @@ def __wmis3():
nx.node_link_data(target_graph)) nx.node_link_data(target_graph))
solver_input_query = queries.WMIS_solver_input_scope_query(db) solver_input_query = queries.WMIS_solver_input_scope_query(db)
solver_input_query.query("c42_v[5-42]_1", target_graph_id)
solver_input_query.query("c42_v[5-84]_1", target_graph_id)
base_sampler = SimulatedAnnealingSampler() base_sampler = SimulatedAnnealingSampler()
chimera_sampler = dimod.StructureComposite(base_sampler, chimera_sampler = dimod.StructureComposite(base_sampler,


+ 4
- 1
util/randomSAT.py View File

@ -24,6 +24,9 @@ def generateRandomKSAT(numberOfClauses,
clauses[clauseIndex].append(varIndex + 1) clauses[clauseIndex].append(varIndex + 1)
for i in range(len(clauses)):
clauses[i].sort()
#fill in the missing bindings #fill in the missing bindings
for clauseIndex, clause in enumerate(clauses): for clauseIndex, clause in enumerate(clauses):
tmpClause = [] tmpClause = []
@ -45,7 +48,7 @@ def generateRandomKSAT(numberOfClauses,
for i in range(len(tmpClause)): for i in range(len(tmpClause)):
tmpClause[i] *= random.choice([-1, 1]) tmpClause[i] *= random.choice([-1, 1])
tmpClause = list(np.sort(tmpClause))
tmpClause.sort()
if tmpClause not in clauses: if tmpClause not in clauses:
clauseIsUnique = True clauseIsUnique = True


Loading…
Cancel
Save