LibraryReExportIsNPComplete

From APIDesign

Revision as of 09:40, 25 May 2008

This page describes a way to convert any wikipedia::3SAT problem to a solution of finding the right configuration from conflicting libraries in a system that can re-export APIs. Thus proving that the later problem is wikipedia::NP-complete.

wikipedia::3SAT

The problem of satisfying a logic formula remains NP-complete even if all expressions are written in wikipedia::conjunctive normal form with 3 variables per clause (3-CNF), yielding the 3SAT problem. This means the expression has the form:

Failed to parse (Can't write to or create math temp directory): (x_{11} \wedge x_{12} \wedge x_{13}) \vee

Failed to parse (Can't write to or create math temp directory): (x_{21} \wedge x_{22} \wedge x_{23}) \vee

Failed to parse (Can't write to or create math temp directory): (x_{31} \wedge x_{32} \wedge x_{33}) \vee

Failed to parse (Can't write to or create math temp directory): ...

Failed to parse (Can't write to or create math temp directory): (x_{n1} \wedge x_{n2} \wedge x_{n3})

where each Failed to parse (Can't write to or create math temp directory): x_{ab}

is a variable Failed to parse (Can't write to or create math temp directory): v_i
or a negation of a variable Failed to parse (Can't write to or create math temp directory): \neg v_i

. Each variable Failed to parse (Can't write to or create math temp directory): v_i

can appear multiple times in the expression.

Module Dependencies Problem

Let Failed to parse (Can't write to or create math temp directory): A, B, C, ...

denote an API.

Let Failed to parse (Can't write to or create math temp directory): A_1, A_{1.1}, A_{1.7}, A_{1.11}

denote compatible versions of API Failed to parse (Can't write to or create math temp directory): A

.

Let Failed to parse (Can't write to or create math temp directory): A_1, A_{2.0}, A_{3.1}

denote incompatible versions of API Failed to parse (Can't write to or create math temp directory): A

.

Let Failed to parse (Can't write to or create math temp directory): A_{x.y} \rightarrow B_{u.v}

denote the fact that version x.y of API A depends on version u.v of API B.

Let Failed to parse (Can't write to or create math temp directory): A_{x.y} \leadsto B_{u.v}

denote the fact that version x.y of API A depends on version u.v of API B and that B re-exports its elements.

Let Repository Failed to parse (Can't write to or create math temp directory): R=(M,D)

be any set of modules with their various versions and their dependencies on other modules with or without re-export.

Let C be a Configuration in a repository Failed to parse (Can't write to or create math temp directory): R=(M,D) , if Failed to parse (Can't write to or create math temp directory): C \subseteq M , where following conditions are satisfied:

Failed to parse (Can't write to or create math temp directory): A_{x.y} \in C \vee A_{u.v} \in C \Rightarrow x = u \vee y = v

Let Failed to parse (Can't write to or create math temp directory): Dep_R(A_{x.y})

be set of all modules in repository Failed to parse (Can't write to or create math temp directory): R
that M depends on directly. E.g. 

Failed to parse (Can't write to or create math temp directory): Dep_R(A_{x.y}) = { B_{u.v} : A_{x.y} \rightarrow B_{u.v} \wedge A_{x.y} \rightarrow B_{u.v} } .

Let say that a repository is Executable if there exists as subset of the set of modules from the repository, where each module is present in only one version and dependencies of a modules are satisfied in the subset and no module sees any class exported by a module twice.

Converstion of wikipedia::3SAT to Module Dependencies Problem

Let (x_a or ¬x_b or ¬x_c) and (x_a or x_b or x_d) be a formula. For each variable x_a let's create two modules with incompatible version A₁ and A₂ and put them into the repository of modules.

For each formula let's create a module F that will have three compatible versions. Each of them will depend on one variable. In case the variable is used with negation, it will depend on version 2, otherwise on version 1. So for the formula (x_a or ¬x_b or ¬x_c) we will get: F_1.1[^A₁] and F_1.2[^B₂] and F_1.3[^C₂]

Now we will create a module M that depends all formulas: M[F_1.0, G_1.0, ...]. The claim is that iff there is a way to satisfy all dependencies of module M, then there is a solution to the wikipedia::3SAT formula.