BVEVE-Solvability

Just another NP-complete Problem

Oliver Möller Septemer, 12th 1996 SRI, Menlo Park, CA

The Problem BVEVE-Solvability

Consider the theory of bitvectors with fixed (finite nonzero) size and the operations . ⊗. (composition) and .ˆ (i,j) (extraction). i and j are allowed to be cardinal variables. Also, there exist constants of arbitrary but fixed length n, further denoted as 0_{[n]} and 1_{[n]}. Let t_{1} and t_{2} be terms over such bitvectors. The problem to decide whether the there exists a sollution to the equation t_{1} = t_{2} is called BVEVE-Solvability (BitVector Equation with Variables in Extraction Solvability).

Claim

BVEVE-Solvability is NP-complete.

Proof:

a) BVEVE-Solvability ∈ NP

One can guess a polynomial-sized sollution (t.i. polynomial in the term-length and the maximum length of the used bitvector variables) and check if the equation holds.

b) BVVE-SAT is NP-hard (Reduction 3-CNF-SAT ≤_{m} BVEVE-Solvability)

Let F = (L_{11} ∨ L_{12} ∨ L_{13}) ∧ ... ∧ (L_{m1} ∨ L_{m2} ∨ L_{m3}) be a boolean formula in 3-CNF over variables x_{i} ∈ V ar = \{x_{1}, ..., x_{n}\}. L_{ij} are literals in V ar ∪ \overline{V ar}, (i ∈ \{1, ..., m\}, j ∈ \{1, 2, 3\}). For each x_{i} ∈ V ar introduce a bitvector variable a_{i} of length 3 and integer-variables r_{i}, s_{i}. Additionally, we need m bitvector variables b_{j} of length 3 and and integer variables t_{j} for padding.

Let φ_{i} := (a_{i}ˆ (2, r_{i})) ⊗ (a_{i}ˆ (s_{i}, 0))
g(x_{i}) := a_{i}ˆ (s_{i}, 0)  }∀i ∈ {1, ..., n}
g(\overline{x_{i}}) := a_{i}ˆ (2, r_{i})
G_{j} := g(L_{j1}) ⊗ g(L_{j2}) ⊗ g(L_{j3}) ⊗ (b_{j}ˆ (t_{j}, 0)) ∀j ∈ {1, ..., m}

Now define the reduction f as follows:

f(F) := \{ \begin{matrix}a_{1} ⊗ ... ⊗ a_{n} & ⊗ & b_{1} ⊗ ... ⊗ b_{m} & ⊗ & φ_{1} ⊗ ... ⊗ φ_{n} & ⊗ & 1_{[1]} ⊗ G_{1} ⊗ 1_{[1]} ⊗ ... ⊗ 1_{[1]} ⊗ G_{m} \\ 0_{[3]} ⊗ ... ⊗ 0_{[3]} & ⊗ & 0_{[3]} ⊗ ... ⊗ 0_{[3]} & ⊗ & 0_{[3]} ⊗ ... ⊗ 0_{[3]} & ⊗ & 1_{[1]} ⊗ 0_{[7]} ⊗ 1_{[1]} ⊗ ... ⊗ 1_{[1]} ⊗ 0_{[7]} \end{matrix} =^{!}

The equation f(F) is solvable, if (and only if) all variables a_{i} and b_{i} equal 0-valued bitvectors; that means also, that each φ_{i} has to be of the length 3 to match the {1_{[1]} \atop 1_{[1]}} -position. This can only be achieved if r_{i} = s_{i} +1 for each i, thus r_{i} ∈ {1, 2}. Consider x_{i} = true equivalent to r_{i} = 1 (and x_{i} = false equivalent to r_{i} = 2). In order to match the lower term, each G_{j} has to be of the length 7. The length of b_{j}ˆ (t_{j}, 0) is in {1, 2, 3}, thus at least one of the g(L_{ij}) in each clause has to be of the length two. This is equivalent to the notion that one of the literals L_{ij} evalueates to true.

Thus, F is satisfiable ⇔ there exists a mapping α : V ar → {true, false} with α(F) = true ⇔ there exists a mapping β : {r_{i}, s_{i}, t_{j}|i = 1, .., n; j = 1, .., m} → N such that f(F) is solvable.

Q.E.D