Example NP problems published in A. Lucas, Front. Phys. (2014) - Satisfiability problem (SAT)¶

This example code implements the satisfiability problem (SAT) introduced in the paper A. Lucas, "Ising formulations of many NP problems", Front. Phys. (2014) using Fixstars Amplify. Other NP-complete and NP-hard problems introduced in the same paper are also discussed below (the corresponding sections in the paper are shown in the brackets).

Graph partitioning problem (Sec. 2.2).
Maximum clique problem (Sec. 2.3)
Exact cover problem (Sec. 4.1)
Set packing problem (Sec. 4.2)
Minimum vertex cover problem (Sec. 4.3)
Satisfiability problem (SAT) (Sec. 4.4)
Minimal maximal matching problem (Sec. 4.5)
Graph coloring problem (Sec. 6.1)
Clique cover problem (Sec. 6.2)
Job sequencing problem with integer lengths (Sec. 6.3)
Hamiltonian cycle problem (Sec. 7.1)
Directed feedback vertex set problem (Sec. 8.3)
Minimum feedback edge set problem (Sec. 8.5)
Graph isomorphism problem (Sec. 9)

3-SAT problem¶

For $N$ logical variables $x_1, x_2, \ldots, x_N$, the logical disjunction (or) of these and some of their negations $\bar{x_1}, \bar{x_2}, \ldots, \bar{x_N}$ is called clause. For example, the following is a typical clause.

$$ x_1 \lor \bar{x_2} \lor x_3 $$

The 3-SAT problem is to determine whether, given several clauses consisting of three literals (e.g. $x_i$ or $\bar{x_i}$), you can assign $0$ or $1$ to each of $x_1, x_2, \ldots, x_N$ so that all clauses have the value $1$. For example,

$$ (x_1 \lor \bar{x_2} \lor x_3) \land (x_2 \lor \bar{x_3} \lor x_4) \land (\bar{x_1} \lor \bar{x_2} \lor \bar{x_4}) \land (x_2 \lor x_3 \lor x_4) $$

is a 3-SAT problem, and if you assign $x_1 = 1$, $x_2 = 1$, $x_3 = 1$, and $x_4 = 0$, all four clauses are $1$.

Here, we will create a program that uses Fixstars Amplify to search for a solution to the 3-SAT problem. The formulation follows the one in Sec. 4.4 of A. Lucas, Front. Phys. (2014).

Problem definition¶

In this example program, we solve the following 3-SAT problem.

$$ (x_1 \lor \bar{x_2} \lor x_3) \land (x_2 \lor \bar{x_3} \lor x_4) \land (\bar{x_1} \lor \bar{x_2} \lor \bar{x_4}) \land (x_2 \lor x_3 \lor x_4). $$

In the code, the logical variables $x_1, x_2, \ldots, x_N$ are represented by the indices $1, 2, \ldots, N$ and their negations $\bar{x_1}, \bar{x_2}, \ldots, \bar{x_N}$ by the corresponding negative numbers $-1, -2, \ldots, -N$. Clauses are represented as literal tuples and 3-SAT problems are represented by a list of clauses as follows.

In [ ]:

N = 4  # Number of logical variables
problem = [(1, -2, 3), (2, -3, 4), (-1, -2, -4), (2, 3, 4)]

Formulation¶

Hereafter, the number of logical variables is $N$, and the number of clauses is $M$. In the present problem setup described above, $N=4$, $M=4$.

Formulation guidelines¶

First, we prepare $3 \times M$ binary variables $q$ and map them to each literal that appears in each clause. That is, $q_{i, j}$ corresponds to the $j$-th literal appearing in the $i$-th clause.

Here, the immediate idea is to map literals and binary variables to each other, but formulating in this way will eventually lead to the use of inequality constraints, which require auxiliary variables. The use of auxiliary variables is not necessarily a bad thing. Still it is better not to use them if possible, so we will consider formulating the problem differently.

Now, let us consider the following problem:

(Problem ☆) : For each clause of the 3-SAT problem, mark only one literal that appears in the clause (see the following logical formula). Can you do so so that a logical variable $x_i$ and its negation $\bar{x_i}$ do not appear in the $M$ literals you have marked?

$$ \text{Marked example: }\:\:(\boxed{x_1} \lor \bar{x_2} \lor x_3) \land (\boxed{x_2} \lor \bar{x_3} \lor x_4) \land (\bar{x_1} \lor \bar{x_2} \lor \boxed{\bar{x_4}}) \land (\boxed{x_2} \lor x_3 \lor x_4) $$

If we can solve this (problem ☆), then we can solve the 3-SAT problem as well because the solution to the 3-SAT problem can be derived from the solution to (Problem ☆) as follows:

Derivation of the 3-SAT problem.
For each of $i = 1, 2, \ldots, N$, find the literal marked in the solution of (Problem ☆) that is $x_i$ or $\bar{x_i}$ (there may be more than one such literal but from the conditions of (Problem ☆), $x_i$ and $\bar{x_i }$ are never marked at the same time). When $x_i$ is marked, $x_i = 1$, and when $\bar{x_i }$ is marked, $x_i = 0$. If no $x_i$ or $\bar{x_i}$ is marked, $x_i$ can be either $0$ or $1$.

