LARA

Differences

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

Link to this comparison view

sav08:homework05 [2008/03/25 14:22]
piskac
sav08:homework05 [2015/04/21 17:30]
Line 1: Line 1:
-====== Homework 05 - due 2 April 2008 (after break) ====== 
  
- 
- 
- 
- 
-===== Problem 1 ===== 
- 
-Extend the DPLL SAT solver from [[homework04]] with the ability to generate resolution proofs. 
- 
-As before, if a given formula is satisfiable,​ the SAT solver should produce an assignment to all variables such that the formula evaluates to //true// under this assignment. 
- 
-Additionally,​ if a given formula is unsatisfiable,​ the SAT solver should produce unsatisfiability proof in some format. ​ Use proof trees for resolution proofs, whose nodes indicate the variable on which resolution is performed and contain subtrees for proofs of clauses on which resolution is performed. 
-  * you can also use [[http://​fmv.jku.at/​booleforce/​README.tracecheck|Tracecheck format]] for TraceCheck tool from [[http://​fmv.jku.at/​booleforce/​|BooleForce]] solver 
- 
-**Optional extension (can be used for project)**: Extend this solver with 2-literal watching, lemma learning and heuristics. ​ You can look at the source code of existing implementations to gain insight into techniques (such as http://​sourceforge.net/​projects/​dpt ) but you are not allowed to copy it, you must write your own implementation. 
- 
-We will run a small competition of implemented solvers. 
- 
-Note that it can be [[http://​www.prover.com/​company/​employment/​view/?​id=27|useful to know about SAT solvers]]. 
- 
-Test examples shown in the class: 
- 
-[[dpll:​test.cnf]] [[dpll:​test2.cnf]] [[dpll:​test3.cnf]] 
- 
-[[http://​icwww.epfl.ch/​~piskac/​test.cnf|test.cnf]]. 
-[[http://​icwww.epfl.ch/​~piskac/​test2.cnf|test2.cnf]]. 
-[[http://​icwww.epfl.ch/​~piskac/​test3.cnf|test3.cnf]]. 
- 
-===== Problem 2 ===== 
- 
-Consider the notion of [[Substitutions for First-Order Logic]]. 
- 
-**Part a)** Consider an implementation of that definition of sfsubst as a recursive function on syntax trees that directly follows its definition. ​ Consider formulas with many identical quantifiers,​ $\exists x. \exists x.\ldots \exists x. P(x)$. ​ More precisely, let $F_0$ denote formula $P(x)$ and $F_{n+1}$ denote formula $\exists x. F_n$ for all $n \geq 0$.  How many accesses to syntax tree nodes does this function perform on the abstract syntax tree of formula $F_n$? 
- 
-**Part b)** Define the "fast, safe" substitution,​ fsfsubst, with the property that for a formula with $n$ syntax tree nodes, the number of accesses to syntax tree nodes is $O(n)$. ​ (You do not need to implement it, but this may be helpful if for you to debug your definition.) 
- 
-**Part c)** Prove (using appropriate proof technique) that your definition of fsfsubst has the property 
-\[ 
-    e_F(fsfsubst(\{x_1 \mapsto t_1,​\ldots,​x_n \mapsto t_n\})(F))(I) = e_F(F)(I[x_1 \mapsto e_T(t_1)(I),​\ldots,​ x_n \mapsto e_T(t_n)(I)]) 
-\] 
-You can assume that formulas are built using only these symbols: 
-  * one constant $a$ 
-  * one unary function symbol $f$ 
-  * one binary relation symbol $R$ 
-  * operations $\land$, $\lnot$, $\exists$ as the only logical operations. 
- 
-===== Problem 3 ===== 
- 
-Consider the definition of [[First-Order Logic Semantics#​Consequence set]] defined in [[First-Order Logic Semantics]]. 
-Prove that it satisfies these properties where $T_1$, $T_2$ denote sets of formulas. 
-\[ 
-\begin{array}{rcl} 
-  T &​\subseteq & Conseq(T) \\ 
-  T_1 \subseteq T_2 &​\rightarrow&​ Conseq(T_1) \subseteq Conseq(T_2) \\ 
-  Conseq(Conseq(T)) &=& Conseq(T) ​ \\ 
-  T_1 \subseteq Conseq(T_2) \land T_2 \subseteq Conseq(T_1) & \rightarrow & Conseq(T_1) = Conseq(T_2) 
-\end{array} 
-\] 
- 
-===== Problem 4 (Optional) ===== 
- 
-Use [[Compactness for First-Order Logic]] to prove the following theorem: 
- 
-If a set $S$ of sentences has arbitrarily large finite models (that is, for every $n$, there exists a model $(D,​\alpha)$ with $D$ a finite set of at least $n$ elements), then $S$ has an infinite model.