You can not select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
848 lines
25 KiB
848 lines
25 KiB
#!/usr/bin/env python3
|
|
|
|
import numpy as np
|
|
from . import kSAT
|
|
from tqdm import tqdm
|
|
import math
|
|
import random
|
|
|
|
__VERTEX_WEIGHT__ = -2
|
|
__EDGE_WEIGHT__ = 2
|
|
|
|
|
|
def WMISdictQUBO(kSATInstance):
|
|
__VERTEX_WEIGHT__ = -1
|
|
|
|
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
|
|
|
|
def WMISdictQUBO_3(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__ * 2
|
|
|
|
return quboInstance
|
|
|
|
def WMISdictQUBO_4(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__ * 2
|
|
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)
|
|
|