It is easy to see that the logical variable $x$ determined in this way is a solution to the 3-SAT problem. Also, if there is a solution to the 3-SAT problem, we can construct a solution to (problem ☆) by marking one literal in each clause that is equal to $1$ in the solution. Thus, we know that it cannot happen that there is no solution to (problem ☆) even though there is a solution to the 3-SAT problem.

Therefore, we can solve (Problem ☆) instead of the 3-SAT problem.

Now let us formulate (Problem ☆). Let $3 \times M$ binary variables $q$ correspond to each literal, and let the binary variables indicate whether the corresponding literal is marked. If it is marked, it is $1$; if not, it is $0$.

For example, if the literal enclosed by the square in the following equation is marked, $q$ is as in the following table.

$$ (\boxed{x_1} \lor \bar{x_2} \lor x_3) \land (\boxed{x_2} \lor \bar{x_3} \lor x_4) \land (\bar{x_1} \lor \bar{x_2} \lor \boxed{\bar{x_4}}) \land (\boxed{x_2} \lor x_3 \lor x_4) $$

$q_{i,j}$	1st literal	3rd literal
1st clause	1	0
2nd clause	1	0
3rd clause	0	1
4th clause	1	0

Also, restoring the solution of the 3-SAT problem from this $q$ yields $x_1 = 1$, $x_2 = 1$, and $x_4 = 0$ (see above Derivation of the 3-SAT problem). The restoration method is, as mentioned above, $x_i = 1$ when $x_i$ is marked, $x_i = 0$ when $\bar{x_i}$ is marked, and $x_i$ can be either $0$ or $1$ when neither $x_i$ nor $\bar{x_i}$ is marked (that is, $x _3$ can be either $0$ or $1$).

Objective function¶

(Problem ☆) is a problem to find one way to mark $M$ literals that satisfy the condition, so we do not conder objective function.

Constraints¶

For the marking corresponding to $q$ to be the solution of (Problem ☆), the following conditions must be satisfied.

Condition 1: For each clause, exactly one of the binary variables is $1$ (one of the literals appearing in the clause is marked).
Condition 2: For each $i$, the binary variable corresponding to $x_i$ and the binary variable corresponding to $\bar{x_i}$ are never both $1$.

Condition 1 is a one-hot constraint on each row of $q$, and we can express this condition as follows.

$$ \sum_{k = 0}^{N-1} q_{i, k} = 1 \quad \text{for} \quad i \in \{0, 1, \ldots, M-1\} $$

We can express condition 2 as follows.

$$ q_{i, k} q_{j, l} = 0 $$

Here, in the above equation, $(i, j, k, l)$ is the index such that the literal corresponding to $q_{i, k}$ is the negation of the literal corresponding to $q_{j, l}$.

Implementation¶

Using the problem and formulation described above, let us implement and solve the 3-SAT problem. First, create a binary variable matrix $q$ of $3\times M$ using BinarySymbolGenerator in Fixstars Amplify SDK.

In [ ]:

from amplify import BinarySymbolGenerator

M = len(problem)  # Number of clauses

gen = BinarySymbolGenerator()
q = gen.array(M, 3)

Next, we create the constraint corresponding to Condition 1. As mentioned, Condition 1 is a one-hot constraint for each row of $q$.

In [ ]:

from amplify.constraint import one_hot

constraint1 = [one_hot(q[i]) for i in range(M)]

Then, let us create the constraint corresponding to Condition 2. Condition 2 is the condition that the element of $q$ corresponding to $x_i$ and the element of $q$ corresponding to $\bar{x_i}$ must not both be $1$. The literal corresponding to $q_{i, k}$ can be obtained by problem[i][k], whose absolute value represents the index of the logical variable and whose sign indicates whether it is negative. Thus, whether two literals are negative to each other is identical to whether the two elements of problem add up to $0$.

In [ ]:

from amplify.constraint import equal_to

constraint2 = [
    equal_to(q[i, k] * q[j, l], 0)
    for i in range(M)
    for k in range(3)
    for j in range(M)
    for l in range(3)
    if problem[i][k] + problem[j][l] == 0
]

Now, we can convert the constructed constraints into a logical model.

In [ ]:

from amplify import BinaryQuadraticModel

model = BinaryQuadraticModel(sum(constraint1) + sum(constraint2))

Configure the client and execute the solver on the Fixstars Amplify Annealing Engine (AE).

In [ ]:

from amplify.client import FixstarsClient
from amplify import Solver

client = FixstarsClient()
# client.token = "xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx"  # If you use Amplify in a local environment or Google Colaboratory, enter your Amplify API token.
client.parameters.timeout = 1000

# Define and execute the solver
solver = Solver(client)
result = solver.solve(model)

Since Solver automatically filters the solutions that satisfy the constraints, if the result is not empty, you know that there is a solution that satisfies the constraints.

In [ ]:

if len(result) == 0:
    print("No solution has been found.")
else:
    print("A solution has been found.")

Finally, convert the solution of (Problem ☆) into the solution of the 3-SAT problem.

In [ ]:

import numpy as np

x = np.zeros(
    N + 1
)  # Default solution values for the 3-SAT problem. Since x is 1-origin, we define x to have (N+1) size
values = q.decode(
    result[0].values
)  # Format the solution to have the same shape as the decision variable matrix by the decode method
ones = np.argwhere(values == 1)  # Search all elements of q which are 1
for i, k in ones:
    if problem[i][k] > 0:
        x[problem[i][k]] = 1
print(x[1:])