Satisfiability and Constraint Systems

The Central Idea

A propositional formula is satisfiable if there exists at least one truth assignment that makes the formula true.

For example,

is satisfiable because

makes the formula true.

Satisfying Assignment

A satisfying assignment is an assignment of truth values to all variables that makes the entire formula true.

If

then

is satisfying because both clauses evaluate to true.

Unsatisfiable Formula

A formula is unsatisfiable if no truth assignment makes it true.

For example,

is unsatisfiable because \(p\) cannot be both true and false.

An unsatisfiable propositional formula is a contradiction.

Tautology versus Satisfiability

A tautology is true under every assignment.

A satisfiable formula needs only one assignment that makes it true.

Therefore,

but not every satisfiable formula is a tautology.

Three Basic Possibilities

A propositional formula can be:

• a tautology: true under every assignment;
• a contradiction: false under every assignment;
• a contingency: true under some assignments and false under others.

Tautologies and contingencies are satisfiable.

Contradictions are unsatisfiable.

Constraint Systems

A constraint system is a collection of conditions that must be satisfied simultaneously.

If the constraints are

then the combined system can be written

A solution must satisfy every constraint.

Example of a Logical Constraint System

Suppose three requirements are:

The full system is

Conjunctive Normal Form

Satisfiability problems are often written in conjunctive normal form, or CNF.

A CNF formula is an AND of OR-clauses:

Each \(L_{ij}\) is a literal.

Clause

A clause is a disjunction of literals.

For example,

is a clause.

A clause is satisfied when at least one of its literals is true.

A CNF Formula Is Satisfied Clause by Clause

For

both clauses must be true.

The first clause requires at least one of \(p,q\) to be true.

The second requires at least one of \(\neg p,r\) to be true.

SAT

The Boolean satisfiability problem, commonly called SAT, asks:

Given a Boolean formula, does there exist an assignment of truth values that makes the formula true?

The answer is either:

or

SAT as a Decision Problem

SAT is a decision problem because the basic question has a yes-or-no answer.

If a satisfying assignment exists, the answer is yes.

If no such assignment exists, the answer is no.

Search and Decision

The decision version asks whether a satisfying assignment exists.

A search version asks us to actually find one.

For example, for

one satisfying assignment is

Truth Tables Can Solve Small SAT Problems

With \(n\) Boolean variables, there are

possible assignments.

A truth table can evaluate the formula under every assignment.

If at least one final row is true, the formula is satisfiable.

Example: Truth-Table Satisfiability

Consider

One true row exists, so

Brute-Force Search

The simplest general SAT strategy is:

1. list every possible assignment;
2. evaluate the formula;
3. stop if a satisfying assignment is found;
4. declare unsatisfiable if every assignment fails.

This is called brute-force search.

The Cost of Brute Force

Every additional variable doubles the number of assignments.

With \(10\) variables:

With \(20\) variables:

With \(30\) variables:

Exhaustive search becomes expensive quickly.

Partial Assignments

A partial assignment gives truth values to only some variables.

For example,

may be assigned while \(r\) remains undecided.

Partial assignments are useful when reasoning step by step.

Unit Clause

A unit clause contains only one literal.

For example,

or

To satisfy a unit clause, its literal must be true.

Unit Propagation

Suppose a CNF formula contains the unit clause

Then any satisfying assignment must have

Substituting that forced value may simplify other clauses and create new unit clauses.

Repeating this process is called unit propagation.

Example of Unit Propagation

Consider

The first clause forces

Then

reduces to

So \(q=T\), which then forces \(r=T\).

Contradiction by Unit Propagation

Consider

The first unit clause forces \(p=T\).

The second forces \(p=F\).

The requirements conflict, so the system is unsatisfiable.

Pure Literals

A variable is pure in a CNF formula if it appears only with one polarity.

For example, if \(p\) appears only as

and never as

then \(p\) is a positive pure literal.

Pure-Literal Reasoning

If \(p\) appears only positively, assigning

