[VLSI CAD] MiniSAT?

🆓 Free article · Anyone can read this article for free

The Satisfiability (SAT) problem is summarized by the following question:

Can the variables be set to True / False such that the given Boolean formula is True?

For example, given the formula f(x,y,z)=(x || y) & (!x || z),

• Finding out how to assign True/False to x, y, and z so that the entire formula is True is an SAT problem.

This seems simple enough,

• but when the number of variables is in the thousands or tens of thousands
• and the constraints are in the hundreds of thousands, complete exploration becomes impossible.

MiniSat Page

by Niklas Eén, Niklas Sörensson

2. What kind of SAT solver is MiniSat

MiniSat is a high-performance CDCL-based SAT solver.

To summarize its features:

• CDCL (Conflict-Driven Clause Learning)
• Very small codebase
• Fast and stable
• Easy to embed as a library in other tools

So, while MiniSat can be used on its own, it is actually used more for the following purposes.

• Formal Verification tool internal engine
• EDA tool decision engine
• Research prototype baseline solver
• SMT/PB solver backend SAT engine

In other words,

MiniSat is more of a "standard engine in the SAT solver world"

3. But real-world problems don't end with SATs

The problem is that real-world constraints aren't always Boolean.

For example, this constraint is not a SAT:

3a + 2b + c ≥ 4

Here, a, b, and c are Boolean variables, but the expression itself is a constraint with integer weights.

This constraint is called a Pseudo-Boolean (PB) constraint.

PB problems are characterized by:

• Variables are Boolean
• Constraints are linear integer inequalities
• Often have an optimization problem (min/max)

4. The core idea of MiniSat+

MiniSat+ is not a new solver.

Translate the PB constraint into SAT, and then solve it with MiniSat

This is the structure:

PB problem
↓ (translation)
SAT problem
↓
MiniSat

MiniSat+ is responsible for this translation layer.

5. How to change PB → SAT

MiniSat+ uses the following logic circuit-based techniques to change PB constraints to SAT.

• BDD (Binary Decision Diagram)
• Adder network
• Sorting network

The key is:

• Create a logic circuit
• Determine if the PB constraint is satisfied
• Convert that circuit to CNF with Tseitin transformation
• Input the result into MiniSat

In other words,

"Create a circuit that checks for constraints,

6. Why switch to SAT

You may ask, why not just write your own PB solver?

• SAT solvers have been optimized for decades
• Clause learning, heuristics, and propagation are very powerful
• For "almost SAT problems",
  • SAT conversion + MiniSat is often faster than PB native solver
    • Mostly Boolean structures
    • Only some weight/count constraints
  • Formal equivalence checking
  • Choosing a minimal fix set in ECO
  • Constraint-based synthesis
  • Resource / option selection problems
  • Some STA/CDC/DFT internal decision logic
  • MiniSat
    → High-performance Boolean SAT solver
    → Fast engine for solving choice problems
  • MiniSat+
    → Integer weighted constraints (PB) to SAT. Leverages the power of MiniSat
  • Why use it
    → SAT solver is still the most powerful combinatorial search engine
    → Structurally well-suited for EDA/Verification

especially for EDA/Verification problems:The MiniSat+ approach works well on these structures.

7. Where is it used from an EDA perspective

From an engineer's perspective, the MiniSat series is a natural fit for the following problems.The common thread is that they all have this in common.

Selection variables + constraints + combinatorial explosion

The moment you try to manually handle this with human logic, it becomes a maintenance nightmare.
SAT solver solves this at the engine level.

8. One-paragraph summary

Frequently Asked Questions

What is the SAT problem?

SAT asks whether variables can be set to true or false so that a given Boolean formula is true. With thousands of variables and hundreds of thousands of constraints, complete exploration becomes impossible.

What kind of SAT solver is MiniSat?

MiniSat is a high-performance CDCL-based SAT solver with a very small codebase that is fast, stable and easy to embed as a library. It is used inside formal verification tools, EDA decision engines and SMT and pseudo-Boolean solver backends.

What is a pseudo-Boolean constraint?

A pseudo-Boolean constraint has Boolean variables but is a linear integer inequality, such as 3a + 2b + c >= 4. Such problems often also include an optimization objective.

How does MiniSat+ solve pseudo-Boolean problems?

MiniSat+ translates the pseudo-Boolean constraint into SAT and solves it with MiniSat. It builds a checking circuit using BDD, adder network or sorting network techniques, converts it to CNF with Tseitin transformation, and passes it to MiniSat.

Related reading

• [VLSI CAD] Expressed in EDA
• [VLSI CAD] Why Optimization is Hard: NP-hard, heuristic, AI EDA
• [VLSI CAD] Why Two-Level Logic Minimization is Challenging
• [VLSI CAD] kbdd - MiniSAT - Espresso - SIS?
• What is VLSI CAD and EDA?: Electronic Design Automation