SAT problems are kind of cool!

While working on fastbrew, I went into the rabbit hole of SAT, short for Boolean satisfiability.

It is quite interesting. For my application I am rewriting brew’s package manager to be faster and more reliable, so it does not update dozens of packages every time I install something and it does not break the ones I already use.

A Package Manager Puzzle #

Let’s start with a real-life scenario to build intuition.

Imagine you’re setting up your development environment, and you want to install two popular packages:

Node.js (node): You need it for your JavaScript projects.
LLVM: You’re experimenting with compilers, and LLVM is a must.

You run the following command:

fastbrew install node llvm

• Node.js depends on an older version of OpenSSL, say openssl@1.1, for its networking features.
• LLVM requires a newer version, openssl@3, because it’s built with modern security features.

Both OpenSSL versions expose the same libraries, so installing them together breaks things. Toss wget into the mix. It has no dependencies, and now you are juggling compatibility, versions, and constraints. Is there any combination that keeps the system healthy?

This is the kind of question SAT solvers answer gracefully. You describe the rules: dependencies, conflicts, requirements, and ask, “Is there a solution, and if so, which packages are in it?”

What Is SAT? #

A SAT problem starts with a Boolean formula that uses AND (∧), OR (∨), and NOT (¬) across a set of variables. The challenge is to assign true or false to each variable so the whole formula evaluates to true. If such an assignment exists, the formula is satisfiable; otherwise it is unsatisfiable.

SAT problems are NP-complete problems: easy to verify, hard to solve. Despite the intimidating label, SAT solvers are surprisingly practical.

Translating Dependencies into Logic #

To encode the earlier fastbrew scenario, assign a Boolean variable to each package:

• N: Install node
• L: Install llvm
• O1: Install openssl@1.1
• O3: Install openssl@3
• W: Install wget

Then translate dependencies and conflicts into clauses:

• N → O1 becomes ¬N ∨ O1.
• L → O3 becomes ¬L ∨ O3.
• ¬(O1 ∧ O3) becomes ¬O1 ∨ ¬O3.

Requesting both node and llvm forces N = true and L = true. The solver then discovers there is no way to satisfy all clauses at once because openssl@1.1 and openssl@3 cannot coexist, so the formula is unsatisfiable. A solver like MiniSAT reports the conflict instantly, sparing you a broken setup.

How SAT Solvers Work #

Modern solvers behave like methodical puzzle players:

1. Decide: Pick a variable, guess a value.
2. Propagate: Infer any values that must follow from that guess.
3. Conflict-check: If contradictions appear, learn from them and backtrack.

This process repeats with smart heuristics so the solver avoids retracing dead ends. For fastbrew that means validating package plans before touching a single file and explaining why an installation fails.

A Tiny Example in Code #

Here is a toy SAT model with three packages A, B, and C:

from pysat.solvers import Minisat22

solver = Minisat22()

# Clauses
solver.add_clause([1, 2])    # A ∨ B
solver.add_clause([-1, 3])   # ¬A ∨ C
solver.add_clause([-2, -3])  # ¬B ∨ ¬C

if solver.solve():
    print("Satisfiable:", solver.get_model())
else:
    print("Unsatisfiable")

One satisfying assignment is [1, -2, 3], which means install A and C, skip B. Scale this up to thousands of packages and you have the heart of fastbrew’s dependency solver.

Why SAT Helps fastbrew #

• Conflict awareness: Spot incompatible packages before installation starts.
• Minimal churn: Install only the necessary dependencies.
• Clear feedback: Explain why an installation fails instead of crashing halfway through.

Other Places SAT Shines #

• Software verification: Tools like CBMC encode program properties as SAT to prove the absence of bugs.
• Hardware design: Chip designers rely on SAT to validate circuits under tight performance constraints.
• Scheduling: Universities and airlines encode timetables as SAT to avoid double-booking people or resources.
• AI planning: Robots and game agents use SAT to plan sequences of actions without violating rules.
• Cryptanalysis: SAT solvers stress-test cryptographic schemes by searching for breaking inputs.
• Puzzles: Everything from Sudoku to logic riddles can be encoded and solved instantly.

SAT Problems Are Everywhere #

SAT problems are like universal problem-solvers, turning messy real-world challenges into clean logic puzzles. From preventing package manager disasters in fastbrew to designing faster chips, planning robot routes, or even solving your favorite Sudoku puzzle, SAT is everywhere.

Published 08 Oct 2025