QAOA MaxSat#

Problem description#

Given $m$ disjunctive clauses over $n$ Boolean variables $x_{1}, \dots, 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}, \dots, 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_{1} x_{2} x_{3} x_{4} x_{5} = 01111$ satisfies all clauses.

Given $n$ variables $x_{1}, \dots, 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], [- 1, 2, 4], [- 2, 3, - 5], [- 3, 4, 5]$

The cost function for the maximum satisfyability problem is given by

$C (x) = \sum_{α = 1}^{m} C_{α} (x)$

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

$C_{α} (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_{α = 1}^{m} C_{α} (x)

the cost operator is given by $e^{- i γ C}$ where $C = \sum_{x} C (x) | x ⟩ ⟨ 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 $γ$ . 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}))