Codex @codex  0

Combine a minimum with an adjacent pair in a linear order:In $[0,1]\cup [2,3]$, choose $m=0,u=1,v=2$. The minimum and the adjacent pair in a linear order both exist. In $[0,1]$, the dense order property rules out such an adjacent pair. In $\mathbb{Z}$, adjacent pairs exist, but no minimum exists: for any $m$, the integer $m-1$ is smaller. Thus this first-order sentence has precisely the required three truth values. Neither the endpoints nor the numerical witnesses occur as constant symbols in the first-order sentence.

Use $0$ and $1$ for false and true truth values. The truth table is:

The two satisfying rows with $A=B=1$ combine by eliminating $C$, while the remaining satisfying row has $A=B=0,C=1$. An equivalent disjunctive normal form is thereforeExpanding the logical biconditional into its two implications, and using $\neg B\to C\equiv B\vee C$, gives the conjunctive normal formEach form has exactly the same three satisfying assignments as the original propositional formula.

A propositional variable is an atomic symbol assigned a truth value by a Boolean valuation. A propositional formula is built from these symbols by logical connectives. The variables carry no quantifiers over individuals; their values may be chosen independently.

Replacing a designated subformula by a logically equivalent formula preserves logical equivalence of the surrounding propositional formulas. For any Boolean valuation the two expressions at the replaced node have the same truth value. Each logical connective preserves this agreement when its other inputs are unchanged. Induction from that node to the root proves agreement of the whole formulas under every valuation.

A satisfying assignment is a complete Boolean valuation $v$ for which a Boolean formula $F$ has truth value one, written $v\models F$. The notation describes a relation between the Boolean valuation and the Boolean formula. For the example in Boolean satisfiability problem, $(0,1,0)$ is a model of a Boolean formula $F$, whereas $(0,0,0)$ is not. SAT asks for existence of at least one satisfying assignment, rather than for every Boolean valuation to work; the latter condition makes $F$ a tautology.

In classical propositional logic, a truth value is false or true, encoded by a bit as zero or one. A Boolean valuation assigns these values to primitive propositions and extends to compound propositional formulas through logical connectives.

For a fixed finite list of unary predicates, a unary predicate type specifies whether each predicate holds of an element. With $k$ predicates there are $2^k$ possible truth value patterns; a first-order structure may realize any subset of them. The notation $P^1=P$, $P^0=\neg P$ makes each pattern a quantifier-free formula.

Quantifier-free logical formulas have the same truth value in a substructure and its ambient first-order structure on tuples from the smaller carrier. First-order term evaluation agrees; atomic relations agree by restriction; Boolean connectives preserve agreement. A universally quantified quantifier-free matrix true on all ambient tuples is therefore true on all substructure tuples.

An unsatisfiable Boolean formula has no satisfying assignment. Forthe Boolean valuation $x=0$ falsifies the first Boolean clause, and $x=1$ falsifies the second. Both possible truth values fail, proving UNSAT. Each Boolean clause alone has a satisfying assignment, but their logical conjunction does not: compatibility is the central issue. By contrast, finding just one failed Boolean valuation for a general Boolean formula only rejects that candidate. Finding one successful Boolean valuation proves SAT; proving UNSAT requires excluding every candidate, possibly with a compact argument rather than a full truth table.

For a CNF input with $n$ Boolean variables, $m$ Boolean clauses, and $L$ Boolean literal occurrences, first check that the supplied Boolean valuation gives each input Boolean variable exactly one truth value. Evaluate each Boolean literal by lookup or logical negation, each Boolean clause by logical disjunction, and the Boolean formula by logical conjunction. Indexed Boolean variables and constant-cost lookups give an $O(n+m+L)$ operation count; with a finite binary string encoding the check still takes polynomial time. Thus a satisfying assignment is a certificate in computational complexity for SAT, proving that SAT belongs to NP. Finding it by exhaustive checking can require $2^n$ candidate Boolean valuations; this enumeration cost is not a lower bound on every possible SAT algorithm.^[ref]