cannot make any clause worse because no clause requires \(\neg p\).

Similarly, a variable appearing only negatively can safely be assigned

when searching for one satisfying assignment.

Branching

When no variable is forced, a solver may choose an undecided variable and branch.

For variable \(p\), consider:

in one branch and

in another.

Each branch creates a smaller logical problem.

Backtracking

If a chosen branch produces a contradiction, that branch cannot contain a satisfying assignment.

The search can return to an earlier choice and try the other value.

This is backtracking.

A Basic SAT Search Pattern

A simple recursive SAT strategy is:

1. simplify using forced assignments;
2. if every clause is satisfied, return success;
3. if some clause becomes impossible, return failure;
4. choose an undecided variable;
5. try one truth value;
6. if that fails, try the other.

Clause Becomes Satisfied

Suppose a clause is

If \(p=T\), the entire clause is already true.

The values of \(q\) and \(r\) no longer matter for satisfying that clause.

Clause Becomes Shorter

Suppose

Then

reduces to

A false literal contributes nothing to a disjunction.

Empty Clause

If every literal in a clause becomes false, the clause cannot be satisfied.

Conceptually, this produces an empty clause.

An empty clause signals contradiction under the current partial assignment.

All Clauses Satisfied

If every clause is already true under a partial assignment, the remaining unassigned variables may be chosen arbitrarily unless some additional condition exists.

A satisfying completion has been found.

Solution Space

The solution space of a Boolean constraint system is the set of all satisfying assignments.

A formula can have:

• no solutions;
• exactly one solution;
• several solutions;
• every possible assignment as a solution.

Unique Satisfiability

A formula is uniquely satisfiable when exactly one assignment makes it true.

For example,

over variables \(p,q\) has exactly one satisfying assignment:

Counting Satisfying Assignments

Sometimes we want more than a yes-or-no SAT answer.

We may ask:

How many assignments satisfy the formula?

For example,

has three satisfying assignments out of four possible assignments.

Constraint Graph Perspective

A logical constraint system can also be viewed structurally.

Variables are connected when they occur together in constraints.

This perspective can reveal which parts of the system interact and which parts are independent.

Independent Subsystems

Consider

The variables \(p,q\) occur only in the first clause, while \(r,s\) occur only in the second.

The two constraints can therefore be reasoned about independently before combining their solutions.

Modeling “At Least One”

If at least one of \(p,q,r\) must be true, write

Modeling “At Most One”

If at most one of \(p,q,r\) may be true, forbid every pair from being true together:

Modeling “Exactly One”

Exactly one of \(p,q,r\) must be true means:

• at least one is true;
• at most one is true.

Therefore,

Modeling Implication as a Constraint

The rule

If \(p\), then \(q\)

can be written

In CNF-style form,

Modeling Mutual Exclusion

Suppose \(p\) and \(q\) cannot both be true.

Write

By De Morgan,

Modeling Equivalence

Suppose \(p\) and \(q\) must have the same truth value.

Write

One CNF representation is

Modeling Difference

Suppose exactly one of \(p\) and \(q\) must be true.

This is XOR:

One CNF form is

Example: Scheduling Constraint

Let

If the meeting must be on exactly one of the two days, write

This enforces both availability and exclusivity.

Example: Resource Assignment

Suppose tasks \(A\) and \(B\) cannot use the same exclusive resource at the same time.

Let

The constraint is

Example: Dependency Constraint

Suppose feature \(A\) requires feature \(B\).

Let

Then

becomes

Example: Configuration System

Suppose a product has Boolean options \(A,B,C\) with rules:

• at least one of \(A\) or \(B\) must be selected;
• \(A\) requires \(C\);
• \(B\) and \(C\) cannot both be selected.

The system becomes

Check a Configuration

Test

Then

Therefore, the configuration satisfies all constraints.

Unsatisfiable Constraint Systems

A constraint system can become impossible when its requirements conflict.

For example,

is unsatisfiable.

