Ordered Binary Decision Diagrams

The brute force approach: $O(2^n)$

If all the leaf nodes point at the same result, we can reducing the tree.

Reduced OBDD: canonical, unique.

Different ordering may have very different graphs.

A graph is reduced if

It contains no vertex s.t. the right child is equal to the left child.
There are no distinct vertices $v,v'$ that are isomorphic.

Predicate Logic

Syntax

A vocabulary $S=(F,\mathcal R,r)$ for FOL is a set of functions, a set of relations, and a function $r$ called arity.

Let $V=\{x,y,\cdots\}$ be a set of variables.

Terms: Any variable in $V$ is a term. If $f$ is a $k$-ary and $t_1,\cdots,t_k$ are terms, then $f(t_1,\cdots,t_k)$ is a term.

Atomic expression: If $R$ is a $k$-ary relation and $t_1,\cdots,t_k$ are terms, then $R(t_1,\cdots,t_k)$ is called atomic expression.

First order expressions: atomic expressions are well-formed expressions. If $\varphi,\psi$ are expressions, then the following are well-formed expressions: $\neg\varphi,\varphi\land\psi$

If $x$ is a variable that occurs free, then $\forall x.\varphi$ is a well-formed expresion.

Notation: $\exists x.\varphi\equiv\neg\forall x.\neg\varphi$, and vice versa.

Example

$F=\{f_1,f_2\},\mathcal R=\{R_1\}$

$f_1$ and $R_1$ have arity $2$, $f_2$ has arity $3$.

$(\forall x\exists y R_1(f_1(x,y),y)\land R_1(f_2(x,y,z),z))$ ($x,y$ are bounded in the first term, $x,y,z$ are free in the second one)

$\forall x\exists y R_1(f_1(x,y),y)$ (every variable is bounded)

When is a formula true?

For example, $\vDash\forall x.(P(x)\lor\neg P(x))$

First-Order Logic

Semantics

A vocabulary $V$.

A model $M$ appropriate to $V$ is a pair $M=(U,\mu)$ where $U$ is the universe of $M$ and $\mu$ is a function assigning to each symbol actual objects in $U$.

Definition of evaluation in a model: If $\varphi=R(t_1,\cdots,t_k)$ is an atomic expression, $$ M\vDash\varphi\Leftrightarrow(\mu(t_1),\cdots,\mu(t_k))\in\mu(R) $$ Also, we have $M\vDash\varphi\land\psi$ iff $M\vDash\varphi$ and $M\vDash\psi$. Similarly for negation and disjunction.

An expression is valid if it is satisfied by any model.

Axiomatization

If $t_1=t_1',\cdots,t_k=t_k'$, then $f(t_1,\cdots,t_k)=f(t_1',\cdots,t_k')$

If $t_1=t_1',\cdots,t_k=t_k'$, then $R(t_1,\cdots,t_k)\Rightarrow R(t_1',\cdots,t_k')$

Any expression of the form $\forall x\phi\Rightarrow\phi[x\gets t]$.

Any expression of the form $\phi\Rightarrow\forall x\phi$ with $x$ not free in $\phi$.

Any expression of the form $\forall x(\phi\Rightarrow\psi)\Rightarrow(\forall x\phi\Rightarrow\forall x\psi)$ Modus Ponens

Proofs

A proof $S$ for an expression $\varphi_n$ is a sequence $S=\{\varphi_1,\cdots,\varphi_n\}$ s.t. each expression $\varphi_i\in S$ is either an element of $\Lambda$, or can be obtained by MP from previous expressions in $S$.

$S$ is a proof of $\varphi_n$ in $\Lambda$
$\varphi_n$ is called a first order theorem, write $\vdash\varphi_n$

Relation between $\vDash\varphi$ and $\vdash\varphi$:

Let $\Delta$ be a set of expressions, $\varphi$ another expression.

$\varphi$ is a valid consequence of $\Delta$: $\Delta\vDash\varphi$ if any model that satisfies each expression in $\Delta$ also satisfies $\varphi$.

$\varphi$ is a $\Delta$-first-order theorem :$\Delta\vdash\varphi$. If there is a finite sequence of expressions $S=\{\varphi_1,\cdots,\varphi_n\}$ s.t. $\varphi_n=\varphi$ and for every $\varphi_i\in S$, either $\varphi_i\in\Lambda\cup\Delta$, or $\varphi_i$ can be obtained by MP from previous expressions in $S$

Soundness and Completeness

A set of expressions $\Delta$ is consistent if it is not $\Delta\vdash\bot$.

Soundness of FOL: $\Delta\vdash\varphi\Rightarrow\Delta\vDash\varphi$.

Completeness of FOL: $\Delta\vDash\varphi\Rightarrow\Delta\vdash\varphi$

If $\Delta$ is consistent, then it has a model.

Undecidability of FOL

Entscheidunsproblem: There is no mechanical procedure to establish whether $\vDash\varphi$ holds for any arbitrary formula $\varphi$.

If we focus on a "subset" of FOL, i.e. we called First Order Theories, there is hope for computability.

Examples:

Quantifier-free equality of real numbers
Quantifier-free linear arithmetic

SMT

Notation

We generalize CDCL to a method for satisfiability of formulae in a certain theory $T$.

The method is called DPLL(T). The tools are called Satisfiability Modulo Theories solvers (SMT solvers).

Assume that for each theory we have a decision procedure $DP_T$ for the conjunctive fragment of $T$. Each literal is a first order atomic expression or its negation

propositional skeleton: we generalize each atomic expression into a Boolean variable, e.g. $$ \varphi:=(x=y)\land(((y=z)\land\neg(x=z))\lor(x=z))\Rightarrow p\land((q\land\neg r)\land r) $$

DPLL(T)

We invoke a SAT solver on propositional skeleton. That could return an assignment $a$.

Then we invoke $DP_T$ with the conjunction of these atoms $Th(a)$. $DP_T$ would return that $Th(a)$ is UNSAT.

We call $\neg Th(a)$ a blocking clause returned by $DP_T$.

We then add $\neg Th(a)$ to the set of clauses for the SAT solver.

... until we get SAT answer.