LibraryReExportIsNPComplete

From APIDesign

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.

Contents 1 wikipedia::3SAT 2 Module Dependencies Problem 3 Converstion of wikipedia::3SAT to Module Dependencies Problem 4 Proof

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} \vee x_{12} \vee x_{13}) \wedge

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

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

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} \vee x_{n2} \vee 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} > 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} \gg 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 is satisfied:

Failed to parse (Can't write to or create math temp directory): \forall A_{x.y} \in C, \forall A_{x.y} \gg B_{u.v} \in D \Rightarrow \exists w >= v \wedge B_{u.w} \in C

- each re-exported dependency is satisfied with some compatible version

Failed to parse (Can't write to or create math temp directory): \forall A_{x.y} \in C, \forall A_{x.y} > B_{u.v} \in D \Rightarrow \exists w >= v B_{u.w} \in C

- each dependency is satisfied with some compatible version

Let there be two chains of re-exported dependencies Failed to parse (Can't write to or create math temp directory): A_{p.q} \gg ... \gg B_{x.y}

and Failed to parse (Can't write to or create math temp directory): A_{p.q} \gg ... \gg B_{u.v}
then Failed to parse (Can't write to or create math temp directory): x = u \wedge y = v
- this guarantees that each class has just one, exact meaning for each importer

Module Dependency Problem: Let there be a repository Failed to parse (Can't write to or create math temp directory): R=(M,D)

and a module Failed to parse (Can't write to or create math temp directory): A \in M

. Does there exist a configuration Failed to parse (Can't write to or create math temp directory): C

in the repository Failed to parse (Can't write to or create math temp directory): R

, such that the module Failed to parse (Can't write to or create math temp directory): A \in C , e.g. the module can be enabled?

Converstion of wikipedia::3SAT to Module Dependencies Problem

Let there be wikipedia::3SAT formula with with variables Failed to parse (Can't write to or create math temp directory): v_1, ..., v_m

as defined above.

Let's create a repository of modules Failed to parse (Can't write to or create math temp directory): R . For each variable Failed to parse (Can't write to or create math temp directory): v_i

let's create two modules Failed to parse (Can't write to or create math temp directory): M^i_{1.0}
and Failed to parse (Can't write to or create math temp directory): M^i_{2.0}

, which are mutually incompatible and put them into repository Failed to parse (Can't write to or create math temp directory): R .

For each formula Failed to parse (Can't write to or create math temp directory): (x_{i1} \vee x_{i2} \vee x_{i3})

let's create a module Failed to parse (Can't write to or create math temp directory): F^i

that will have three compatible versions. Each of them will depend on one variable's module. In case the variable is used with negation, it will depend on version 2.0, otherwise on version 1.0. So for the formula 

Failed to parse (Can't write to or create math temp directory): v_a \vee \neg v_b \vee \neg v_c

we will get:

Failed to parse (Can't write to or create math temp directory): F^i_{1.1} \gg M^a_{1.0}

Failed to parse (Can't write to or create math temp directory): F^i_{1.2} \gg M^b_{2.0}

Failed to parse (Can't write to or create math temp directory): F^i_{1.3} \gg M^c_{2.0}

All these modules and dependencies add into repository Failed to parse (Can't write to or create math temp directory): R

Now we will create a module Failed to parse (Can't write to or create math temp directory): T_{1.0}

that depends all formulas: 

Failed to parse (Can't write to or create math temp directory): T_{1.0} \gg F^1_{1.0}

Failed to parse (Can't write to or create math temp directory): T_{1.0} \gg F^2_{1.0}

...

Failed to parse (Can't write to or create math temp directory): T_{1.0} \gg F^n_{1.0}

and add this module as well as its dependencies into repository Failed to parse (Can't write to or create math temp directory): R .

Claim: There Failed to parse (Can't write to or create math temp directory): \exists

a configuration Failed to parse (Can't write to or create math temp directory): C
of repository Failed to parse (Can't write to or create math temp directory): R
and Failed to parse (Can't write to or create math temp directory): T_{1.0} \in C
Failed to parse (Can't write to or create math temp directory): \Longleftrightarrow
there is a solution to the wikipedia::3SAT formula.

Proof

"Failed to parse (Can't write to or create math temp directory): \Leftarrow ": Let's have an evaluation of each variable to either true or false that evaluates the whole wikipedia::3SAT formula to true. Then Failed to parse (Can't write to or create math temp directory): C = { T_{1.0} } \bigcup { M^i_{1.0} : v_i } \bigcup {M^i_{2.0} : \neg v_i } \bigcup { F^i_{1.1} : x_{i1} } \bigcup { F^i_{1.2} : \neg x_{i1} \vee x_{i2} } \bigcup { F^i_{1.3} : \neg x_{i1} \vee \neg x_{i2} \vee x_{i3} }