Satisfiable in logic: meaning and examples

A formula is satisfiable when at least one assignment of values to its variables makes it true. The assignment that does so is its witness, or satisfying assignment.

Satisfiability is the weakest useful property of a formula: it asks only whether the formula can be true, not whether it must be. Every tautology and every contingency is satisfiable; a contradiction is the one kind of formula that is not, so unsatisfiable and contradictory mean the same thing. Deciding satisfiability for large formulas is the SAT problem, the job of a SAT solver, and the engine switches to one when a formula has more inputs than an exhaustive check can enumerate.

The artefact on this page is the four-row table of (A OR B) AND NOT A. The output column reads false, true, false, false: the formula is true on row 1 only. The satisfiable check holds with the witness A = FALSE, B = TRUE, the summary being that f can be true because the witness makes it true. The contradiction check is violated with the same witness, and the tautology check is violated with the counterexample A = FALSE, B = FALSE. Every witness shown has been replayed through the evaluator before display.

In practice, satisfiability is the question behind reachability: can this branch ever run, can this rule ever grant access, can this alarm ever sound? A rule that is not satisfiable is dead code with a business label on it. The term is confused with validity, which is the opposite extreme; a formula can be satisfiable and still fail on most rows, as this example does on three rows out of four.

Example

f := (A OR B) AND NOT A · output

Exact checks

Always true (tautology)? No Counterexample: A = F, B = F · Exhaustively checked and solver cross-checked · 1 rows

Always false (contradiction)? No Counterexample: A = F, B = T · Exhaustively checked and solver cross-checked · 2 rows

Can be true? Yes Example assignment: A = F, B = T · Exhaustively checked and solver cross-checked · 2 rows

Truth table (4 rows)

Satisfiable in logic: meaning and examples
#	A	B	f
0	FALSE	FALSE	FALSE
1	FALSE	TRUE	TRUE
2	TRUE	FALSE	FALSE
3	TRUE	TRUE	FALSE

Plain-language reading

Beginnerf is true exactly when both of the following hold:
1. at least one of A or B is true (both may be true)
2. A is false
In every other case, f is false.
About the operators:
- AND is true only when all of its parts are true.
- OR is inclusive: it is true when at least one part is true, including when several are.
- NOT reverses a value: true becomes false and false becomes true.

Intermediatef is true exactly when both of the following hold:
1. at least one of A or B is true (both may be true)
2. A is false
In every other case, f is false.

Advancedf is true exactly when both of the following hold [conjunction ∧]:
1. at least one of A or B is true (both may be true) [inclusive disjunction ∨]
2. A is false [negation ¬]
In every other case, f is false.
Formal notation: (A ∨ B) ∧ ¬A

The common slip

Reading “satisfiable” as “usually true” or “correct”. It means true on at least one row and nothing more; (A OR B) AND NOT A is satisfiable and false on three of its four rows. The witness tells you which case to look at, not how common it is.

Questions

How does the engine show that a formula is satisfiable?

By producing a witness, an assignment on which the formula evaluates to TRUE, and replaying it through the independent evaluator before showing it. For a formula that is not satisfiable there is no witness, and the check reports that no assignment makes it true.

Practice

Tautology, contradiction or contingency: exercises with answers

Glossary

Generated from the Tangibool engine, semantics tangibool-semantics/1, engine 1.0.0, build 2026-11-07. Every table, map, simplification and verdict on these pages was computed by the Tangibool engine when the site was built, and every claim was re-checked by the same exact checker the app uses. Limits are stated where they apply. © 2026 Foreranger LTD.