Exhaustive check: meaning and examples

An exhaustive check evaluates a property on every assignment of the variables, so its verdict is a proof rather than a sample. The engine runs its checks exhaustively up to 20 inputs and reports a row count with the result.

Exhaustive means complete: for n variables, all 2 to the power n rows are evaluated, and a property that holds on all of them holds outright. This is only possible because propositional formulas have finitely many cases; it is what separates a truth-table proof from testing, where a passing sample leaves other cases open. The cost doubles with each variable, so the engine draws a line at 20 inputs, about a million rows, and switches to a SAT solver beyond it, where the result is still exact but found by search rather than enumeration.

The artefact on this page is (A XOR B) <-> (NOT A <-> B). The tautology check holds, with the summary that f is true on every assignment and a row count of 4: all four rows were evaluated. The simplifier was also run and found no law to apply; it reports the expression unchanged at 4 operators, with the note that smaller equivalent forms are not ruled out. The two results sit together deliberately: the check proves the formula is a tautology, while the simplifier, which only rewrites syntax, could not see that it reduces to TRUE.

Exhaustive checking is the right tool for small rules, access policies and gate-level designs, where the inputs are few and the cost of a missed case is high; it is the method behind every verdict on these pages. Its limit is the exponential row count, which is where SAT solvers and symbolic methods take over. The term is confused with thorough testing (a large sample is still a sample) and with brute force in the pejorative sense; for a million rows, enumeration is simply the honest method.

Example

f := (A XOR B) <-> (NOT A <-> B) · output

Exact checks

Always true (tautology)? Yes · Exhaustively checked and solver cross-checked · 4 rows

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

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

Truth table (4 rows)

Exhaustive check: meaning and examples
#	A	B	f
0	FALSE	FALSE	TRUE
1	FALSE	TRUE	TRUE
2	TRUE	FALSE	TRUE
3	TRUE	TRUE	TRUE

Plain-language reading

Beginnerf is true exactly when the following two conditions have the same truth value (both hold or neither holds):
1. exactly one of A and B is true (not both)
2. A is false if and only if B is true
In every other case, f is false.
About the operators:
- A biconditional (↔) is true when both sides have the same value.
- XOR (exclusive or) is true when exactly one of its two parts is true.
- NOT reverses a value: true becomes false and false becomes true.

Intermediatef is true exactly when the following two conditions have the same truth value (both hold or neither holds):
1. exactly one of A and B is true (not both)
2. A is false if and only if B is true
In every other case, f is false.

Advancedf is true exactly when the following two conditions have the same truth value (both hold or neither holds) [biconditional ↔]:
1. exactly one of A and B is true (not both) [exclusive disjunction ⊕]
2. A is false if and only if B is true [biconditional ↔]
In every other case, f is false.
Formal notation: (A ⊕ B) ↔ (¬A ↔ B)

Simplification, step by step

The engine found no law that shortens this expression; it is already as short as its rewriting laws can make it.

A XOR B <-> (NOT A <-> B)

The common slip

Expecting the simplifier to tell you a formula is a tautology. It applies rewriting laws and stops when none matches, as it did here at 4 operators; the exhaustive check is what proves the property. The pitfall page on simplifier results explains why the two tools answer different questions.

Questions

What does the row count on a verdict mean?

The number of rows the check evaluated before deciding. For a property that holds everywhere, as here, it equals the size of the table, 4 rows; for a violated property it is the number of rows examined up to the first counterexample, which the check then replays and shows.

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.