QAOA MaxSat problem implementation

Problem description

Given \(m\) disjunctive clauses over \(n\) Boolean variables \(x\) , where each clause contains at most \(l \geq 2\) literals, find a variable assignment that maximizes the number of satisfied clauses.

Cost operator

maxSatCostOp(clauses)

Implementation for MaxSat Cost-Operator, in accordance to the original QAOA-paper.

For each clause \(C_i\) apply \(C_i(x) = 1 - \prod_j x_j\) (replace \(x_j\) with

\((1-x_j)\) if \(x_j\) is negated). The problem operator is acquired with the substitution \(x_j = (I - Z_j)\) , where \(Z_j\) is the Pauli- \(Z\) operator applied to the \(j\) -th qubit.

Parameters

clausesList(Lists)

Clauses to be considered for MaxSat. Should be given as a list of lists and 1-indexed instead 0-indexed, see example

Returns

QuantumCircuit: qrisp.QuantumCircuit

the Operator applied to the circuit-QuantumVariable

Examples

>>> clauses11 = [[1,2,-3], [1,4,-6], [4,5,6], [1,3,-4], [2,4,5], [1,3,5], [-2,-3,6]]

Explanation:

Clause [1, 2, -4] is fulfilled by the QuantumStates “1100”, “1110”

• if positive sign: the index has to be “1”, if negative sign the index has to be “0”.

• indices not mentioned can be “0” or “1” (the third integer in this case).

• start with 1 in your clauses! because int 0 has no sign and this problematic.

• we want to stay with mathematical formulation, so no handing over strings!

Assign the operators

>>> cost_operator=maxSatCostOp(clauses11),
>>> mixer=RX_mixer 

Classical cost function

maxSatclCostfct(decodedClauses)

Parameters

decodedClausesIterable(tuple)

clauses as bitstrings, as returned by clausesdecoder() helper function

Returns

Costfunctionfunction

the classical function for the problem instance, which takes a dictionary of measurement results as input

Helper function

clausesdecoder(clauses, numVars)

Decodes the clause arrays to represent binary bitstrings, that fulfill the clauses –> used to calculate objective function, i.e. the classical cost function

Parameters

clausesList(List)

clauses to be considered for maxSat (! 1-indexed, instead of 0-indexed, see example above)

numVarsint

the total amount of Variables considered within the clauses

Returns

decodedClausesIterable(tuple)

clauses as bitstrings, to be compared to the QAOA-bitstring results

Examples

As above:

>>> clauses11 = [[1,2,-3], [1,4,-6], [4,5,6], [1,3,-4], [2,4,5], [1,3,5], [-2,-3,6]]
>>> decodedClauses = clausesdecoder( clauses = clauses11, numVars = 6)

Assign cost_function

>>> cl_cost_function=maxSatclCostfct(decodedClauses)

Full example implementation:

from qrisp.qaoa import QAOAProblem
from qrisp.qaoa.problems.maxSatInfrastr import maxSatclCostfct, maxSatCostOp, clausesdecoder, init_state
from qrisp.qaoa.mixers import RX_mixer
from qrisp import QuantumVariable


clauses11 = [[1,2,-3],[1,4,-6], [4,5,6],[1,3,-4],[2,4,5],[1,3,5],[-2,-3,6]]

#Clauses are decoded, s.t. the Cost-Optimizer can read them
#numVars is the amount of considered variables, i.e. highest number (= Number of Qubits in Circuit aswell)
decodedClauses = clausesdecoder( clauses = clauses11, numVars = 6)
#print(decodedClauses)

qarg = QuantumVariable(len(clauses11))

#CostOperator-Generator has to be called with the clauses
#CostFct-Generator has to be called with decodedClauses
QAOAinstance = QAOAProblem(cost_operator=maxSatCostOp(clauses11), mixer=RX_mixer, cl_cost_function=maxSatclCostfct(decodedClauses))
QAOAinstance.set_init_function(init_function=init_state)
theNiceQAOA = QAOAinstance.run(qarg=qarg, depth=5)

 #print the ideal solutions
 print("5 most likely Solutions")
 maxfive = sorted(theNiceQAOA, key=theNiceQAOA.get, reverse=True)[:5]
 for res, val in theNiceQAOA.items():
     if res in maxfive:
         print((res, val))
         print(clCostfct({res : 1}))


print("Final energy value and associated solution values")
costfct = maxSatclCostfct(decodedClauses)
print(costfct(theNiceQAOA))
#Final Result-dictionary
resDict = dict()
for index in decodedClauses:
   for index2 in index:
      if index2 in resDict.keys():
            resDict[index2] +=1
      else:
            resDict[index2] =1
print(resDict)