The first two constraints force \(q=T\), while the third requires \(q=F\).

Minimal Conflicting Sets

In a large unsatisfiable system, a smaller subset of constraints may already be contradictory.

Identifying such a conflicting subset can help explain why the full system has no solution.

Redundant Constraints

A constraint is redundant if removing it does not change the set of satisfying assignments.

For example, if a system already contains

then adding

imposes no new restriction.

Logical Consequence inside a Constraint System

A formula \(C\) is a logical consequence of a constraint system \(S\) if every assignment satisfying \(S\) also satisfies \(C\).

For example,

logically implies

Checking Consequence with Satisfiability

To test whether

ask whether

is satisfiable.

If it is unsatisfiable, then no model of \(S\) can make \(C\) false.

Constraint Satisfaction beyond Boolean Variables

The general idea of constraint satisfaction is broader than Boolean SAT.

Variables may take values from finite domains such as

or

Constraints restrict which combinations are allowed.

Finite-Domain Constraint Problem

A finite-domain constraint problem typically contains:

• variables;
• a finite domain for each variable;
• constraints relating the variables.

A solution assigns one domain value to every variable while satisfying all constraints.

Boolean SAT as a Special Constraint Problem

SAT is a special case in which every variable has the domain

The constraints are expressed with Boolean formulas.

Graph Coloring as a Constraint System

In a graph-coloring problem, each vertex receives a color from a finite set.

Adjacent vertices are constrained to receive different colors.

This is a finite-domain constraint satisfaction problem.

Scheduling as a Constraint System

Scheduling problems may assign times, rooms, or resources to activities.

Constraints can express:

• non-overlap;
• precedence;
• availability;
• capacity;
• required dependencies.

Puzzles as Constraint Systems

Many logic puzzles can be represented by variables and constraints.

The puzzle solution is simply an assignment satisfying every stated rule.

Formalization separates the logical structure from the story used to present it.

Why SAT Is Important

SAT is one of the central problems in theoretical computer science and practical automated reasoning.

Many problems can be encoded as Boolean variables and constraints.

A SAT solver can then search for a satisfying configuration.

Applications of Satisfiability

Satisfiability methods appear in areas such as:

• hardware verification;
• software verification;
• planning;
• scheduling;
• configuration;
• test generation;
• logical reasoning;
• combinatorial search.

Complexity Perspective

SAT is historically important because it was the first problem proved NP-complete.

Informally, this means that many apparently different computational problems can be translated into SAT with polynomial overhead.

A full treatment of computational complexity belongs later, but the key idea is that SAT provides a universal language for many finite search problems.

Verification Is Easy Once a Candidate Is Given

If someone proposes a complete assignment, checking it is straightforward:

1. substitute the truth values;
2. evaluate each clause;
3. confirm that every clause is true.

Finding the assignment can be much harder than checking one.

Common Error: Confusing Satisfiable with True

A formula is not simply “satisfiable” or “unsatisfiable” under one assignment.

Under a specific assignment, the formula is true or false.

Satisfiability asks whether at least one assignment exists that makes it true.

Common Error: Requiring Every Assignment to Work

A satisfiable formula does not need to be true under every assignment.

That stronger condition defines a tautology.

Common Error: Satisfying Only Some Clauses

In CNF,

every clause must be true.

Satisfying most clauses is not enough.

Common Error: Requiring Every Literal in a Clause

A clause is a disjunction.

Therefore, only one literal needs to be true for the clause to be satisfied.

Requiring all literals would incorrectly turn OR into AND.

Common Error: Ignoring Negation

The literal

is true when

A variable and its negation impose opposite truth requirements.

Common Error: Assuming a Partial Assignment Is a Full Solution

A partial assignment may satisfy every currently examined clause, but unassigned variables may still affect remaining constraints.

A full satisfying assignment must assign every relevant variable.

Common Error: Continuing a Contradictory Branch

Once a clause has become impossible under a partial assignment, no extension of that assignment can repair the clause.

