• English only

# Differences

This shows you the differences between two versions of the page.

using_automata_to_decide_presburger_arithmetic [2009/04/29 10:53]
vkuncak
using_automata_to_decide_presburger_arithmetic [2015/04/21 17:26] (current)
Line 28: Line 28:
v:  1 0 0 0 0   v:  1 0 0 0 0
This string represents the satisfying assignment $\{(x,4),\ (y,3),\ (z,4),\ (v,1)\}$ for the above formula. If we take the valid formula This string represents the satisfying assignment $\{(x,4),\ (y,3),\ (z,4),\ (v,1)\}$ for the above formula. If we take the valid formula
-$+\begin{equation*} \lnot (x = y + v \land z = y + v\ \land\ v=1)\ \lor\ (x = z) \lnot (x = y + v \land z = y + v\ \land\ v=1)\ \lor\ (x = z) -$+\end{equation*}
the corresponding automaton accepts all strings. **(End of example.)** the corresponding automaton accepts all strings. **(End of example.)**

Line 83: Line 83:
Therefore, to check if $F$ is satisfiable,​ we construct $A(F)$ automaton and check whether the graph of $A(F)$ has a reachable accepting state. Therefore, to check if $F$ is satisfiable,​ we construct $A(F)$ automaton and check whether the graph of $A(F)$ has a reachable accepting state.

+**Example:​** Step-by-step construction of automaton for
+\begin{equation*}
+   \lnot (x = y + v \land z = y + v\ \land\ v=1)\ \lor\ (x = z)
+\end{equation*}