QIRO MaxSat#

Problem description#

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

For example, for $l=3$ and $n=5$ Boolean variables $x_1,\dotsc,x_5$ consider the clauses

$$(x_1\lor x_2\lor x_3), (\bar x_1\lor x_2\lor x_4), (\bar x_2\lor x_3\lor \bar x_5), (\bar x_3\lor x_4\lor x_5)$$

where $\bar x_i$ denotes the negation of $x_i$. What is sought now is an assignment of the variables with 0 (False) or 1 (True) that maximizes the number of satisfied clauses. In this case, the assignment $x=x_1x_2x_3x_4x_5=01111$ satisfies all clauses.

Given $n$ variables $x_1,\dotsc,x_n$ we represent each clause as a list of integers such that the absolute values correspond to the indices of the variables and a minus sign corresponds to negation of the variable. For example, the above clauses correspond to

$$[1,2,3],\quad [-1,2,4],\quad [-2,3,-5],\quad [-3,4,5]$$

The cost function for the maximum satisfyability problem is given by

$$C(x)=\sum_{\alpha=1}^mC_{\alpha}(x)$$

where for each clause $C_{\alpha}(x)=1$ if the corresponding clause is satisfied and $C_{\alpha}(x)=0$ otherwise. Here,

$$C_{\alpha}(x)=1-\prod_{j>0}(1-x_j)\prod_{j<0}x_{-j}$$

Replacement routine#

The replacements work based on the problem encoding. We discard clauses, based on the truth value assignments 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, problem, solutions, exclusions)[source]#

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

Parameters:

resdict: Result dictionary of QAOA optimization procedure.
problemtuple(int, list[list[int]]): The number of variables and a list of clauses for the MaxSat instance.
solutionslist: Qubits which were found to be positively correlated, i.e., part of the problem solution.
exclusionslist: Qubits which were found to be negatively correlated, i.e., not part of the problem solution, or contradict solution qubits in accordance with 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]#

Creates the cost_operator for the problem instance. This operator is adjusted to consider qubits that were found to be a part of the problem solution.

Parameters:

problemtuple(int, list[list[int]]): The number of variables and a list of clauses for the MaxSat instance.
solutionslist: Variables that were found to be a part of the solution.

Returns:

cost_operatorfunction: A function receiving a QuantumVariable and a real parameter $\gamma$. This function performs the application of the cost operator.

Example implementation#

from qrisp import QuantumVariable
from qrisp.qaoa import create_maxsat_cl_cost_function
from qrisp.qiro import QIROProblem, qiro_init_function, qiro_RXMixer, create_maxsat_replacement_routine, create_maxsat_cost_operator_reduced

clauses = [[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]]
num_vars = 8
problem = (num_vars, clauses)
qarg = QuantumVariable(num_vars)

qiro_instance = QIROProblem(problem = problem,
                            replacement_routine = create_maxsat_replacement_routine,
                            cost_operator = create_maxsat_cost_operator_reduced,
                            mixer = qiro_RXMixer,
                            cl_cost_function = create_maxsat_cl_cost_function,
                            init_function = qiro_init_function
                            )
res_qiro = qiro_instance.run_qiro(qarg=qarg, depth = 3, n_recursions = 2)

That’s it! In the following, we print the 5 most likely solutions together with their cost values, and the final clauses.

cl_cost = create_maxsat_cl_cost_function(problem)

print("5 most likely QIRO solutions")
max_five_qiro = sorted(res_qiro, key=res_qiro.get, reverse=True)[:5]
for res in max_five_qiro:
    print(res)
    print(cl_cost({res : 1}))

final_clauses = qiro_instance.problem
print("final clauses")
print(final_clauses)