QAOA 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}$$

Cost operator#

create_maxsat_cost_operator(problem)[source]#

Creates the cost operator for an instance of the maximum satisfiability problem. For a given cost function

\[C(x) = \sum_{\alpha=1}^m C_{\alpha}(x)\]

the cost operator is given by $e^{-i\gamma C}$ where $C=\sum_x C(x)\ket{x}\bra{x}$.

Parameters:

problemtuple(int, list[list[int]]): The number of variables, and the clauses of the maximum satisfiability problem instance.

Returns:

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

Classical cost function#

create_maxsat_cl_cost_function(problem)[source]#

Creates the classical cost function for an instance of the maximum satisfiability problem.

Parameters:

problemtuple(int, list[list[int]]): The number of variables, and the clauses of the maximum satisfiability problem instance.

Returns:

cl_cost_functionfunction: The classical cost function for the problem instance, which takes a dictionary of measurement results as input.

Helper functions#

create_maxsat_cost_polynomials(problem)[source]#

Creates a list of polynomials representing the cost function for each clause, and a list of symbols.

Parameters:

problemtuple(int, list[list[int]]): The number of variables, and the clauses of the maximum satisfiability problem instance.

Returns:

cost_polynomialslist[sympy.Expr]: A list of the cost functions for each clause as SymPy polynomials.
symbolslist[sympy.Symbol]: A list of SymPy symbols.

MaxSat problem#

maxsat_problem(problem)[source]#

Creates a QAOA problem instance with appropriate phase separator, mixer, and classical cost function.

Parameters:

problemtuple(int, list[list[int]]): The number of variables, and the clauses of the maximum satisfiability problem instance.

Returns:

QAOAProblem: A QAOA problem instance for MaxSat for given a problem.

Example implementation#

from qrisp import QuantumVariable
from qrisp.qaoa import QAOAProblem, RX_mixer, create_maxsat_cl_cost_function, create_maxsat_cost_operator

clauses = [[1,2,-3],[1,4,-6],[4,5,6],[1,3,-4],[2,4,5],[1,3,5],[-2,-3,6]]
num_vars = 6
problem = (num_vars, clauses)
qarg = QuantumVariable(num_vars)

qaoa_max_indep_set = QAOAProblem(cost_operator=create_maxsat_cost_operator(problem),
                                 mixer=RX_mixer,
                                 cl_cost_function=create_maxsat_cl_cost_function(problem))
results = qaoa_max_indep_set.run(qarg=qarg, depth=5)

That’s it! Feel free to experiment with the init_type='tqa' option in the .run method for improved performance. In the following, we print the 5 most likely solutions together with their cost values.

cl_cost = create_maxsat_cl_cost_function(problem)

print("5 most likely solutions")
max_five = sorted(results.items(), key=lambda item: item[1], reverse=True)[:5]
for res, prob in max_five:
   print(res, prob, cl_cost({res : 1}))