\documentclass[]{article}
% Required packages.
\usepackage[T1]{fontenc}
\usepackage{lmodern}
\usepackage{amssymb,amsmath}
\usepackage{color}
\usepackage{tikz}
\usepackage[utf8]{inputenc}
\usepackage{dsfont}
\usepackage{enumerate}
\usepackage{ifthen}
\let\mathbb\mathds
% Some setup.
\setlength{\parindent}{0pt}
\setlength{\parskip}{6pt plus 2pt minus 1pt}
\setlength{\emergencystretch}{3em} % prevent overfull lines
\setcounter{secnumdepth}{0}
\usetikzlibrary{calc}
% Input data macros for \maketitle.
\title{CS 4810: Homework 7}
\author{due 10/31 11:59pm}
\date{(your name + netid)} % TODO: Fill in your own name and netID here.
\sloppy
% The actual document technically begins here.
\begin{document}
\maketitle
Collaborators: (names and netids) % TODO: List the names and netIDs of everyone who collaborated with you on this homework here.
Each problem is worth 25 points.
\section{Problem 1}
Show that \textbf{NP} is closed under union, concatenation, intersection, and Kleene star.
\section{Problem 2}
Show that the following language is \textbf{NP}-complete (polynomial-time reduction from \textsc{sat}),
\begin{displaymath}
\textsc{double sat} = \{\langle \varphi \rangle \mid \text{$\varphi$ is a Boolean formula with at least two satisfying assignments} \}.
\end{displaymath}
\section{Problem 3}
Let $G$ be a graph.
A \emph{clique} in $G$ is a subset $C$ of vertices such that any two vertices $u,v\in C$ are adjacent.
A \emph{vertex cover} of $G$ is a subset $S$ of vertices such that every edge of $G$ has at least one endpoint in $S$.
Show polynomial-time reductions between the following languages,
\begin{align*}
\textsc{clique} & = \{ \langle G,k \rangle \mid \text{$G$ contains a clique of size $k$} \},\\
\textsc{vertex cover} & = \{ \langle G,\ell \rangle \mid \text{$G$ has a vertex cover of size $\ell$} \}.
\end{align*}
\section{Problem 4}
This problem investigates \emph{resolution}, a method for proving the unsatisfiability of
CNF formulas.
%Let φ = C1 ∧ C2 ∧ · · · ∧ Cm be a formula in cnf, where the Ci are its clauses.
Let $\varphi = C_1\land C_2 \land \cdots \land C_m$ be a CNF formula with clauses $C_1,\ldots,C_m$.
Let
$$
\mathcal C = \{C_i \mid \text{$C_i$ is a clause of $\varphi$}\}.
$$
A resolution step proceeds as follows:
Take two clauses $C_a$ and $C_b$ in $\mathcal C$, which both have some variable $x$ occurring positively in one of the clauses and negatively in the other.
Thus, $C_a = (x \lor y_1 \lor y_2 \lor \cdots \lor y_k)$ and $C_b = (\neg x \lor z_1 \lor z_2 \lor \cdots\lor z_\ell)$, where the $y_i$ and the $z_j$ are literals.
Form the new clause $(y_1 \lor y_2 \lor \cdots \lor y_k \lor z_1 \lor z_2 \lor \cdots \lor z_\ell)$ and remove repeated literals.
Add this new clause to $\mathcal C$.
Repeat the resolution steps until no additional clauses can be obtained.
If the empty clause $()$ is in $\mathcal C$, then declare $\varphi$ unsatisfiable.
Say that resolution is sound if it never declares satisfiable formulas to be unsatisfiable.
Say that resolution is complete if all unsatisfiable formulas are declared to be unsatisfiable.
\subsection{Part a}
Show that resolution is sound and complete.
\subsection{Part b}
Use Part a to show that $\textsc{2-cnf sat} \in \textbf{P}$.
(\textsc{2-cnf sat} is the set of satisfiable formulas in conjunctive normal form with at most two literals per clause.)
\end{document}