\documentclass[12pt,a4paper,english]{article}

\usepackage[utf8]{inputenc}
\usepackage{babel}
\usepackage{amsmath}
\usepackage{amssymb}
\usepackage{amsthm}

\usepackage{enumerate}

\usepackage{hyperref}

\usepackage{bussproofs}
\usepackage{tikz}

\usetikzlibrary{calc,arrows}

\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}

\theoremstyle{definition}
\newtheorem{definition}[theorem]{Definition}
\newtheorem{example}[theorem]{Example}

\newcommand{\dsb}[1]{[\![ #1 ]\!]}
\newcommand{\intp}[1]{\dsb{#1}_\mathfrak A}

\title{Oblig 2}
\author{INF3170 / INF4171}

\date{\textbf{Deadline:} November 9, 2015}

\begin{document}

\maketitle{}

\section*{Delivery}

The answers should be handed in using \href{https://devilry.ifi.uio.no/}{Devilry}. The deadline is Monday, November 9, at 23:59. Delivery should be a single plain text (.txt) or PDF file.

For those choosing to submit a SAT solver, a .tgz-archive with all source code should be delivered in addition to the other answers.

\section*{Problem 1: Resolution}

\subsection*{Part 1a}

Use the Resolution calculus to show that
\begin{align*}
    (P\lor Q) \land (P\lor \neg Q) \land (\neg P\lor Q) \land (\neg P\lor \neg Q)
\end{align*}
is unsatisfiable.

\subsection*{Part 1b}

Use the Resolution calculus to show that
\begin{align*}
    &\{\{P,Q,R\},\{P,Q,\neg R\},\{P,\neg Q,R\},\{P,\neg Q,\neg R\},\\
    &\qquad\{\neg P,Q,R\},\{\neg P,Q,\neg R\},\{\neg P,\neg Q,R\},\{\neg P,\neg Q,\neg R\}\}
\end{align*}
is unsatisfiable. Hint: You should use a modified Resolution where you do not create every resolvent at every step. Try to create only those you need.

\section*{{Problem 2: LK}}

\subsection*{Part 2a}

Use LK (or another calculus of your choice) to prove or find counter models to the following formulas

\begin{enumerate}[i)]
    \item $(P\to Q)\to(Q\to P)$
    \item $P\to (Q\to P)$
    \item $((P\land Q)\to R) \to (P\to (Q\to R))$
\end{enumerate}

\subsection*{Part 2b}

Use LK (or another calculus of your choice) to prove or find counter models to the following formulas

\begin{enumerate}[i)]
    \item $\forall x Px \to \exists x Px$
    \item $\exists x Px \to \forall x Px$
\end{enumerate}

\subsection*{Part 2c}

In the LK rules $R\forall$ and $L\exists$ we introduce a parameter in the premise. This parameter may not occur in the conclusion. Drop this requirement, and use the new rules $R\forall^*$ and $L\exists^*$ in separate proofs of falsifiable formulas. (That is, show that these new rules are unsound.)

\section*{Problem 3: SAT-solver (OPTIONAL)}

If you chose this option, all the other problems are optional.

Write a program that checks whether a given CNF formula is satisfiable. The program can be written in Java, Python, C, C++, Haskell or Scheme. Contact Andreas (\href{mailto:andreana@ifi.uio.no}{andreana@ifi.uio.no}) if you want to use a different language.

The program should take as input the name of a file. This file will contain the formulas to be checked. The output should at least contain the line numbers of the satisfiable formulas. An empty formula (empty line) is unsatisfiable, while an empty clause is valid.

The input file will be constructed as follows: Each line is a ;-separated list of clauses, where each clause is a space-separated list of literals. Each literal is a non-zero number, where each positive number is an atomic formula, and negative numbers are negative literals (negations of atomic formulas), such that $\overline x = -x$.

The file \texttt{CNF\_test.txt} contains three formulas where the first two are unsatisfiable.

\appendix

\section{Proofs in different calculi}

The calculi we have seen in this course differ in what they aim to prove, but they can all be used to show validity, satisfiability, falsifiability and unsatisfiability. Since these are pairwise opposite, we divide our calculi into those showing validity and those showing satisfiability.

Since $\phi$ is valid if and only if $\neg \phi$ is not satisfiable. We can use a satisfiability calculus with $\neg\phi$ as input to check if $\phi$ is valid. We use similar tricks to apply any calculus to any problem.

If we want to use LK to prove that a $\phi$ is valid, we need to prove the sequent $\vdash \phi$. If we want to show that $\phi$ is unsatisfiable we prove $\vdash \neg\phi$ or $\phi\vdash$.

\section{DPLL}

The algorithm DPLL\footnote{\url{https://en.wikipedia.org/wiki/DPLL_algorithm}} is an algorithm for checking the satisfiability of Propositional Conjunctive Normal Form formulas. Despite the fact that CNFSAT is an NP-complete problem, DPLL turned out to perform very well in many situations.

The core of DPLL is based on the following observations: First, if some clause contains a single literal, then any satisfying valuation must make this literal true. Forcing the truth value assignment to the associated atomic formula.

For the second observation, we need some terminology. We characterise literals by their polarity. An atomic formula is a positive literal, the negation of an atomic formula is a negative literal. Complementary literals always have opposite polarity.

The second observation is that if an atomic formula always occurs in literals with the same polarity, we can make all literals containing that atomic formula true.

These observations needs to be accounted for in any efficient SAT solver.

\section{Additional LK rules}

Sometimes, it saves work to split a proof on some propositional variable. That is, split it onto two cases, one for each possible truth assignment.

\begin{prooftree}
    \AxiomC{$\Gamma,P\vdash \Delta$}
    \AxiomC{$\Gamma\vdash \Delta,P$}
    \RightLabel{Atomic Cut}
    \BinaryInfC{$\Gamma\vdash\Delta$}
\end{prooftree}

Another rule that can be very useful is the Lemma Generation rule. To understand this rule, note that $\phi\lor\psi\Leftrightarrow \phi\lor(\neg\phi\land\psi)$.

\begin{prooftree}
    \AxiomC{$\phi,\Gamma\vdash\Delta$}
    \AxiomC{$\neg\phi,\psi,\Gamma\vdash\Delta$}
    \RightLabel{Lemma Generation}
    \BinaryInfC{$\phi\lor\psi, \Gamma\vdash\Delta$}
\end{prooftree}

\end{document}
