Dependency resolution and SAT #2
Replies: 6 comments 1 reply
-
@DavidJurajdaNXP , could just give more visibility on which step of the process is expected to get benefit from satisfiability analysis : for the component maintainer when creating a PDSC, for the end user when choosing components and looking for dependencies or somewhere else ? |
Beta Was this translation helpful? Give feedback.
-
Hi @mdortel-stm, I am expecting main benefit for end user in shorter response times during component filtering or project creation (dependency resolution). Any algorithm (filtering, dependency resolution) which is evaluating constrains described by boolean or other expression should decide whether input expression could be satisfied or not in first step. In case of big expression, simple brute force approach consume too much time, but there are advanced algorithms which might provide answer whether it make sense to search for specific solution (expression could be satisfied) in much shorter period. I have not any specific data, but main benefit should be in reduced time consumption in case of large data sets (all components in public register). Specific scenario might be custom filtering of whole public index on web view. I am expecting it might be beneficial also in case of dependency resolver for project creation tool. Data set might significantly grow in future if we decide to introduce configurations, where each individual configuration entity like macro act as operand in dependency expression. |
Beta Was this translation helpful? Give feedback.
-
Article about version solver used by Dart language: |
Beta Was this translation helpful? Give feedback.
-
Another solution used by openSUSE: |
Beta Was this translation helpful? Give feedback.
-
Boolean dependencies by rpm: |
Beta Was this translation helpful? Give feedback.
-
Packaging conference: Conference recordings: Spack package manager: Conda metapackage: uuid: purl: ASP (Answer Set Programing): |
Beta Was this translation helpful? Give feedback.
-
Various software management systems and EDA tools are dealing with dependencies. There are several typical problems:
This problems may be very complex, but there are existing solutions which could offer effective resolution.
A Peek Inside SAT Solvers - Jon Smock
https://rise4fun.com/z3/tutorial (Z3 is a state-of-the art theorem prover from Microsoft Research. It can be used to check the satisfiability of logical formulas over one or more theories)
Solving Linux Upgradeability Problems Using Boolean Optimization
https://medium.com/@sdboyer/so-you-want-to-write-a-package-manager-4ae9c17d9527
Other links:
https://arxiv.org/pdf/1007.1021.pdf
PyEDA
Espresso minimizer
https://doc.opensuse.org/projects/satsolver/11.4/
http://www.lifl.fr/LION9/presentation_orator/lion9.pdf
https://www.cril.univ-artois.fr/documents/nanjing-leberre.pdf
https://www.sat4j.org/
https://www.youtube.com/watch?v=-7jm0siKVtc (I can't get no) satisfaction: Can SAT-solvers resolve dependency hell?
https://research.swtch.com/version-sat
https://hal.inria.fr/hal-00697463/document
https://news.ycombinator.com/item?id=15354838
https://arxiv.org/pdf/2011.07851.pdf
https://en.opensuse.org/openSUSE:Libzypp_satsolver
https://en.opensuse.org/images/b/b9/Fosdem2008-solver.pdf
https://opam.ocaml.org/doc/External_solvers.html
https://www.mancoosi.org/cudf/
https://jlbp.dev/what-is-a-diamond-dependency-conflict
https://wiki.eclipse.org/Equinox_P2_Resolution
https://en.wikipedia.org/wiki/ZYpp
https://news.ycombinator.com/item?id=15354838
https://en.wikipedia.org/wiki/Multiple_inheritance#The_diamond_problem
https://well-typed.com/blog/9/
https://jlbp.dev/
https://cseweb.ucsd.edu/~lerner/papers/opium.pdf
http://wiki.apidesign.org/wiki/LibraryWithoutImplicitExportIsPolynomial
http://lambda-the-ultimate.org/node/3588
https://hal.inria.fr/hal-00697463
https://www.honeybadger.io/blog/golang-go-package-management/
https://arxiv.org/abs/1508.05117
https://wiki.apache.org/confluence/display/MAVENOLD/SAT+Based+Dependency+Resolution
https://doc.opensuse.org/projects/satsolver/11.4/
https://sahandsaba.com/understanding-sat-by-implementing-a-simple-sat-solver-in-python.html
https://cse.buffalo.edu/~erdem/cse331/support/sat-solver/index.html
https://dudka.cz/fss
https://github.com/mame/ruby-minisat
https://pysathq.github.io/usage.html
https://github.com/netom/satispy/
http://t-a-w.blogspot.com/2016/10/z3-constraint-solver-library-for-ruby.html
https://en.wikipedia.org/wiki/Constraint_programming
https://en.wikipedia.org/wiki/Constraint_satisfaction_problem
Beta Was this translation helpful? Give feedback.
All reactions