CS292C-7: Computer-Aided Reasoning for Software
Lecture 7: Applications and Extensions of SAT

by Yu Feng

Logistics
Homework
HW1 is due
HW2 is out
Final Project
Will provide 2-3 options to choose
Lecture Roadmap
SAT Solving Recap
Boolean satisfiability fundamentals
SAT Power
Why SAT is widely used
Applications & Variants
MaxSAT, optimization, real-world examples
SAT Solving: Recap
SAT Definition
Find assignment making formula true
CDCL
Industrial-grade solving method
NP-complete
First proven NP-complete problem
SAT solving and its applications
Why SAT Is a Big Deal
First NP-complete problem
Historically significant as the first proven NP-complete problem
Problem reduction
Many difficult computational problems can be reduced to SAT
One powerful solver
Build one great SAT solver to tackle all NP-complete problems
Domains Powered by SAT
Hardware Verification
CPU correctness checking
Software Analysis
Symbolic execution, testing
AI Planning
Scheduling, optimization
Product Configuration
Real-world systems
Configuration Problems
Lots of Options = Lots of dependencies
Mercedes C-Class Example
  • 650+ customizable options
  • Complex dependency rules
  • SAT checks consistency
Configuration Dependencies
  • "Thermotronic comfort air conditioning requires high-capacity battery except when combined with gasoline engines of 3.2 liter capacity"
  • Thousands of interacting rules
  • SAT ensures all constraints are satisfied
Why Use SAT for Configurations
Catch Impossibilities
Identify conflicting configurations
Auto-Resolve Dependencies
Handle complex option relationships
Scale Without Errors
Help sales and manufacturing
Beyond SAT — Variants

Basic SAT
Find any satisfying assignment
Optimization
Balance multiple goals
MaxSAT
Maximize satisfied clauses
MaxSAT (Maximum Satisfiability)
Problem: Given formula F in CNF, find assignment maximizing the number of satisfied clauses of F.
For Satisfiable Formulas
If F is satisfiable, the solution to the MaxSAT problem is the number of clauses in F.
For Unsatisfiable Formulas
If F is unsatisfiable, we want to find a maximum subset of F's clauses whose conjunction is satisfiable.
Example: (a ∨b)∧¬a ∧¬b
This formula is unsatisfiable because ¬a ∧¬b contradicts (a ∨b). The MaxSAT solution is to satisfy 2 out of 3 clauses by choosing either (a ∨b)∧¬a or (a ∨b)∧¬b, with assignment (a=false, b=true) or (a=true, b=false) respectively.
Partial MaxSAT
A variant of MaxSAT that distinguishes between two kinds of clauses:
Hard Clauses
Must be satisfied
Non-negotiable constraints
Soft Clauses
Preferably satisfied
Flexible preferences
Partial MaxSAT Problem: Given a CNF formula F where each clause is marked as either hard or soft, find an assignment that:
  1. Satisfies all hard clauses
  1. Maximizes the number of satisfied soft clauses
Partial MaxSAT Generalizes SAT & MaxSAT
SAT
Special case of Partial MaxSAT where:
  • All clauses are hard clauses
  • Must satisfy every constraint
  • Binary outcome: satisfiable or unsatisfiable
MaxSAT
Special case of Partial MaxSAT where:
  • All clauses are implicitly soft clauses
  • Goal is to maximize satisfied clauses
  • Always returns an assignment
Partial MaxSAT
Generalization that provides flexibility:
  • Mixed hard and soft clauses
  • Hard clauses must be satisfied
  • Soft clauses are maximized
