Difference-map Algorithm - Example: Logical Satisfiability

Example: Logical Satisfiability

Incomplete algorithms, such as stochastic local search, are widely used for finding satisfying truth assignments to boolean formulas. As an example of solving an instance of 2-SAT with the difference-map algorithm, consider the following formula (~ indicates NOT):

(q₁ or q₂) and (~q₁ or q₃) and (~q₂ or ~q₃) and (q₁ or ~q₂)

To each of the eight literals in this formula we assign one real variable in an eight dimensional Euclidean space. The structure of the 2-SAT formula can be recovered when these variables are arranged in a table:

x11	x12
(x21)		x22
	(x31)	(x32)
x41	(x42)

Rows are the clauses in the 2-SAT formula and literals corresponding to the same boolean variable are arranged in columns, with negation indicated by parentheses. For example, the real variables x₁₁, x₂₁ and x₄₁ correspond to the same boolean variable (q₁) or its negation, and are called replicas. It is convenient to associate the values 1 and -1 with TRUE and FALSE rather than the traditional 1 and 0. With this convention, the compatibility between the replicas takes the form of the following linear equations:

x₁₁ = -x₂₁ = x₄₁

x₁₂ = -x₃₁ = -x₄₂

x₂₂ = -x₃₂

The linear subspace where these equations are satisfied is one of the constraint spaces, say A, used by the difference map. To project to this constraint we replace each replica by the signed replica average, or its negative:

a₁ = (x₁₁ - x₂₁ + x₄₁) / 3

x₁₁ → a₁ x₂₁ → -a₁ x₄₁ → a₁

The second difference-map constraint applies to the rows of the table, the clauses. In a satisfying assignment, the two variables in each row must be assigned the values (1, 1), (1, -1), or (-1, 1). The corresponding constraint set, B, is thus a set of 34 = 81 points. In projecting to this constraint the following operation is applied to each row. First, the two real values are rounded to 1 or -1; then, if the outcome is (-1, -1), the larger of the two original values is replaced by 1. Examples:

(-.2, 1.2) → (-1, 1)

(-.2, -.8) → (1, -1)

It is a straightforward exercise to check that both of the projection operations described minimize the Euclidean distance between input and output values. Moreover, if the algorithm succeeds in finding a point x that lies in both constraint sets, then we know that (i) the clauses associated with x are all TRUE, and (ii) the assignments to the replicas are consistent with a truth assignment to the original boolean variables.

To run the algorithm one first generates an initial point x₀, say

-0.5	-0.8
(-0.4)		-0.6
	(0.3)	(-0.8)
0.5	(0.1)

Using β = 1, the next step is to compute P_B(x₀) :

1	-1
(1)		-1
	(1)	(-1)
1	(1)

This is followed by 2P_B(x₀) - x₀,

2.5	-1.2
(2.4)		-1.4
	(1.7)	(-1.2)
1.5	(1.9)

and then projected onto the other constraint, P_A(2P_B(x₀) - x₀) :

0.53333	-1.6
(-0.53333)		-0.1
	(1.6)	(0.1)
0.53333	(1.6)

Incrementing x₀ by the difference of the two projections gives the first iteration of the difference map, D(x₀) = x₁ :

-0.96666	-1.4
(-1.93333)		0.3
	(0.9)	(0.3)
0.03333	(0.7)

Here is the second iteration, D(x₁) = x₂ :

-0.3	-1.4
(-2.6)		-0.7
	(0.9)	(-0.7)
0.7	(0.7)

This is a fixed point: D(x₂) = x₂. The iterate is unchanged because the two projections agree. From P_B(x₂),

1	-1
(-1)		1
	(1)	(-1)
1	(1)

we can read off the satisfying truth assignment: q₁ = TRUE, q₂ = FALSE, q₃ = TRUE.