Reusing libraries produced by others is essential aspect of [[DistributedDevelopment]]. It simplifies [[Time To Market]], it reduces long term cost of ownership and leads to creation of [[Good Technology|good technologies]]. However it does not come for free. Read details or directly jump to the [[LibraryReExportIsNPComplete#Implications|implications]] that shall improve your every day development habits.

Reusing libraries produced by others is essential aspect of [[DistributedDevelopment]]. It simplifies [[Time To Market]], it reduces long term cost of ownership and leads to creation of [[Good Technology|good technologies]]. However it does not come for free. Read details or directly jump to the [[LibraryReExportIsNPComplete#Implications|implications]] that shall improve your every day development habits.

If you happen to reuse a library that cannot be trusted to keep its [[BackwardCompatibility]], then do whatever you can to not re-export its [[API]]s! This has been discussed in [[Chapter 10]], Cooperating with Other [[API]]s, but in short: If you hide such library for internal use and do not export any of its interfaces, you can use whatever version of library you want (even few years older) and nobody shall notice. Moreover in many [[module system]]s there can even be multiple versions of the same library in case they are not re-exported.

If you happen to reuse a library that cannot be trusted to keep its [[BackwardCompatibility]], then do whatever you can to not re-export its [[API]]s! This has been discussed in [[Chapter 10]], Cooperating with Other [[API]]s, but in short: If you hide such library for internal use and do not export any of its interfaces, you can use whatever version of library you want (even few years older) and nobody shall notice. Moreover in many [[module system]]s there can even be multiple versions of the same library in case they are not re-exported.

== Conclusion ==

== Conclusion ==

# discussion at [http://lambda-the-ultimate.org/node/3588 Lambda the Ultimate]

# discussion at [http://lambda-the-ultimate.org/node/3588 Lambda the Ultimate]

# LtU guys pointed out that the proof has already been published: [http://people.debian.org/~dburrows/model.pdf D. Burrows, Modelling and Resolving Software Dependencies]

# LtU guys pointed out that the proof has already been published: [http://people.debian.org/~dburrows/model.pdf D. Burrows, Modelling and Resolving Software Dependencies]

# Equinox is said to [http://blog.bjhargrave.com/2008/03/equinox-and-google-summer-of-code.html use SAT4J solver]

# [[Equinox]] is said to [http://blog.bjhargrave.com/2008/03/equinox-and-google-summer-of-code.html use SAT4J solver]

# EDOS Project seems to find similar proof: See section 3.2 in [http://www.edos-project.org/xwiki/bin/download/Main/D2-1/edos-wp2d1.pdf edos-wp2d1.pdf]

# EDOS Project seems to find similar proof: See section 3.2 in [http://www.edos-project.org/xwiki/bin/download/Main/D2-1/edos-wp2d1.pdf edos-wp2d1.pdf]

<!-- Added correct link to D. Burrows article -->

<!-- Added correct link to D. Burrows article -->

'''qed'''.

'''qed'''.

== Implications ==

== Implications ==

If you happen to reuse a library that cannot be trusted to keep its [[BackwardCompatibility]], then do whatever you can to not re-export its [[API]]s! This has been discussed in [[Chapter 10]], Cooperating with Other [[API]]s, but in short: If you hide such library for internal use and do not export any of its interfaces, you can use whatever version of library you want (even few years older) and nobody shall notice. Moreover in many [[module system]]s there can even be multiple versions of the same library in case they are not re-exported.

If you happen to reuse a library that cannot be trusted to keep its [[BackwardCompatibility]], then do whatever you can to not re-export its [[API]]s! This has been discussed in [[Chapter 10]], Cooperating with Other [[API]]s, but in short: If you hide such library for internal use and do not export any of its interfaces, you can use whatever version of library you want (even few years older) and nobody shall notice. Moreover in many [[module system]]s there can even be multiple versions of the same library in case they are not re-exported.

== Conclusion ==

== Conclusion ==

This page starts by describing a way to convert any [[3SAT]] problem to a solution of finding whether there is a way to satisfy all dependencies of a library in a repository of libraries. Thus proving that the later problem is [[wikipedia::NP-complete|NP-Complete]]. Then it describes the importance of such observations on our [[DistributedDevelopment|development practices]].

This page starts by describing a way to convert any [[3SAT]] problem to a solution of finding whether there is a way to satisfy all dependencies of a library in a repository of libraries. Thus proving that the later problem is [[wikipedia::NP-complete|NP-Complete]]. Then it describes the importance of such observations on our [[DistributedDevelopment|development practices]].

== [[3SAT]] ==

== [[3SAT]] ==

All these modules and dependencies are added into repository <math>R</math>

All these modules and dependencies are added into repository <math>R</math>

Now we will create a module <math>T_{1.0}</math> that depends all formulas:

Now we will create a module <math>T_{1.0}</math> that depends on all formulas:

:<math>T_{1.0} \gg F^1_{1.0}</math>

:<math>T_{1.0} \gg F^1_{1.0}</math>

:<math>T_{1.0} \gg F^2_{1.0}</math>

:<math>T_{1.0} \gg F^2_{1.0}</math>

For <math>i</math>-th ''3-or'' there is <math>T_{1.0} \gg F^i_{1.0}</math> dependency which is satisfied. That means <math>F^i_{1.1} \in C \vee F^i_{1.2} \in C \vee F^i_{1.3} \in C</math> - at least one version of <math>F^i</math> module is present in the configuration. The one <math>F^i</math> that has the satisfied dependency reexports <math>M^j_{1.0}</math> (which means <math>v_j = true</math>) or <math>M^j_{2.0}</math> (which means <math>v_j = false</math>). Anyway each <math>i</math> ''3-or'' evaluates to <math>true</math>.

For <math>i</math>-th ''3-or'' there is <math>T_{1.0} \gg F^i_{1.0}</math> dependency which is satisfied. That means <math>F^i_{1.1} \in C \vee F^i_{1.2} \in C \vee F^i_{1.3} \in C</math> - at least one version of <math>F^i</math> module is present in the configuration. The one <math>F^i</math> that has the satisfied dependency reexports <math>M^j_{1.0}</math> (which means <math>v_j = true</math>) or <math>M^j_{2.0}</math> (which means <math>v_j = false</math>). Anyway each <math>i</math> ''3-or'' evaluates to <math>true</math>.

The only remaining question is whether a <math>C</math> configuration can force truth variable <math>v_j</math> to be true in one ''3-or'' and false in another. However that would mean that there is re-export via <math>T_{1.0} \gg F^i_{1.x} \gg M^j_{1.0}</math> and also another one via <math>T_{1.0} \gg F^p_{1.u} \gg M^j_{2.0}</math>. However those two ''chain of dependencies'' ending in different versions of <math>M^j</math> cannot be in one <math>C</math> as that breaks the last condition of configuration definition. Thus each <math>M^j</math> is represented only by one version and each <math>v_j</math> is evaluated either to true or false, but never both.

The only remaining question is whether a <math>C</math> configuration can force truth variable <math>v_j</math> to be true in one ''3-or'' and false in another. However that would mean that there is re-export via <math>T_{1.0} \gg F^i_{1.x} \gg M^j_{1.0}</math> and also another one via <math>T_{1.0} \gg F^p_{1.u} \gg M^j_{2.0}</math>. However those two ''chain of dependencies'' ending in different versions of <math>M^j</math> cannot be in one <math>C</math> as that breaks the last condition of configuration definition (each imported object has just one meaning). Thus each <math>M^j</math> is represented only by one version and each <math>v_j</math> is evaluated either to true or false, but never both.

The [[3SAT]] formula's evaluation based on the configuration <math>C</math> is consistent and satisfies the formula.

The [[3SAT]] formula's evaluation based on the configuration <math>C</math> is consistent and satisfies the formula.

"<math>\Rightarrow</math>": Let's have a <math>C</math> configuration satisfies all dependencies of <math>T_{1.0}</math>. Can we also find positive valuation of [[3SAT]] formula?

"<math>\Rightarrow</math>": Let's have a <math>C</math> configuration satisfies all dependencies of <math>T_{1.0}</math>. Can we also find positive valuation of [[3SAT]] formula?

For <math>i</math>-th ''3-or'' there is <math>T_{1.0} \gg F^i_{1.0}</math> dependency which is satisfied. That means <math>F^i_{1.1} \in C \vee F^i_{1.2} \in C \vee F^i_{1.3}</math> - at least one version of <math>F^i</math> module is present in the configuration. The one <math>F^i</math> that has the satisfied dependency reexports <math>M^j_{1.0}</math> (which means <math>v_j = true</math>) or <math>M^j_{2.0}</math> (which means <math>v_j = false</math>). Anyway each <math>i</math> ''3-or'' evaluates to <math>true</math>.

For <math>i</math>-th ''3-or'' there is <math>T_{1.0} \gg F^i_{1.0}</math> dependency which is satisfied. That means <math>F^i_{1.1} \in C \vee F^i_{1.2} \in C \vee F^i_{1.3} \in C</math> - at least one version of <math>F^i</math> module is present in the configuration. The one <math>F^i</math> that has the satisfied dependency reexports <math>M^j_{1.0}</math> (which means <math>v_j = true</math>) or <math>M^j_{2.0}</math> (which means <math>v_j = false</math>). Anyway each <math>i</math> ''3-or'' evaluates to <math>true</math>.

The only remaining question is whether a <math>C</math> configuration can force truth variable <math>v_j</math> to be true in one ''3-or'' and false in another. However that would mean that there is re-export via <math>T_{1.0} \gg F^i_{1.x} \gg M^j_{1.0}</math> and also another one via <math>T_{1.0} \gg F^p_{1.u} \gg M^j_{2.0}</math>. However those two ''chain of dependencies'' ending in different versions of <math>M^j</math> cannot be in one <math>C</math> as that breaks the last condition of configuration definition. Thus each <math>M^j</math> is represented only by one version and each <math>v_j</math> is evaluated either to true or false, but never both.

The only remaining question is whether a <math>C</math> configuration can force truth variable <math>v_j</math> to be true in one ''3-or'' and false in another. However that would mean that there is re-export via <math>T_{1.0} \gg F^i_{1.x} \gg M^j_{1.0}</math> and also another one via <math>T_{1.0} \gg F^p_{1.u} \gg M^j_{2.0}</math>. However those two ''chain of dependencies'' ending in different versions of <math>M^j</math> cannot be in one <math>C</math> as that breaks the last condition of configuration definition. Thus each <math>M^j</math> is represented only by one version and each <math>v_j</math> is evaluated either to true or false, but never both.

"<math>\Rightarrow</math>": Let's have a <math>C</math> configuration satisfies all dependencies of <math>T_{1.0}</math>. Can we also find positive valuation of [[3SAT]] formula?

"<math>\Rightarrow</math>": Let's have a <math>C</math> configuration satisfies all dependencies of <math>T_{1.0}</math>. Can we also find positive valuation of [[3SAT]] formula?

For <math>i</math>-th ''3-or'' there is <math>T_{1.0} \gg F^i_{1.0}</math> dependency which is satisfied. At least by one from <math>F^i_{1.1}</math> or <math>F^i_{1.2}</math> or <math>F^i_{1.3}</math>. The one <math>F^i</math> that has the satisfied dependency reexports <math>M^j_{1.0}</math> (which means <math>v_j = true</math>) or <math>M^j_{2.0}</math> (which means <math>v_j = false</math>). Anyway each <math>i</math> ''3-or'' evaluates to <math>true</math>.

For <math>i</math>-th ''3-or'' there is <math>T_{1.0} \gg F^i_{1.0}</math> dependency which is satisfied. That means <math>F^i_{1.1} \in C \vee F^i_{1.2} \in C \vee F^i_{1.3}</math> - at least one version of <math>F^i</math> module is present in the configuration. The one <math>F^i</math> that has the satisfied dependency reexports <math>M^j_{1.0}</math> (which means <math>v_j = true</math>) or <math>M^j_{2.0}</math> (which means <math>v_j = false</math>). Anyway each <math>i</math> ''3-or'' evaluates to <math>true</math>.

The only remaining question is whether a <math>C</math> configuration can force truth variable <math>v_j</math> to be true in one ''3-or'' and false in another. However that would mean that there is re-export via <math>T_{1.0} \gg F^i_{1.x} \gg M^j_{1.0}</math> and also another one via <math>T_{1.0} \gg F^p_{1.u} \gg M^j_{2.0}</math>. However those two ''chain of dependencies'' ending in different versions of <math>M^j</math> cannot be in one <math>C</math> as that breaks the last condition of configuration definition. Thus each <math>M^j</math> is represented only by one version and each <math>v_j</math> is evaluated either to true or false, but never both.

The only remaining question is whether a <math>C</math> configuration can force truth variable <math>v_j</math> to be true in one ''3-or'' and false in another. However that would mean that there is re-export via <math>T_{1.0} \gg F^i_{1.x} \gg M^j_{1.0}</math> and also another one via <math>T_{1.0} \gg F^p_{1.u} \gg M^j_{2.0}</math>. However those two ''chain of dependencies'' ending in different versions of <math>M^j</math> cannot be in one <math>C</math> as that breaks the last condition of configuration definition. Thus each <math>M^j</math> is represented only by one version and each <math>v_j</math> is evaluated either to true or false, but never both.

# LtU guys pointed out that the proof has already been published: [http://people.debian.org/~dburrows/model.pdf D. Burrows, Modelling and Resolving Software Dependencies]

# LtU guys pointed out that the proof has already been published: [http://people.debian.org/~dburrows/model.pdf D. Burrows, Modelling and Resolving Software Dependencies]

# Equinox is said to [http://blog.bjhargrave.com/2008/03/equinox-and-google-summer-of-code.html use SAT4J solver]

# Equinox is said to [http://blog.bjhargrave.com/2008/03/equinox-and-google-summer-of-code.html use SAT4J solver]

<!-- Added correct link to D. Burrows article -->

<!-- Added correct link to D. Burrows article -->