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 NN logical variables x1,x2,…,xNx1,x2,…,xN, the logical disjunction (or) of these and some of their negations ¯x1,¯x2,…,¯xN¯x1,¯x2,…,¯xN is called clause. For example, the following is a typical clause.
x1∨¯x2∨x3x1∨¯x2∨x3
The 3-SAT problem is to determine whether, given several clauses consisting of three literals (e.g. xixi or ¯xi¯xi), you can assign 00 or 11 to each of x1,x2,…,xNx1,x2,…,xN so that all clauses have the value 11. For example,
(x1∨¯x2∨x3)∧(x2∨¯x3∨x4)∧(¯x1∨¯x2∨¯x4)∧(x2∨x3∨x4)(x1∨¯x2∨x3)∧(x2∨¯x3∨x4)∧(¯x1∨¯x2∨¯x4)∧(x2∨x3∨x4)
is a 3-SAT problem, and if you assign x1=1x1=1, x2=1x2=1, x3=1x3=1, and x4=0x4=0, all four clauses are 11.
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.
(x1∨¯x2∨x3)∧(x2∨¯x3∨x4)∧(¯x1∨¯x2∨¯x4)∧(x2∨x3∨x4).(x1∨¯x2∨x3)∧(x2∨¯x3∨x4)∧(¯x1∨¯x2∨¯x4)∧(x2∨x3∨x4).
In the code, the logical variables x1,x2,…,xNx1,x2,…,xN are represented by the indices 1,2,…,N1,2,…,N and their negations ¯x1,¯x2,…,¯xN¯x1,¯x2,…,¯xN by the corresponding negative numbers −1,−2,…,−N−1,−2,…,−N. Clauses are represented as literal tuples and 3-SAT problems are represented by a list of clauses as follows.
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 NN, and the number of clauses is MM. In the present problem setup described above, N=4N=4, M=4M=4.
Formulation guidelines¶
First, we prepare 3×M3×M binary variables qq and map them to each literal that appears in each clause. That is, qi,jqi,j corresponds to the jj-th literal appearing in the ii-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 xixi and its negation ¯xi¯xi do not appear in the MM literals you have marked?
Marked example: (x1∨¯x2∨x3)∧(x2∨¯x3∨x4)∧(¯x1∨¯x2∨¯x4)∧(x2∨x3∨x4)Marked example: (x1∨¯x2∨x3)∧(x2∨¯x3∨x4)∧(¯x1∨¯x2∨¯x4)∧(x2∨x3∨x4)
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,…,Ni=1,2,…,N, find the literal marked in the solution of (Problem ☆) that is xixi or ¯xi¯xi (there may be more than one such literal but from the conditions of (Problem ☆), xixi and ¯xi¯xi are never marked at the same time). When xixi is marked, xi=1xi=1, and when ¯xi¯xi is marked, xi=0xi=0. If no xixi or ¯xi¯xi is marked, xixi can be either 00 or 11.
It is easy to see that the logical variable xx 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 11 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×M3×M binary variables qq correspond to each literal, and let the binary variables indicate whether the corresponding literal is marked. If it is marked, it is 11; if not, it is 00.
For example, if the literal enclosed by the square in the following equation is marked, qq is as in the following table.
(x1∨¯x2∨x3)∧(x2∨¯x3∨x4)∧(¯x1∨¯x2∨¯x4)∧(x2∨x3∨x4)(x1∨¯x2∨x3)∧(x2∨¯x3∨x4)∧(¯x1∨¯x2∨¯x4)∧(x2∨x3∨x4)
qi,jqi,j | 1st literal | 2nd literal | 3rd literal |
---|---|---|---|
1st clause | 1 | 0 | 0 |
2nd clause | 1 | 0 | 0 |
3rd clause | 0 | 0 | 1 |
4th clause | 1 | 0 | 0 |
Also, restoring the solution of the 3-SAT problem from this qq yields x1=1x1=1, x2=1x2=1, and x4=0x4=0 (see above Derivation of the 3-SAT problem). The restoration method is, as mentioned above, xi=1xi=1 when xixi is marked, xi=0xi=0 when ¯xi¯xi is marked, and xixi can be either 00 or 11 when neither xixi nor ¯xi¯xi is marked (that is, x3x3 can be either 00 or 11).
Objective function¶
(Problem ☆) is a problem to find one way to mark MM literals that satisfy the condition, so we do not conder objective function.
Constraints¶
For the marking corresponding to qq to be the solution of (Problem ☆), the following conditions must be satisfied.
- Condition 1: For each clause, exactly one of the binary variables is 11 (one of the literals appearing in the clause is marked).
- Condition 2: For each ii, the binary variable corresponding to xixi and the binary variable corresponding to ¯xi¯xi are never both 11.
Condition 1 is a one-hot constraint on each row of qq, and we can express this condition as follows.
N−1∑k=0qi,k=1fori∈{0,1,…,M−1}N−1∑k=0qi,k=1fori∈{0,1,…,M−1}
We can express condition 2 as follows.
qi,kqj,l=0qi,kqj,l=0
Here, in the above equation, (i,j,k,l)(i,j,k,l) is the index such that the literal corresponding to qi,kqi,k is the negation of the literal corresponding to qj,lqj,l.
Implementation¶
Using the problem and formulation described above, let us implement and solve the 3-SAT problem.
First,
create a binary variable matrix qq of 3×M3×M using BinarySymbolGenerator
in
Fixstars
Amplify SDK.
from amplify import VariableGenerator
M = len(problem) # Number of clauses
gen = VariableGenerator()
q = gen.array("Binary", shape=(M, 3))
Next, we create the constraint corresponding to Condition 1. As mentioned, Condition 1 is a one-hot
constraint for each row of qq, and can be implemented by passing 1 to the axis
parameter
of
the one_hot
function.
from amplify import one_hot
constraint1 = one_hot(q, axis=1)
Then, let us create the constraint corresponding to Condition 2. Condition 2 is the condition that
the
element of qq corresponding to xixi and the element of qq corresponding to ¯xi¯xi must not
both be
11. The literal corresponding to qi,kqi,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.
from amplify import equal_to, sum as amplify_sum
constraint2 = amplify_sum(
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 an optimization model.
from amplify import Model
model = Model(constraint1 + constraint2)
Configure the client and execute the solver on the Fixstars Amplify Annealing Engine (AE).
from amplify import FixstarsClient, solve
from datetime import timedelta
client = FixstarsClient()
# client.token = "xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx" # If you use Amplify in a local environment or Google Colaboratory, enter your Amplify API token.
client.parameters.timeout = timedelta(milliseconds=1000) # timeout is 1000 ms
# Solve the problem
result = solve(model, client)
Since Amplify SDK 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.
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.
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.evaluate(
result.best.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:])