QIRO MaxSat#

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.

Replacement routine#

The replacements work based on the problem encoding. We look throw out clauses, based on the truth value assigments as those are what is described by the qubits. Based on the maximum absolute entry of the correlation matrix M and its sign, one of the following replacements is employed:

If \(\text{M}_{ii} \geq 0\) is the maximum absolute value, then the \(i\)-th value is set to be true. In turn, we can remove all clauses that negate that value.
If \(\text{M}_{ii} < 0\) is the maximum absolute value we remove \(i\)-th value is set to be false and we will exclude clause that include that value.
If \(\text{M}_{ij} > 0, (i, j) ∈ E\) was selected, we transfer this correlation to the clauses, by replacing the first item with the second one.
If \(\text{M}_{ij} < 0, (i, j) ∈ E\) was selected, we transfer this correlation to the clauses, by replacing the first item with the negation of the second one.

create_maxSat_replacement_routine(res, oldproblem, solutions, exclusions)[source]#

Creates a replacement routine for the problem structure, i.e. defines the replacement rules. See the original paper for description of the update rules

Parameters:

resdict: Result dictionary of initial QAOA optimization procedure.
oldproblemList: The clauses defining the problem instance.
solutionsList: Qubits which have been found to be positive correlated, i.e. part of the problem solution.
exclusionsList: Qubits which have been found to be negative correlated, i.e. not part of the problem solution, or contradict solution qubits in accordance to the update rules.

Returns:

new_problem: list: Updated clauses of the problem instance.
solutionsList: Updated set of solutions to the problem.
signInt: The sign of the correlation.
exclusionsList: Updated set of exclusions to the problem.

QIRO Cost operator#

create_maxSat_cost_operator_reduced(problem, solutions=[])[source]#

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

Adjusted for QIRO to also respect found solutions to the problem

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
solutionsList: Variables that were found to be a part of the solution.
Returns
——-
cost_operatorfunction: the Operator applied to the circuit-QuantumVariable

Examples

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

Explanation: 
First entry of tuple is the number of variables, second is the clauses
Clause [1, 2, -4] is fulfilled by the QuantumStates “1100”, “1110” 

if the sign is positive : the index has of the QuantumVariable 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 is problematic.
we want to keep the mathematical formulation, so no handing over strings!

Full Example implementation:#

# imports
from qrisp.qaoa.problems.maxSatInfrastr import maxSatclCostfct, clausesdecoder
from qrisp.qiro import QIROProblem, qiro_init_function, qiro_RXMixer, create_maxSat_replacement_routine, create_maxSat_cost_operator_reduced
from qrisp import QuantumVariable
import matplotlib.pyplot as plt
import networkx as nx

# define the problem according to maxSat encoding
problem = [8 , [[1,2,-3],[1,4,-6], [4,5,6],[1,3,-4],[2,4,5],[1,3,5],[-2,-3,6], [1,7,8], [3,-7,-8], [3,4,8],[4,5,8], [1,2,7]]]
decodedClauses = clausesdecoder( problem)

qarg = QuantumVariable(problem[0])


# assign cost_function and maxclique_instance, normal QAOA
testCostFun = maxSatclCostfct(problem)

# assign the correct new update functions for qiro from above imports
qiro_instance = QIROProblem(problem = problem,
                            replacement_routine = create_maxSat_replacement_routine,
                            cost_operator = create_maxSat_cost_operator_reduced,
                            mixer = qiro_RXMixer,
                            cl_cost_function = maxSatclCostfct,
                            init_function = qiro_init_function
                            )


# We run the qiro instance and get the results!
res_qiro = qiro_instance.run_qiro(qarg=qarg, depth = 3, n_recursions = 2,
                                #mes_kwargs = mes_kwargs
                                )

print("QIRO 5 best results")
maxfive = sorted(res_qiro, key=res_qiro.get, reverse=True)[:5]
for key, val in res_qiro.items():
    if key in maxfive:

        print(key)
        print(testCostFun({key:1}))

# or compare it with the networkx result of the max_clique algorithm...
# or a write brute force solution, this is up to you

# and finally, we print the final clauses!
final_clauses = qiro_instance.problem
print(final_clauses)