BV_{[n]}-Solvability

Another NP-hard Problem

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

The Problem BV_{[n]}-Solvability

Consider the theory of bitvectors with variable size and the operation . ⊗. (composition). A bitvector variable is denoted to be of the type bvec_{[n]}, where n is either a nonzero cardinal or a variable. The theory contains constants of arbitrary but fixed length m, further denoted as 0_{[m]} and 1_{[m]}. Let t_{1} and t_{2} be terms in this theory. The problem to decide whether the there exists a sollution of the equation t_{1} = t_{2} is called BV_{[n]}-Solvability.

Claim BV_{[n]}-Solvability is NP-hard.

Proof: (Reduction 3-CNF-SAT ≤_{m} BV_{[n]}-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 two bitvector variables a^{(i)} : bvec_{[p_{i}]} and b^{(i)} : bvec_{[q_{i}]} of unknown size. Also we need m pairs of variables c^{(j)} : bvec_{[r_{j}]}, d^{(j)} : bvec[s_{j}] for padding.

Let  φ_{i}  := 1_{[1]} ⊗ a^{(i)} ⊗ b^{(i)}  ∀i ∈ {1, ..., n}
ψ_{j}  := 1_{[1]} ⊗ c^{(j)} ⊗ d^{(j)}  ∀j ∈ {1, ..., m}
\begin{matrix}g(x_{i}) \\ g(\overline{x_{i}}) \end{matrix}  {:= \atop :=}  \begin{matrix}a^{(i)} \\ b^{(i)} \end{matrix}  \}  ∀i ∈ \{1, ..., n\}
G_{j}  := g(L_{j1}) ⊗ g(L_{j2}) ⊗ g(L_{j3}) ⊗ c^{(j)}  ∀j ∈ {1, ..., m}
Ψ  := a^{(p_{1})} ⊗ .. ⊗ a^{(p_{n})} ⊗ b^{(q_{1})} ⊗ .. ⊗ b^{(q_{n})} ⊗ c^{(r_{1})} ⊗ .. ⊗ c^{(r_{m})} ⊗ d^{(s_{1})} ⊗ .. ⊗ d^{(s_{m})}

Now define the reduction f as follows:

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

This equation is solvable, if (and only if) Ψ equals a composition of 0-valued bitvectors, because the 0_{[1]} is propagated to every cell of Ψ. Therefore each sum p_{i} + q_{i} must equal 3 and each sum r_{j} + s_{j} must equal 4. One bitvector of the pair a^{(i)}, b^{(i)} has the length 2, the other one is of the length 1. Consider x_{i} = true equivalent to ||a^{(i)}|| = 2 (and x_{i} = false equivalent to ||a^{(i)}|| = 1). For there are no zero length bitvectors allowed, each ||c^{(j)}|| can be chosen between 1 and 3. Every G_{j} has to reach the length 7, this is equivalent to the notion that in each disjunction of the 3-CNF-formula F at least one literal evaluates to true.

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

Q.E.D

Remark:

The question if BV_{[n]}-Solvability ∈^{?} NP is still open. There seems to be no hint that for every solvable equation exists a polynomial sized (in the input, that is) sollution.