Satisfying assignment (source code)

= Satisfying assignment
{title2=$v\models F$}

= Model of a Boolean formula
{synonym}

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>.