The branch should be abandoned.

A Reliable Procedure for Checking One Assignment

1. Write the proposed truth value of every variable.
2. Evaluate each literal.
3. Evaluate each clause.
4. Check whether every clause is true.
5. If yes, the assignment satisfies the system.
6. If any clause is false, the assignment fails.

A Reliable Procedure for Small SAT Problems

1. List the variables.
2. Compute the \(2^n\) possible assignments.
3. Evaluate the formula under each assignment.
4. Stop if a satisfying assignment is found when only existence matters.
5. If no assignment works, declare the formula unsatisfiable.

A Reliable Procedure for Constraint Translation

1. Choose a Boolean variable for each yes/no condition.
2. Translate “at least one” using OR.
3. Translate “all” using AND.
4. Translate “if ... then ...” using implication.
5. Translate “not both” using \(\neg p\lor\neg q\).
6. Translate “exactly one” as at least one plus at most one.
7. Combine all independent requirements with AND.

A Reliable Procedure for Basic Propagation

1. Look for unit clauses.
2. Assign the forced truth values.
3. Remove clauses already satisfied.
4. Remove false literals from remaining clauses.
5. Repeat when new unit clauses appear.
6. If a clause becomes impossible, backtrack or conclude contradiction.

Example: Full Constraint Reasoning Workflow

Consider

The first clause forces

Then

forces

Next,

forces

Finally,

forces

Thus one satisfying assignment is

Practice 1: Satisfiable or Unsatisfiable?

Determine whether

is satisfiable.

Practice 2: Find a Satisfying Assignment

Find one satisfying assignment for

Practice 3: Check an Assignment

Does

satisfy

Practice 4: Unit Clause

If a CNF formula contains the clause

what value must \(q\) have in every satisfying assignment?

Practice 5: At Least One

Write a Boolean constraint saying that at least one of \(p,q,r\) is true.

Practice 6: Mutual Exclusion

Write a CNF clause saying that \(p\) and \(q\) cannot both be true.

Practice 7: Implication

Rewrite

as a clause using only NOT and OR.

Practice 8: Exactly One of Two

Write a CNF formula requiring exactly one of \(p\) and \(q\) to be true.

Practice 9: Count Assignments

How many possible truth assignments exist for \(5\) Boolean variables?

Practice 10: Logical Consequence

If

and

are both required, what value must \(q\) have?

Practice Answers

Practice 1

No assignment can make \(p\) and \(\neg p\) true simultaneously.

Practice 2

One example is

Practice 3

First,

Next,

Both clauses are true, so

Practice 4

For \(\neg q\) to be true,

Practice 5

Practice 6

Practice 7

Practice 8

At least one:

At most one:

Together:

Practice 9

Therefore,

Practice 10

Since \(p=T\), the implication \(p\to q\) can be true only if

What to Remember

• A formula is satisfiable if at least one truth assignment makes it true.
• An unsatisfiable Boolean formula has no satisfying assignment.
• A CNF formula is satisfied only when every clause is true.
• A clause is satisfied when at least one of its literals is true.
• SAT asks whether a Boolean formula has a satisfying assignment.
• Truth tables solve small SAT instances by exhaustive search.
• Unit clauses force variable values and support propagation.
• Branching and backtracking explore alternative assignments.
• Many finite scheduling, configuration, and allocation problems can be expressed as constraints.
• Boolean SAT is a special case of finite-domain constraint satisfaction.

The central habit is to translate each requirement into a precise logical condition, combine the requirements carefully, and then reason about whether any complete assignment can satisfy them all.

Where We Go Next

Satisfiability shows how finite Boolean structures can encode and solve constraint systems. The final lesson in this sequence turns to another digital use of finite structure: representing information with bits and detecting errors when that information is stored or transmitted.

The next lesson, Error Detection and Digital Representation, introduces binary representation, parity checks, redundancy, simple error-detection schemes, and the logic behind reliable digital data.