QA_SAT
/
qubo_lab


								#!/usr/bin/env python3


								from util.kSAT import kSAT

								import util.randomSAT as rand_sat

								import util.SAT2QUBO as SAT2QUBO

								import util.script as script

								import util.queries as queries

								import util.graph as graph


								from dwave.system.composites import FixedEmbeddingComposite

								import dimod

								from neal import SimulatedAnnealingSampler

								import minorminer

								import networkx as nx

								import dwave_networkx as dnx

								import dwave.embedding


								from dwave.cloud import Client

								from dwave.cloud import Future

								from dwave.system.samplers import DWaveSampler


								from dwave_qbsolv import QBSolv


								import numpy as np

								import random

								import re


								from tqdm import tqdm


								def main():

								    #__wmis()

								    __pqubo_3()

								    #__pqubo()

								    #__wmis3()


								def __qubo_to_nx_graph(qubo):

								    graph = nx.Graph()


								    for coupler, energy in qubo.items():

								        if coupler[0] != coupler[1]:

								            graph.add_edge(coupler[0], coupler[1], weight=energy)


								    return graph


								def __wmis2():

								    db = script.connect_to_instance_pool("dbc")

								    target_graph =  dnx.chimera_graph(16, 16, 4)

								    target_graph_id = queries.get_id_of_solver_graph(db["solver_graphs"],

								                                                     nx.node_link_data(target_graph))

								    instance_id = "5c9ccb998c6fe61926458351"

								    qubo, wmis_id = queries.load_WMIS_qubo_of_instance(db["wmis_qubos"], instance_id)


								    emb = queries.load_embedding(db["embeddings"], wmis_id, target_graph_id)


								    chimera_sampler = dimod.StructureComposite(SimulatedAnnealingSampler(),

								                                               target_graph.nodes(),

								                                               target_graph.edges())


								    sampler = FixedEmbeddingComposite(chimera_sampler, emb)


								    res = sampler.sample_qubo(__negate_qubo(qubo))


								    print(res.first)


								def __wmis3():

								    db = script.connect_to_instance_pool()

								    target_graph =  dnx.chimera_graph(16, 16, 4)

								    target_graph_id = queries.get_id_of_solver_graph(db["solver_graphs"],

								                                                     nx.node_link_data(target_graph))


								    solver_input_query = queries.WMIS_solver_input_scope_query(db)

								    solver_input_query.query("c42_vLogistic_6", target_graph_id)


								    base_sampler = SimulatedAnnealingSampler()

								    #base_sampler = QBSolv()

								    chimera_sampler = dimod.StructureComposite(base_sampler,

								                                               target_graph.nodes(),

								                                               target_graph.edges())


								    for solver_input in tqdm(solver_input_query):


								        sampler = FixedEmbeddingComposite(chimera_sampler, solver_input["embeddings"][0])


								        #res = sampler.sample_qubo(solver_input["qubo"], solver_limit=2048)

								        res = sampler.sample_qubo(solver_input["qubo"])


								        script.save_result(db["wmis_siman_results"],

								                                               res,

								                                               solver_input,

								                                               0,

								                                               1)


								def __wmis_qpu():

								    db = script.connect_to_instance_pool()


								    base_solver = DWaveSampler()


								    solver_graph = graph.create_qpu_solver_nxgraph(base_solver)

								    solver_graph_id = queries.get_id_of_solver_graph(db["solver_graphs"],

								                                                     nx.node_link_data(solver_graph))


								    solver_input_query = queries.WMIS_solver_input_scope_query(db)

								    solver_input_query.query("c42_vLogistic_6", solver_graph_id)


								    for solver_input in tqdm(solver_input_query):


								        embedding = solver_input["embeddings"][0]

								        qubo = solver_input["qubo"]


								        solver = FixedEmbeddingComposite(base_solver, embedding)


								        res = solver.sample_qubo(qubo, annealing_time=5)


								        script.save_result(db["wmis_qpu_results"],

								                                               res,

								                                               solver_input,

								                                               emb_list_index = 0,

								                                               run = 1)


								def __wmis():

								    sat_count = 0

								    no_embedding_count = 0


								    for i in range(200):

								        sat = rand_sat.generateRandomKSAT(40, 14, 3)

								        qubo = SAT2QUBO.WMISdictQUBO(sat)

								        #qubo = SAT2QUBO.WMISdictQUBO(sat)

								        nx_qubo = __qubo_to_nx_graph(qubo)


								        target_graph = dnx.chimera_graph(16, 16, 4)


								        emb = minorminer.find_embedding(nx_qubo.edges(),

								                                        target_graph.edges(),

								                                        return_overlap=True)


								        if emb[1] != 1:

								            print("no embedding found")

								            no_embedding_count += 1

								            continue


								        #print(emb[0])


								        chimera_sampler = dimod.StructureComposite(SimulatedAnnealingSampler(),

								                                                target_graph.nodes(),

								                                                target_graph.edges())


								        sampler = FixedEmbeddingComposite(chimera_sampler, emb[0])


								        res = sampler.sample_qubo(qubo, chain_strength=2)

								        #res = SimulatedAnnealingSampler().sample_qubo(qubo)


								        #dwave.embedding.chain_breaks.majority_vote(res, emb[0])


								        first = res.first


								        print("chain_break_fraction={}".format(first.chain_break_fraction))

								        #for lit, spin in first.sample.items():

								            #print(lit, spin)

								        print("true count: {}".format(np.count_nonzero(list(first.sample.values()))))


								        assignments = {}


								        for coupler, energy in first.sample.items():


								            var = abs(coupler[1])


								            if var not in assignments:

								                assignments[var] = {"all": []}


								            if energy == 1:

								                assignments[var]["all"].append(1 if coupler[1] > 0 else 0)


								        __majority_vote(assignments)


								        #for var, a in assignments.items():

								            ##print(var, np.sort(a["all"]), __majority_percentage(a["all"]))

								            #print(var, a)

								        final = __extract_assignment(assignments)

								        print(final)

								        print("satisfies sat: {}".format(sat.checkAssignment(final)))


								        if sat.checkAssignment(final):

								            sat_count += 1


								    print("sat ratio: {}".format(sat_count / (200 - no_embedding_count)))


								def __optimize_assignment(sat, assignment, consistencies):

								    rnd = random.Random()


								    max_steps = 4000

								    steps = 0


								    while not sat.checkAssignment(assignment) and steps < max_steps:

								        steps += 1


								        for i in range(len(assignment)):

								            if 0.9 * rnd.random() > consistencies[i]:

								                assignment[i] = (1 + assignment[i]) % 2

								                consistencies[i] = 1 - consistencies[i]


								    print("steps: {}".format(steps))


								    return assignment


								def __random_assignment(number_of_variables):

								    rnd = random.Random()

								    assignment = [rnd.choice([0, 1]) for i in range(number_of_variables)]

								    consistencies = [0.5 for i in range(number_of_variables)]


								    return assignment, consistencies


								def __extract_assignment(assignments):

								    assignment = [0 for i in range(len(assignments))]


								    for var, a in assignments.items():

								        assignment[var - 1] = a["major"]


								    return assignment


								def __extract_consistencies(assignments)    :

								    consistencies = [0.0 for i in range(len(assignments))]


								    for var, a in assignments.items():

								        consistencies[var - 1] = a["consistency"]


								    return consistencies


								def __majority_vote(assignments):

								    for var, a in assignments.items():

								        assignments[var]["major"] = 1 if __true_percentage(a["all"]) >= 0.5 else 0

								        assignments[var]["consistency"] = __majority_percentage(a["all"])


								def __true_percentage(a):

								    if len(a) == 0:

								        return 0


								    return np.count_nonzero(a) / len(a)


								def __majority_percentage(a):

								    true_perc = __true_percentage(a)


								    return true_perc if true_perc >= 0.5 else 1 - true_perc


								def __pqubo():

								    sat = rand_sat.generateRandomKSAT(42, 7, 3)

								    ising = SAT2QUBO.primitiveQUBO(sat)

								    nx_qubo = __qubo_to_nx_graph(ising)


								    target_graph = dnx.chimera_graph(16, 16, 4)


								    emb = minorminer.find_embedding(nx_qubo.edges(),

								                                    target_graph.edges(),

								                                    return_overlap=True)


								    if emb[1] != 1:

								        print("no embedding found")

								        return


								    chimera_sampler = dimod.StructureComposite(SimulatedAnnealingSampler(),

								                                               target_graph.nodes(),

								                                               target_graph.edges())


								    sampler = FixedEmbeddingComposite(chimera_sampler, emb[0])


								    h, J = __split_ising(ising)


								    res = sampler.sample_ising(h, J)

								    #res = sampler.sample_ising(h, J, find_max=False)


								    print(res.truncate(10))


								    sample = res.first.sample


								    extracted = {}


								    r = re.compile("c\d+_l-?\d*")


								    for label, assignment in sample.items():

								        if r.fullmatch(label):


								            extracted[tuple(re.split(r"\_l", label[1:]))] = assignment


								    model = [True for i in range(len(extracted))]


								    assignments = {}


								    for label, assignment in extracted.items():

								        clause = int(label[0])

								        lit = int(label[1])

								        var = abs(lit)


								        if lit < 0:

								            assignment *= -1


								        if var in assignments:

								            assignments[var].append(assignment)

								        else:

								            assignments[var] = [assignment]


								    conflicts = False

								    for var, a in assignments.items():

								        if abs(np.sum(a)) != len(a):

								            conflicts = True

								            print("conflicts - no solution found")

								            print(var, np.sort(a))


								    if conflicts:

								        print(assignments)

								        return


								    model = [True for i in range(sat.getNumberOfVariables())]


								    for var, assignment in assignments.items():

								        model[var - 1] = True if assignment[0] > 0 else False


								    print(model, sat.checkAssignment(model))


								def __pqubo_3():

								    sat_count = 0

								    no_embedding_count = 0


								    for i in range(200):

								        sat = rand_sat.generateRandomKSAT(40, 14, 3)

								        #ising = SAT2QUBO.primitiveQUBO_8(sat)

								        ising = SAT2QUBO.WMISdictQUBO_2(sat)

								        nx_qubo = __qubo_to_nx_graph(ising)


								        target_graph = dnx.chimera_graph(16, 16, 4)


								        emb = minorminer.find_embedding(nx_qubo.edges(),

								                                        target_graph.edges(),

								                                        return_overlap=True)


								        if emb[1] != 1:

								            print("no embedding found")

								            no_embedding_count += 1

								            continue


								        chimera_sampler = dimod.StructureComposite(SimulatedAnnealingSampler(),

								                                                target_graph.nodes(),

								                                                target_graph.edges())


								        sampler = FixedEmbeddingComposite(chimera_sampler, emb[0])


								        h, J = __split_ising(ising)


								        res = sampler.sample_qubo(ising)

								        #res = sampler.sample_ising(h, J, find_max=False)


								        print(res.truncate(10))


								        print("chain_break_fraction", res.first.chain_break_fraction)


								        sample = res.first.sample


								        assignments = {}

								        vars = set()


								        for node, energy in sample.items():

								            if node[0] == "x":

								                lit = int(node[1:])


								                vars.add(abs(lit))


								                assignments[lit] = energy


								        print(assignments)


								        conflicts = set()

								        for var in vars:

								            if var in assignments and -var in assignments:

								                if assignments[var] == assignments[-var]:

								                    print("conflict at var: {}".format(var))

								                    conflicts.add(var)


								        #if conflicts:

								        #    return


								        model = [True for i in range(len(vars))]


								        for var in vars:

								            if var in assignments:

								                model[var - 1] = True if assignments[var] == 1 else False

								            elif -var in assignments:

								                model[var - 1] = True if assignments[-var] == 0 else False


								        var_list = list(conflicts)


								        print(sat.checkAssignment(model))

								        if len(var_list) > 0:

								            for i in range(1000):


								                if sat.checkAssignment(model):

								                    print(i)

								                    break


								                rand_var = random.choice(var_list)


								                model[rand_var - 1] = not model[rand_var - 1]


								        print()


								        print(model)

								        print()


								        print(sat.checkAssignment(model))

								        if sat.checkAssignment(model):

								            sat_count += 1

								        print()


								        degrees = sat.getDegreesOfVariables()


								        for var in conflicts:

								            node_var = "x{}".format(var)

								            node_nvar = "x{}".format(-var)

								            print("var {}: deg={}, coupler={}, e={}, ne={}"

								                .format(var,

								                        degrees[var],

								                        ising[(node_var, node_nvar)],

								                        assignments[var],

								                        assignments[-var]))


								    print("sat ratio: {}".format(sat_count / (200 - no_embedding_count)))


								def __split_ising(ising):

								    h = {}

								    J = {}


								    for coupler, energy in ising.items():

								        if coupler[0] == coupler[1]:

								            h[coupler[0]] = energy

								        else:

								            J[coupler] = energy


								    return h, J


								def __negate_qubo(qubo):

								    negative_qubo = {}


								    for coupler, energy in qubo.items():

								        negative_qubo[coupler] = -1 * energy


								    return  negative_qubo


								if __name__ == "__main__":

								    main()