Boolean satisfiability problem facts for kids

The Boolean satisfiability problem is a special kind of puzzle in logic and computer science. Imagine you have a statement or a rule, like a math problem, but instead of numbers, it uses ideas that can be either true or false.

This puzzle asks: Can you make this statement true by picking the right "true" or "false" values for its parts?

• If you can find a way to make the statement true, it's called satisfiable.
• If there's no way to make it true, and it will always be false no matter what values you pick, then it's unsatisfiable.

Computer scientists often call this problem SAT for short.

What is a SAT Problem?

Building Blocks of the Puzzle

To understand SAT, we need to know a few terms:

• Variables: These are like placeholders, usually letters (like A, B, C). Each variable can be either true or false.
• Literals: A literal is a variable itself (like A) or the opposite of a variable (like "not A"). If A is true, "not A" is false.
• Clauses: These are small groups of literals joined by "OR". For example, (A OR B OR C) is a clause. This clause is true if at least one of A, B, or C is true.
• Formulas: A SAT problem is usually written as a "formula." This formula is made up of several clauses joined together by "AND".

So, a SAT problem looks like: (Clause 1) AND (Clause 2) AND (Clause 3) ... For the whole formula to be true, every single clause must be true.

A Special Way to Write Puzzles: CNF

In computer science, SAT problems are often written in a special way called "conjunctive normal form" (CNF). This just means the puzzle is set up with clauses joined by "AND", and inside each clause, literals are joined by "OR".

Example: 3SAT

One common type of SAT problem is called 3SAT. In 3SAT, every clause has exactly three literals.

Here's what a 3SAT problem might look like:

(A₁ OR B₁ OR C₁) AND

(A₂ OR B₂ OR C₂) AND

(A₃ OR B₃ OR C₃) AND ...

In this example, (A₁ OR B₁ OR C₁) is one clause, and B₁ is one of the literals in that clause. The goal is to find if you can pick "true" or "false" for all the A's, B's, and C's so that every single clause becomes true.

Why is SAT Important?

The Boolean satisfiability problem is very important in computer science. It helps us understand how hard certain problems are for computers to solve.

The Cook-Levin Theorem

In the early 1970s, two computer scientists named Stephen Cook and Leonid Levin showed something very important about SAT. They proved that SAT is an "NP-complete" problem. This discovery is known as the Cook–Levin theorem.

What does "NP-complete" mean?

• It means that if you can find a fast way to solve SAT, you can also find a fast way to solve many, many other difficult problems in computer science.
• However, no one has ever found a truly fast way to solve NP-complete problems for very large puzzles. This is one of the biggest unsolved questions in computer science!

Karp's 21 Problems

The 3SAT problem is one of the "21 NP-complete problems" identified by Richard M. Karp in 1972. These problems are like a special club of hard problems that are all connected to each other. If you solve one quickly, you can solve them all quickly.

Images for kids

• 

  This image shows a way to change a 3-SAT puzzle into another type of puzzle. The goal is to make sure exactly one part of a group is true.

See also

In Spanish: Problema de satisfacibilidad booleana para niños