LibraryReExportIsNPComplete

From APIDesign

Revision as of 10:10, 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 (math_image_error /var/www/apidesign/httpdocs/images/tmp/47a0277764a595bcd1283bc249ff6e29.png , , /var/www/apidesign/httpdocs): (x_{11} \wedge x_{12} \wedge x_{13}) \vee

Failed to parse (math_image_error /var/www/apidesign/httpdocs/images/tmp/c93acfeee2c280a097d1de66d239c0c4.png , , /var/www/apidesign/httpdocs): (x_{21} \wedge x_{22} \wedge x_{23}) \vee

Failed to parse (math_image_error /var/www/apidesign/httpdocs/images/tmp/1056e7a0d1d607627d29f1837aeb8c3f.png , , /var/www/apidesign/httpdocs): (x_{31} \wedge x_{32} \wedge x_{33}) \vee

Failed to parse (math_image_error /var/www/apidesign/httpdocs/images/tmp/2f43b42fd833d1e77420a8dae7419000.png , , /var/www/apidesign/httpdocs): ...

Failed to parse (math_image_error /var/www/apidesign/httpdocs/images/tmp/444d35b526a6051b0c8736ccebed1e89.png , , /var/www/apidesign/httpdocs): (x_{n1} \wedge x_{n2} \wedge x_{n3})

where each Failed to parse (math_image_error /var/www/apidesign/httpdocs/images/tmp/f7c29f8af650931b6a58668170124ac3.png , , /var/www/apidesign/httpdocs): x_{ab}

is a variable Failed to parse (math_image_error /var/www/apidesign/httpdocs/images/tmp/1df181eaa1bb40a0067c06ead197170d.png  ,  , /var/www/apidesign/httpdocs): v_i
or a negation of a variable Failed to parse (math_image_error /var/www/apidesign/httpdocs/images/tmp/59f40fb0dfe22965c7f08c66ddfca2bc.png  ,  , /var/www/apidesign/httpdocs): \neg v_i

. Each variable Failed to parse (math_image_error /var/www/apidesign/httpdocs/images/tmp/1df181eaa1bb40a0067c06ead197170d.png , , /var/www/apidesign/httpdocs): v_i

can appear multiple times in the expression.

Module Dependencies Problem

Let Failed to parse (math_image_error /var/www/apidesign/httpdocs/images/tmp/603461a02a54d311299bbe0f2ee2fd57.png , , /var/www/apidesign/httpdocs): A, B, C, ...

denote an API.

Let Failed to parse (math_image_error /var/www/apidesign/httpdocs/images/tmp/23539be001ebf31cc0b1204218c778eb.png , , /var/www/apidesign/httpdocs): A_1, A_{1.1}, A_{1.7}, A_{1.11}

denote compatible versions of API Failed to parse (math_image_error /var/www/apidesign/httpdocs/images/tmp/7fc56270e7a70fa81a5935b72eacbe29.png  ,  , /var/www/apidesign/httpdocs): A

.

Let Failed to parse (math_image_error /var/www/apidesign/httpdocs/images/tmp/3af6e7b3a4a6412d2fd9a134660bf029.png , , /var/www/apidesign/httpdocs): A_1, A_{2.0}, A_{3.1}

denote incompatible versions of API Failed to parse (math_image_error /var/www/apidesign/httpdocs/images/tmp/7fc56270e7a70fa81a5935b72eacbe29.png  ,  , /var/www/apidesign/httpdocs): A

.

Let Failed to parse (math_image_error /var/www/apidesign/httpdocs/images/tmp/d3747fe17dea5426abe438fc8a47a064.png , , /var/www/apidesign/httpdocs): 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 (math_image_error /var/www/apidesign/httpdocs/images/tmp/0cef438625ca45280c922aaf3d8d7bd9.png , , /var/www/apidesign/httpdocs): 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 (math_image_error /var/www/apidesign/httpdocs/images/tmp/5f0c2abe81264bb793e9c277e5d23a42.png , , /var/www/apidesign/httpdocs): 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 (math_image_error /var/www/apidesign/httpdocs/images/tmp/5f0c2abe81264bb793e9c277e5d23a42.png , , /var/www/apidesign/httpdocs): R=(M,D) , if Failed to parse (math_image_error /var/www/apidesign/httpdocs/images/tmp/ccb62089b190b0fbd045249cbcd47fc9.png , , /var/www/apidesign/httpdocs): C \subseteq M , where following is satisfied:

