• English only

# Differences

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

 sav08:qbf_and_quantifier_elimination [2008/03/10 11:17]vkuncak sav08:qbf_and_quantifier_elimination [2015/04/21 17:30] (current) Both sides previous revision Previous revision 2008/03/11 16:14 vkuncak 2008/03/10 11:17 vkuncak 2008/03/10 11:16 vkuncak 2008/03/10 11:16 vkuncak 2008/03/10 11:14 vkuncak 2008/03/10 11:13 vkuncak 2008/03/10 11:11 vkuncak 2008/03/06 18:09 vkuncak 2008/03/05 21:34 vkuncak created Next revision Previous revision 2008/03/11 16:14 vkuncak 2008/03/10 11:17 vkuncak 2008/03/10 11:16 vkuncak 2008/03/10 11:16 vkuncak 2008/03/10 11:14 vkuncak 2008/03/10 11:13 vkuncak 2008/03/10 11:11 vkuncak 2008/03/06 18:09 vkuncak 2008/03/05 21:34 vkuncak created Line 1: Line 1: ====== QBF and Quantifier Elimination ====== ====== QBF and Quantifier Elimination ====== - === Quantified Propositional Formula Syntax === + ===== Quantified Propositional Formula Syntax ​===== We extend the definition of formulas with quantifiers $\forall p.F$ and $\exists p.F$ where $p \in V$: We extend the definition of formulas with quantifiers $\forall p.F$ and $\exists p.F$ where $p \in V$: - $\begin{array}{rcl} + \begin{equation*}\begin{array}{rcl} ​F ​ & ::= & V \mid {\it false} \mid {\it true} \mid (F \land F) \mid (F \lor F) \mid (\lnot F) \mid (F \rightarrow F) \mid (F \leftrightarrow F) \\ ​F ​ & ::= & V \mid {\it false} \mid {\it true} \mid (F \land F) \mid (F \lor F) \mid (\lnot F) \mid (F \rightarrow F) \mid (F \leftrightarrow F) \\ & \mid & \forall V. F\ \mid\ \exists V. F & \mid & \forall V. F\ \mid\ \exists V. F \end{array} \end{array} -$ + \end{equation*} - === Eliminating quantifiers by expansion === + ===== Eliminating quantifiers by expansion ​===== We can apply the following rules to eliminate propositional quantifiers:​ We can apply the following rules to eliminate propositional quantifiers:​ - $+ \begin{equation*} \exists p. F \ \leadsto subst(\{p \mapsto {\it false}\},F) \lor subst(\{p \mapsto {\it true}\},F) \exists p. F \ \leadsto subst(\{p \mapsto {\it false}\},F) \lor subst(\{p \mapsto {\it true}\},F) -$ + \end{equation*} - $+ \begin{equation*} \forall p. F \ \leadsto subst(\{p \mapsto {\it false}\},F) \land subst(\{p \mapsto {\it true}\},F) \forall p. F \ \leadsto subst(\{p \mapsto {\it false}\},F) \land subst(\{p \mapsto {\it true}\},F) -$ + \end{equation*} Note that the expansion can produce exponentially larger formula. Note that the expansion can produce exponentially larger formula. Notion of quantifier elimination applies to other logic as well. Notion of quantifier elimination applies to other logic as well. - Definition: A logic has //​quantifier elimination//​ if for every formula in the logic, there exists an equivalent formula without quantifiers. + **Definition:** A logic has //​quantifier elimination//​ if for every formula in the logic, there exists an equivalent formula without quantifiers. - Definition: A quantifier elimination algorithm is an algorithm that takes a formula in a logic and converts it into an equivalent formula without quantifiers. + **Definition:** A quantifier elimination algorithm is an algorithm that takes a formula in a logic and converts it into an equivalent formula without quantifiers. - Note: Formula $F$ is valid iff $\forall p_1,​\ldots,​p_n. F$ is true. + **Observation:** Formula $F$ is valid iff $\forall p_1,​\ldots,​p_n. F$ is true. - Note: Formula $F$ is satisfiable iff $\exists p_1,​\ldots,​p_n. F$ is true. + **Observation:** Formula $F$ is satisfiable iff $\exists p_1,​\ldots,​p_n. F$ is true. In general QBF formulas can have alternations between $\forall$ and $\exists$ quantifiers:​ In general QBF formulas can have alternations between $\forall$ and $\exists$ quantifiers:​ - $+ \begin{equation*} ​\forall p. \exists q. ((p \rightarrow q) \land (q \rightarrow r)) ​\forall p. \exists q. ((p \rightarrow q) \land (q \rightarrow r)) -$ + \end{equation*} - === Quantified Propositional Formula Semantics === + ===== Quantified Propositional Formula Semantics ​===== We can similarly provide recursive semantic function definition for propositional logic. We can similarly provide recursive semantic function definition for propositional logic. - === Notes on Computational Complexity === + ===== Summary of Computational Complexity ​of Problems ===== * checking satisfiability of propositional formula $F$ is NP-complete * checking satisfiability of propositional formula $F$ is NP-complete

sav08/qbf_and_quantifier_elimination.txt · Last modified: 2015/04/21 17:30 (external edit)

© EPFL 2018 - Legal notice