#!/usr/bin/env python3 import numpy as np from . import kSAT from tqdm import tqdm import math import random __VERTEX_WEIGHT__ = -2#-1 __EDGE_WEIGHT__ = 2#2 def WMISdictQUBO(kSATInstance): quboInstance = {} for clauseIndex in range(kSATInstance.getNumberOfClauses()): clause = kSATInstance.getClause(clauseIndex) # build triangles for varIndexInClause in range(len(clause)): label = kSATInstance.getLableOfBinding(clauseIndex, clause[varIndexInClause]) quboInstance[(label, label)] = __VERTEX_WEIGHT__ for i in range(varIndexInClause + 1, len(clause)): targetLabel = kSATInstance.getLableOfBinding(clauseIndex, clause[i]) quboInstance[(label, targetLabel)] = __EDGE_WEIGHT__ # connect conflicts for conflict in kSATInstance.getConflicts(): quboInstance[(conflict[0], conflict[1])] = __EDGE_WEIGHT__ return quboInstance def WMISdictQUBO_2(kSATInstance): quboInstance = {} for clauseIndex in range(kSATInstance.getNumberOfClauses()): clause = kSATInstance.getClause(clauseIndex) # build triangles for varIndexInClause in range(len(clause)): lit = clause[varIndexInClause] var = abs(lit) aux = "z{}_{}".format(clauseIndex, var) var_node = "x{}".format(var) if lit < 0: quboInstance[(aux, aux)] = __VERTEX_WEIGHT__ quboInstance[(var_node, aux)] = __EDGE_WEIGHT__ else: quboInstance[(var_node, aux)] = __VERTEX_WEIGHT__ for i in range(varIndexInClause + 1, len(clause)): var2 = abs(clause[i]) aux2 = "z{}_{}".format(clauseIndex, var2) quboInstance[(aux, aux2)] = __EDGE_WEIGHT__ return quboInstance # only 3sat def primitiveQUBO(sat): quboInstance = {} chains = {} for clauseIndex in range(sat.getNumberOfClauses()): clause = sat.getClause(clauseIndex); #build clause primitives lit1 = "c{}_l{}".format(clauseIndex, clause[0]) lit2 = "c{}_l{}".format(clauseIndex, clause[1]) lit3 = "c{}_l{}".format(clauseIndex, clause[2]) aux1 = "z{}_{}".format(clauseIndex, 1) aux2 = "z{}_{}".format(clauseIndex, 2) aux3 = "z{}_{}".format(clauseIndex, 3) aux4 = "z{}_{}".format(clauseIndex, 4) quboInstance[(lit1, lit1)] = 1; quboInstance[(lit2, lit2)] = 1; quboInstance[(lit3, lit3)] = 1; quboInstance[(aux1, aux1)] = -2; quboInstance[(aux2, aux2)] = 1; quboInstance[(aux3, aux3)] = -2; quboInstance[(aux4, aux4)] = -2; quboInstance[(lit1, lit2)] = 1; quboInstance[(lit1, aux1)] = -2; quboInstance[(lit2, aux1)] = -2; quboInstance[(aux1, aux2)] = -2; quboInstance[(aux2, aux3)] = -2; quboInstance[(aux2, lit3)] = 1; quboInstance[(lit3, aux3)] = -2; quboInstance[(aux3, aux4)] = -2; if clause[0] in chains: chains[clause[0]].append(lit1) else: chains[clause[0]] = [lit1] if clause[1] in chains: chains[clause[1]].append(lit2) else: chains[clause[1]] = [lit2] if clause[2] in chains: chains[clause[2]].append(lit3) else: chains[clause[2]] = [lit3] #build chains longestChain = 0; for lit, nodes in chains.items(): if len(nodes) > longestChain: longestChain = len(nodes) if lit > 0 and -1 * lit in chains: len_smaller_chain = min(len(chains[lit]), len(chains[-lit])) indices = random.sample(list(range(len_smaller_chain)), round(len_smaller_chain / 2)) for index in indices: quboInstance[(chains[lit][index], chains[-1*lit][index])] = 10 #quboInstance[(chains[lit][0], chains[-1*lit][0])] = 2 print("longest chain = {}".format(longestChain)) for nodes in chains.values(): while len(nodes) > 1: quboInstance[(nodes[0], nodes[1])] = -2; nodes.pop(0) return quboInstance # only 3sat def primitiveQUBO_2(sat): quboInstance = {} chains = {} for clauseIndex in range(sat.getNumberOfClauses()): clause = sat.getClause(clauseIndex) lit1 = clause[0] lit2 = clause[1] lit3 = clause[2] var1 = abs(lit1) var2 = abs(lit2) var3 = abs(lit3) sign1 = 1 if lit1 > 0 else -1 sign2 = 1 if lit2 > 0 else -1 sign3 = 1 if lit3 > 0 else -1 node_var1 = "x{}".format(var1) node_var2 = "x{}".format(var2) node_var3 = "x{}".format(var3) node_aux1 = "a{}_{}".format(clauseIndex, 1) node_aux2 = "a{}_{}".format(clauseIndex, 2) node_aux3 = "a{}_{}".format(clauseIndex, 3) node_aux4 = "a{}_{}".format(clauseIndex, 4) quboInstance[(node_var1, node_var1)] = 1 * sign1 quboInstance[(node_var2, node_var2)] = 1 * sign2 quboInstance[(node_var3, node_var3)] = 1 * sign3 quboInstance[(node_aux1, node_aux1)] = -2 quboInstance[(node_aux2, node_aux2)] = 1 quboInstance[(node_aux3, node_aux3)] = -2 quboInstance[(node_aux4, node_aux4)] = -2 quboInstance[(node_var1, node_var2)] = 1 * sign1 * sign2 quboInstance[(node_var1, node_aux1)] = -2 * sign1 quboInstance[(node_var2, node_aux1)] = -2 * sign2 quboInstance[(node_aux1, node_aux2)] = -2 quboInstance[(node_aux2, node_var3)] = 1 * sign3 quboInstance[(node_var3, node_aux3)] = -2 * sign3 quboInstance[(node_aux2, node_aux3)] = -2 quboInstance[(node_var3, node_aux4)] = -2 return quboInstance # only 3sat def primitiveQUBO_3(sat): quboInstance = {} chains = {} lits = {} vars = {} n_clauses = sat.getNumberOfClauses() for clauseIndex in range(sat.getNumberOfClauses()): clause = sat.getClause(clauseIndex) lit1 = clause[0] lit2 = clause[1] lit3 = clause[2] lits[lit1] = True lits[lit2] = True lits[lit3] = True var1 = abs(lit1) var2 = abs(lit2) var3 = abs(lit3) vars[var1] = True vars[var2] = True vars[var3] = True node_lit1 = "x{}".format(lit1) node_lit2 = "x{}".format(lit2) node_lit3 = "x{}".format(lit3) node_aux1 = "z{}_{}".format(clauseIndex, 1) node_aux2 = "z{}_{}".format(clauseIndex, 2) node_aux3 = "z{}_{}".format(clauseIndex, 3) node_aux4 = "z{}_{}".format(clauseIndex, 4) quboInstance[(node_lit1, node_lit1)] = 1 quboInstance[(node_lit2, node_lit2)] = 1 quboInstance[(node_lit3, node_lit3)] = 1 quboInstance[(node_aux1, node_aux1)] = -2 quboInstance[(node_aux2, node_aux2)] = 1 quboInstance[(node_aux3, node_aux3)] = -2 quboInstance[(node_aux4, node_aux4)] = -2 quboInstance[(node_lit1, node_lit2)] = 1 quboInstance[(node_lit1, node_aux1)] = -2 quboInstance[(node_lit2, node_aux1)] = -2 quboInstance[(node_aux1, node_aux2)] = -2 quboInstance[(node_aux2, node_lit3)] = 1 quboInstance[(node_lit3, node_aux3)] = -2 quboInstance[(node_aux2, node_aux3)] = -2 quboInstance[(node_aux3, node_aux4)] = -2 for var in vars.keys(): if var in lits and -var in lits: node_var = "x{}".format(var) node_nvar = "x{}".format(-var) print((node_var, node_nvar)) quboInstance[(node_var, node_nvar)] = 2 return quboInstance def primitiveQUBO_4(sat): quboInstance = {} clauses_per_lit = {} lits = {} vars = {} n_clauses = sat.getNumberOfClauses() master_z = "zm" #quboInstance[(master_z, master_z)] = -2 for clauseIndex in range(sat.getNumberOfClauses()): clause = sat.getClause(clauseIndex) lit1 = clause[0] lit2 = clause[1] lit3 = clause[2] lits[lit1] = True lits[lit2] = True lits[lit3] = True sign1 = 1 if lit1 > 0 else -1 sign2 = 1 if lit2 > 0 else -1 sign3 = 1 if lit3 > 0 else -1 for lit in clause: if lit in clauses_per_lit: clauses_per_lit[lit] += 1 else: clauses_per_lit[lit] = 1 var1 = abs(lit1) var2 = abs(lit2) var3 = abs(lit3) vars[var1] = True vars[var2] = True vars[var3] = True node_lit1 = "x{}".format(lit1) node_lit2 = "x{}".format(lit2) node_lit3 = "x{}".format(lit3) node_aux = "z{}".format(clauseIndex) #quboInstance[(node_aux, node_aux)] = -2 #quboInstance[(node_aux, master_z)] = -2 #quboInstance[(node_lit1, node_lit1)] = +1 #* sign3 #quboInstance[(node_lit2, node_lit2)] = +1 #* sign3 #quboInstance[(node_lit3, node_lit3)] = +1 #* sign3 quboInstance[(node_lit1, node_aux)] = -2 #* sign1 quboInstance[(node_lit2, node_aux)] = -2 #* sign2 quboInstance[(node_lit3, node_aux)] = -2 #* sign3 for lit in lits.keys(): node_lit = "x{}".format(lit) #quboInstance[(node_lit, node_lit)] = 2 * clauses_per_lit[lit] for var in vars.keys(): if var in lits and -var in lits: node_var = "x{}".format(var) node_nvar = "x{}".format(-var) max_clauses = max(clauses_per_lit[var], clauses_per_lit[-var]) num_clauses = clauses_per_lit[var] + clauses_per_lit[-var] print((node_var, node_nvar)) quboInstance[(node_var, node_nvar)] = 2 * num_clauses #quboInstance[(node_var, node_nvar)] = 2# * num_clauses return quboInstance def primitiveQUBO_5(sat): quboInstance = {} clauses_per_lit = {} lits = {} vars = {} n_clauses = sat.getNumberOfClauses() master_z = "zm" #quboInstance[(master_z, master_z)] = -2 for clauseIndex in range(sat.getNumberOfClauses()): clause = sat.getClause(clauseIndex) lit1 = clause[0] lit2 = clause[1] lit3 = clause[2] lits[lit1] = True lits[lit2] = True lits[lit3] = True for lit in clause: if lit in clauses_per_lit: clauses_per_lit[lit] += 1 else: clauses_per_lit[lit] = 1 var1 = abs(lit1) var2 = abs(lit2) var3 = abs(lit3) vars[var1] = True vars[var2] = True vars[var3] = True node_lit1 = "x{}".format(lit1) node_lit2 = "x{}".format(lit2) node_lit3 = "x{}".format(lit3) node_aux1 = "z{}_1".format(clauseIndex) node_aux2 = "z{}_2".format(clauseIndex) quboInstance[(node_lit1, node_aux1)] = -2 quboInstance[(node_lit2, node_aux1)] = -2 quboInstance[(node_lit1, node_lit2)] = +2 quboInstance[(node_aux1, node_lit3)] = +2 quboInstance[(node_lit3, node_aux2)] = -2 for var in vars.keys(): if var in lits and -var in lits: node_var = "x{}".format(var) node_nvar = "x{}".format(-var) max_clauses = max(clauses_per_lit[var], clauses_per_lit[-var]) num_clauses = clauses_per_lit[var] + clauses_per_lit[-var] #print((node_var, node_nvar)) quboInstance[(node_var, node_nvar)] = 2 * max_clauses return quboInstance def primitiveQUBO_6(sat): quboInstance = {} clauses_per_lit = {} lits = {} vars = {} n_clauses = sat.getNumberOfClauses() master_z = "zm" #quboInstance[(master_z, master_z)] = -2 for clauseIndex in range(sat.getNumberOfClauses()): clause = sat.getClause(clauseIndex) lit1 = clause[0] lit2 = clause[1] lit3 = clause[2] lits[lit1] = True lits[lit2] = True lits[lit3] = True for lit in clause: if lit in clauses_per_lit: clauses_per_lit[lit] += 1 else: clauses_per_lit[lit] = 1 var1 = abs(lit1) var2 = abs(lit2) var3 = abs(lit3) vars[var1] = True vars[var2] = True vars[var3] = True node_lit1 = "x{}".format(lit1) node_lit2 = "x{}".format(lit2) node_lit3 = "x{}".format(lit3) node_aux1 = "z{}_1".format(clauseIndex) node_aux2 = "z{}_2".format(clauseIndex) node_aux3 = "z{}_3".format(clauseIndex) node_aux4 = "z{}_4".format(clauseIndex) quboInstance[(node_lit1, node_aux1)] = -2 quboInstance[(node_lit2, node_aux2)] = -2 quboInstance[(node_aux1, node_aux2)] = +2 quboInstance[(node_aux1, node_aux3)] = -2 quboInstance[(node_aux2, node_aux3)] = -2 quboInstance[(node_aux1, node_aux1)] = +2 quboInstance[(node_aux2, node_aux2)] = +2 quboInstance[(node_aux3, node_lit3)] = +2 quboInstance[(node_lit3, node_aux4)] = -2 for var in vars.keys(): if var in lits and -var in lits: node_var = "x{}".format(var) node_nvar = "x{}".format(-var) max_clauses = max(clauses_per_lit[var], clauses_per_lit[-var]) num_clauses = clauses_per_lit[var] + clauses_per_lit[-var] #print((node_var, node_nvar)) quboInstance[(node_var, node_nvar)] = 2 * max_clauses return quboInstance def primitiveQUBO_7(sat): quboInstance = {} clauses_per_lit = {} lits = {} vars = {} n_clauses = sat.getNumberOfClauses() master_z = "zm" #quboInstance[(master_z, master_z)] = -2 direct_cupplers = {} for clauseIndex in range(sat.getNumberOfClauses()): clause = sat.getClause(clauseIndex) lit1 = clause[0] lit2 = clause[1] lit3 = clause[2] lits[lit1] = True lits[lit2] = True lits[lit3] = True for lit in clause: if lit in clauses_per_lit: clauses_per_lit[lit] += 1 else: clauses_per_lit[lit] = 1 var1 = abs(lit1) var2 = abs(lit2) var3 = abs(lit3) vars[var1] = True vars[var2] = True vars[var3] = True node_lit1 = "x{}".format(lit1) node_lit2 = "x{}".format(lit2) node_lit3 = "x{}".format(lit3) node_aux1 = "z{}_1".format(clauseIndex) node_aux2 = "z{}_2".format(clauseIndex) quboInstance[(node_lit1, node_aux1)] = -2 quboInstance[(node_lit2, node_aux1)] = -2 quboInstance[(node_lit1, node_lit2)] = +2 quboInstance[(node_aux1, node_lit3)] = +2 quboInstance[(node_lit3, node_aux2)] = -2 if (node_lit1, node_lit2) in direct_cupplers: direct_cupplers[(node_lit1, node_lit2)] += 1 else: direct_cupplers[(node_lit1, node_lit2)] = 1 for var in vars.keys(): if var in lits and -var in lits: node_var = "x{}".format(var) node_nvar = "x{}".format(-var) max_clauses = max(clauses_per_lit[var], clauses_per_lit[-var]) num_clauses = clauses_per_lit[var] + clauses_per_lit[-var] print((node_var, node_nvar)) quboInstance[(node_var, node_nvar)] = 2 * max_clauses for coupler, count in direct_cupplers.items(): quboInstance[coupler] = count * 2 return quboInstance def primitiveQUBO_8(sat): quboInstance = {} clauses_per_lit = {} lits = {} vars = {} n_clauses = sat.getNumberOfClauses() direct_cupplers = {} for clauseIndex in range(sat.getNumberOfClauses()): clause = sorted(sat.getClause(clauseIndex)) if clause[2] < 0: __add_3not_or_clause(quboInstance, clause, clauseIndex) elif clause[1] < 0: __add_2not_or_clause(quboInstance, clause, clauseIndex) elif clause[0] < 0: __add_1not_or_clause(quboInstance, clause, clauseIndex, direct_cupplers) else: __add_3_or_clause(quboInstance, clause, clauseIndex, direct_cupplers) for coupler, count in direct_cupplers.items(): quboInstance[coupler] = count * 2 return quboInstance def __add_3not_or_clause(quboInstance, clause, clause_index): var1 = abs(clause[0]) var2 = abs(clause[1]) var3 = abs(clause[2]) node_var1 = "x{}".format(var1) node_var2 = "x{}".format(var2) node_var3 = "x{}".format(var3) node_aux1 = "z{}_1".format(clause_index) node_aux2 = "z{}_2".format(clause_index) node_aux3 = "z{}_3".format(clause_index) quboInstance[(node_var1, node_aux1)] = +2 quboInstance[(node_var2, node_aux2)] = +2 quboInstance[(node_aux1, node_aux2)] = +2 quboInstance[(node_aux1, node_aux1)] = -2 quboInstance[(node_aux2, node_aux2)] = -2 quboInstance[(node_var1, node_aux3)] = -2 quboInstance[(node_var2, node_aux3)] = -2 quboInstance[(node_var3, node_aux3)] = +2 quboInstance[(node_aux3, node_aux3)] = +2 def __add_2not_or_clause(quboInstance, clause, clause_index): var1 = abs(clause[0]) var2 = abs(clause[1]) var3 = abs(clause[2]) node_var1 = "x{}".format(var1) node_var2 = "x{}".format(var2) node_var3 = "x{}".format(var3) node_aux1 = "z{}_1".format(clause_index) node_aux2 = "z{}_2".format(clause_index) node_aux3 = "z{}_3".format(clause_index) node_aux4 = "z{}_4".format(clause_index) node_aux5 = "z{}_5".format(clause_index) quboInstance[(node_var1, node_aux1)] = +2 quboInstance[(node_var2, node_aux2)] = +2 quboInstance[(node_aux1, node_aux2)] = +2 quboInstance[(node_aux1, node_aux3)] = -2 quboInstance[(node_aux2, node_aux3)] = -2 quboInstance[(node_aux3, node_aux3)] = +2 quboInstance[(node_aux3, node_aux4)] = -2 quboInstance[(node_var3, node_aux5)] = -2 quboInstance[(node_aux4, node_aux5)] = +2 def __add_1not_or_clause(quboInstance, clause, clause_index, direct_cupplers): var1 = abs(clause[1]) var2 = abs(clause[2]) var3 = abs(clause[0]) node_var1 = "x{}".format(var1) node_var2 = "x{}".format(var2) node_var3 = "x{}".format(var3) node_aux1 = "z{}_1".format(clause_index) node_aux2 = "z{}_2".format(clause_index) quboInstance[(node_var1, node_var2)] = +2 quboInstance[(node_var1, node_aux1)] = -2 quboInstance[(node_var2, node_aux1)] = -2 quboInstance[(node_aux1, node_aux2)] = +2 quboInstance[(node_var3, node_aux2)] = +2 quboInstance[(node_aux2, node_aux2)] = -2 if (node_var1, node_var2) in direct_cupplers: direct_cupplers[(node_var1, node_var2)] += 1 else: direct_cupplers[(node_var1, node_var2)] = 1 def __add_3_or_clause(quboInstance, clause, clause_index, direct_cupplers): var1 = abs(clause[0]) var2 = abs(clause[1]) var3 = abs(clause[2]) node_var1 = "x{}".format(var1) node_var2 = "x{}".format(var2) node_var3 = "x{}".format(var3) node_aux1 = "z{}_1".format(clause_index) node_aux2 = "z{}_2".format(clause_index) quboInstance[(node_var1, node_var2)] = +2 quboInstance[(node_var1, node_aux1)] = -2 quboInstance[(node_var2, node_aux1)] = -2 quboInstance[(node_aux1, node_var3)] = +2 quboInstance[(node_var3, node_aux2)] = -2 if (node_var1, node_var2) in direct_cupplers: direct_cupplers[(node_var1, node_var2)] += 1 else: direct_cupplers[(node_var1, node_var2)] = 1 class QuboWriter: def __init__(self, qubo): self.__labelIndexDict = {} self.__qubo = qubo self.__initLabelIndexDict(self.__qubo) print(self.__labelIndexDict) def __initLabelIndexDict(self, qubo): indexCount = 0 for coupler in qubo: label1 = coupler[0] label2 = coupler[1] if label1 not in self.__labelIndexDict: self.__labelIndexDict[label1] = indexCount indexCount += 1 if label2 not in self.__labelIndexDict: self.__labelIndexDict[label2] = indexCount indexCount += 1 def write(self, filePath): quboFile = open(filePath, "w") self.__writeQuboFileHeader(quboFile) self.__writeQuboFileNodes(quboFile) self.__writeQuboFileCouplers(quboFile) quboFile.close() def __writeQuboFileHeader(self, quboFile): numberOfNodes = len(self.__labelIndexDict) numberOfCouplers = len(self.__qubo) - numberOfNodes quboFile.write("c\n") quboFile.write("c this is a generated qubo file\n") quboFile.write("c\n") quboFile.write("p qubo 0 %d %d %d\n" %(numberOfNodes, numberOfNodes, numberOfCouplers)) def __writeQuboFileNodes(self, quboFile): for label in self.__labelIndexDict: self.__writeCoupler(quboFile, (label, label)) def __writeCoupler(self, quboFile, coupler): indices = self.__getNodeIndicesFromCoupler(coupler) quboFile.write("%d %d %d\n" % (indices[0], indices[1], self.__qubo[coupler])) def __getNodeIndicesFromCoupler(self, coupler): index1 = self.__labelIndexDict[coupler[0]] index2 = self.__labelIndexDict[coupler[1]] if index1 <= index2: return [index1, index2] else: return [index2, index1] def __writeQuboFileCouplers(self, quboFile): for coupler in self.__qubo: if coupler[0] != coupler[1]: self.__writeCoupler(quboFile, coupler)