Failed to parse (math_image_error /var/www/apidesign/httpdocs/images/tmp/933575179f38635778eb726243afda3f.png , , /var/www/apidesign/httpdocs): \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 (math_image_error /var/www/apidesign/httpdocs/images/tmp/8a64fff2b98c6fd70e01eecf6caa1d03.png , , /var/www/apidesign/httpdocs): \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 (math_image_error /var/www/apidesign/httpdocs/images/tmp/ea05cb7649741b2628bf63ab9aa0ecbd.png , , /var/www/apidesign/httpdocs): A_{p.q} \gg ... \gg B_{x.y}

and Failed to parse (math_image_error /var/www/apidesign/httpdocs/images/tmp/3355e82c29534cf56c7a4436ec086a94.png  ,  , /var/www/apidesign/httpdocs): A_{p.q} \gg ... \gg B_{u.v}
then Failed to parse (math_image_error /var/www/apidesign/httpdocs/images/tmp/37ba8d851c836f6ca0158c0be1489f40.png  ,  , /var/www/apidesign/httpdocs): 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 (math_image_error /var/www/apidesign/httpdocs/images/tmp/5f0c2abe81264bb793e9c277e5d23a42.png , , /var/www/apidesign/httpdocs): R=(M,D)

and a module Failed to parse (math_image_error /var/www/apidesign/httpdocs/images/tmp/4cfccc68f6f2a85824f1e2aa908a72a2.png  ,  , /var/www/apidesign/httpdocs): A \in M

. Does there exist a configuration Failed to parse (math_image_error /var/www/apidesign/httpdocs/images/tmp/0d61f8370cad1d412f80b84d143e1257.png , , /var/www/apidesign/httpdocs): C

in the repository Failed to parse (math_image_error /var/www/apidesign/httpdocs/images/tmp/e1e1d3d40573127e9ee0480caf1283d6.png  ,  , /var/www/apidesign/httpdocs): R

, such that the module Failed to parse (math_image_error /var/www/apidesign/httpdocs/images/tmp/21b399ddb43f8c61fbea617b595cba1b.png , , /var/www/apidesign/httpdocs): A \in C , e.g. the module can be enabled?

Converstion of wikipedia::3SAT to Module Dependencies Problem

Let

Failed to parse (math_image_error /var/www/apidesign/httpdocs/images/tmp/47a0277764a595bcd1283bc249ff6e29.png , , /var/www/apidesign/httpdocs): (x_{11} \wedge x_{12} \wedge x_{13}) \vee

Failed to parse (math_image_error /var/www/apidesign/httpdocs/images/tmp/c93acfeee2c280a097d1de66d239c0c4.png , , /var/www/apidesign/httpdocs): (x_{21} \wedge x_{22} \wedge x_{23}) \vee

Failed to parse (math_image_error /var/www/apidesign/httpdocs/images/tmp/1056e7a0d1d607627d29f1837aeb8c3f.png , , /var/www/apidesign/httpdocs): (x_{31} \wedge x_{32} \wedge x_{33}) \vee

Failed to parse (math_image_error /var/www/apidesign/httpdocs/images/tmp/2f43b42fd833d1e77420a8dae7419000.png , , /var/www/apidesign/httpdocs): ...

Failed to parse (math_image_error /var/www/apidesign/httpdocs/images/tmp/444d35b526a6051b0c8736ccebed1e89.png , , /var/www/apidesign/httpdocs): (x_{n1} \wedge x_{n2} \wedge x_{n3})

be a formula with variables Failed to parse (math_image_error /var/www/apidesign/httpdocs/images/tmp/8d70b5d26b99f566646b0538598fa174.png , , /var/www/apidesign/httpdocs): v_1, ..., v_m .

For each variable Failed to parse (math_image_error /var/www/apidesign/httpdocs/images/tmp/1df181eaa1bb40a0067c06ead197170d.png , , /var/www/apidesign/httpdocs): v_i

let's create two modules Failed to parse (math_image_error /var/www/apidesign/httpdocs/images/tmp/7f452842ac00f6d3f3eb60578b77bd23.png  ,  , /var/www/apidesign/httpdocs): M^i_{1.0}
and Failed to parse (math_image_error /var/www/apidesign/httpdocs/images/tmp/4bb26054d98decfa57f82430a4d3a170.png  ,  , /var/www/apidesign/httpdocs): M^i_{2.0}

, which are mutually incompatible.

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.