SAT solvers are used in package managers to resolve dependencies. SAT solver is a tool that determines whether a given boolean formula can be True (it is calle

SAT solvers are used in package managers to resolve dependencies. SAT solver is a tool that determines whether a given boolean formula can be True (it is called SAT) or not. If it can be True, a SAT solver provides values for variables so that you can check that they are correct. For example, a Boolean formula a & (b | c) Can be True if a = True, b = True and c = False. SAT solver can be useful for resolving dependencies in a package manager. Imagine if a user wants to install package A with version >= 1.0, but package A depends on other packages and might conflicts with some packages as well. The package manager converts these requirements into a boolean formula like this: let's say that if variable A₁₀ is True, then package A version 1.0 is installed, if A₁₁ is True, then package A version 1.1 is installed and so on. First, let's express user's desire to have any version of A installed. Here is the rule: A₁₀ | A₁₁ must be True Let's say A version 1.0 requires B version 1.0 or 1.1. We can then write a rule, that if A 1.0 is installed, then B 1.0 or 1.1 must be installed as well: !A₁₀ | (B₁₀ | B₁₁) must be True Now, let' say that B 1.0 conflicts with C 1.0 and both cannot be installed at the same time. We can express that as a formula as well: !(B₁₀ & C₁₀) must be True Finally, we cannot install two versions of the same package, so let's write that too: !(A₁₀ & A₁₁) & !(B₁₀ & B₁₁) must be True Now we can combine all the rules into a single formula. All the rules must be true, so we join them using AND operator: (A₁₀ | A₁₁) & (!A₁₀ | (B₁₀ | B₁₁)) & !(B₁₀ & C₁₀) & !(A₁₀ & A₁₁) & !(B₁₀ & B₁₁) Now we can give the formula to the SAT solver. If will solve it and give a set of versions that need to be installed in order to satisfy all requirements. Or it will prove that this is impossible. Another use of SAT solver is verification of programs: if you have two pieces of code without loops and you want to make sure that they are equivalent, you can convert them into boolean formulas and use SAT to prove that for any given input they produce the same output.