In this sense, Partial MaxSAT offers a more flexible framework that encompasses both the strict constraints of SAT and the optimization aspects of MaxSAT in a single formulation.
Weighted MaxSAT
A further generalization of the MaxSAT problem family:
Hard and Soft Clauses
Like Partial MaxSAT, distinguishes between hard clauses (must be satisfied) and soft clauses (preferably satisfied)
Weight Assignment
Each soft clause has an associated weight indicating its importance or priority
Optimization Goal
Find an assignment that satisfies all hard clauses and maximizes the sum of weights of satisfied soft clauses
Partial Weighted MaxSAT provides a flexible framework for modeling complex problems with varying constraint priorities.
Partial MaxSAT is an instance of partial weighted MaxSAT where all clauses have equal weight
Component Configuration Problems
Given a configuration with components, dependencies, and conflicts, we need to:
Feasibility Check
Determine if a new component can be added to the existing configuration without violating constraints
Optimized Installation
Add the component while optimizing a linear objective function (e.g., minimize installation size, maximize performance)
Minimal Disruption
If direct installation is impossible, find an installation path that removes as few conflicting components as possible
These problems can be effectively encoded as Partial Weighted MaxSAT instances, with hard constraints for dependencies and soft constraints for preferences.
Pseudo-Boolean Solvers
SAT + Optimization
Boolean satisfaction with linear objectives
Like 0-1 ILP
Integer Linear Programming with binary variables
Linear Constraints
Variables: 0 or 1, constraints: inequalities
Pseudo-Boolean Constraints Example
SAT for component installation
To install component a, the following constraints must be satisfied:
(¬a ⋁ b) ⋀
(¬a ⋁ c) ⋀
(¬a ⋁ z) ⋀
(¬b ⋁ d) ⋀
(¬c ⋁ d ⋁ e) ⋀
(¬c ⋁ f ⋁ g) ⋀
(¬d ⋁ ¬e) ⋀
(¬y ⋁ z) ⋀
a ⋀ z
Optimal installation
To install component a, the following constraints must be satisfied:
(¬a ⋁ b) ⋀
(¬a ⋁ c) ⋀
(¬a ⋁ z) ⋀
(¬b ⋁ d) ⋀
(¬c ⋁ d ⋁ e) ⋀
(¬c ⋁ f ⋁ g) ⋀
(¬d ⋁ ¬e) ⋀ (¬y ⋁ z) ⋀ a ⋀ z
Assume f and g are 5MB and 2MB each, and all other components are 1MB. How to install a, while minimizing total size?
Optimal installation
Pseudo-boolean optimization:
Minimize: a+b+c+d+e+5f+2g+y+0z
Subject to:
  • (-a + b ≥ 0) ⋀ (-a + c ≥ 0) ⋀ (-a + z ≥ 0)
  • (-b + d ≥ 0) ⋀ (-c + d + e ≥ 0)
  • (-c + f + g ≥ 0) ⋀ (-d + -e ≥ -1)
  • (-y + z ≥ 0) ⋀ (a ≥ 1) ⋀ (z ≥ 1)
Assume f and g are 5MB and 2MB each, and all other components are 1MB. How to install a, while minimizing total size?
Installation with conflicts
Partial MaxSAT solver for component installation
Partial MaxSAT takes as input a set of hard clauses and a set of soft clauses, producing an assignment that satisfies all hard clauses and the greatest number of soft clauses.
To install component a while minimizing removed components:
Hard clauses:
(¬a ⋁ b) ⋀ (¬a ⋁ c) ⋀ (¬a ⋁ z) ⋀
(¬b ⋁ d) ⋀ (¬c ⋁ d ⋁ e) ⋀
(¬c ⋁ f ⋁ g) ⋀ (¬d ⋁ ¬e) ⋀
(¬y ⋁ z) ⋀ a
Soft clauses:
e ⋀ z
Summary
SAT solvers handle massive, complex systems
Enabling solutions for previously intractable problems across multiple domains
MaxSAT, Partial MaxSAT, Weighted MaxSAT generalize SAT
Extending traditional SAT solving with optimization capabilities
Pseudo-Boolean SAT = SAT + Optimization
Adding the ability to minimize or maximize objective functions while satisfying constraints
Applications everywhere
Configuration, synthesis, scheduling, and many other real-world problem domains