uni/sysver/3-sat/blogpost/3-sat.tex

% Options for packages loaded elsewhere
\PassOptionsToPackage{unicode}{hyperref}
\PassOptionsToPackage{hyphens}{url}
%
\documentclass[
  12pt,
]{article}
\usepackage{amsmath,amssymb}
\usepackage{lmodern}
\usepackage{ifxetex,ifluatex}
\usepackage{pagecolor}
\ifnum 0\ifxetex 1\fi\ifluatex 1\fi=0 % if pdftex
  \usepackage[T1]{fontenc}
  \usepackage[utf8]{inputenc}
  \usepackage{textcomp} % provide euro and other symbols
\else % if luatex or xetex
  \usepackage{unicode-math}
  \defaultfontfeatures{Scale=MatchLowercase}
  \defaultfontfeatures[\rmfamily]{Ligatures=TeX,Scale=1}
\fi
% Use upquote if available, for straight quotes in verbatim environments
\IfFileExists{upquote.sty}{\usepackage{upquote}}{}
\IfFileExists{microtype.sty}{% use microtype if available
  \usepackage[]{microtype}
  \UseMicrotypeSet[protrusion]{basicmath} % disable protrusion for tt fonts
}{}
\usepackage{xcolor}
\makeatletter
\@ifundefined{KOMAClassName}{% if non-KOMA class
  \IfFileExists{parskip.sty}{%
    \usepackage{parskip}
  }{% else
    \setlength{\parindent}{0pt}
    \setlength{\parskip}{6pt plus 2pt minus 1pt}}
}{% if KOMA class
  \KOMAoptions{parskip=half}}
\newcommand{\globalcolor}[1]{%
  \color{#1}\global\let\default@color\current@color
}
\makeatother
\definecolor{myforeground}{HTML}{d9bdd7}
\AtBeginDocument{\globalcolor{myforeground}}
\IfFileExists{xurl.sty}{\usepackage{xurl}}{} % add URL line breaks if available
\IfFileExists{bookmark.sty}{\usepackage{bookmark}}{\usepackage{hyperref}}
\hypersetup{
  hidelinks,
  pdfcreator={LaTeX via pandoc}}
\urlstyle{same} % disable monospaced font for URLs
\usepackage[top=2cm, bottom=2cm]{geometry}
\setlength{\emergencystretch}{3em} % prevent overfull lines
\providecommand{\tightlist}{%
  \setlength{\itemsep}{0pt}\setlength{\parskip}{0pt}}
\setcounter{secnumdepth}{-\maxdimen} % remove section numbering
\usepackage{float}
\let\origfigure\figure
\let\endorigfigure\endfigure
\renewenvironment{figure}[1][2] {
    \expandafter\origfigure\expandafter[H]
} {
    \endorigfigure
}
\ifluatex
  \usepackage{selnolig}  % disable illegal ligatures
\fi

\author{}
\date{}

\begin{document}
\definecolor{mybackground}{HTML}{100410}
\pagecolor{mybackground}

\hypertarget{tseitin-transformation}{%
\subsection{Tseitin transformation}\label{tseitin-transformation}}

Let \(F\) be a formula in \(\text{conjunctive normal form}\) (CNF),
i.e., a conjunction of clauses

\begin{equation}
\bigwedge\limits_i^{C} \bigvee\limits_j^{S_i} \ell_{i,j},\ \text{where}\ \ell_{i,j} \in \{ P, \neg P \mid P \text{ is an atom} \}
\label{eq:clauses}\end{equation}

Note that every clause \(C_i\) with \(m\) literals can be seen as a
``nested'' disjunction, i.e.,

\begin{equation}
C_i = (\ell_{i,1} \lor (\ell_{i,2} \lor (\text{...} \lor (\ell_{i,m-1} \lor \ell_{i,m})
\label{eq:nested}\end{equation}

Explain how you can use Tseitin's transformation to convert any
arbitrary formula in CNF into an \textbf{\emph{equi-satisfiable}}
formula in CNF whose clauses have at most 3 literals.

\hypertarget{solution}{%
\paragraph{solution}\label{solution}}

A clause in the formula is with no loss of generality described by

\begin{equation}
C_i = (\ell_{i,1} \lor \ell_{i,2} \lor (\ell_{i,3} \lor (\ell_{i,4} \lor (F))),\ F = \bigvee_{j}^A \ell_{i,j},\ A = {S_i} \setminus \{1,2,3,4\}
\label{eq:general-formula}\end{equation}

We can introduce a new symbol for a satisfiability-equivalent formula

\begin{equation}
(\ell_{i,1} \lor \ell_{i,2} \lor O_1) \land (O_1 \Leftrightarrow (\ell_{i,3} \lor (\ell_{i,4} \lor (F)))
\label{eq:equivalent-formula}\end{equation}

and apply the corresponding Tseitin Encoding

\begin{equation}
\begin{aligned}
(\ell_{i,1} \lor \ell_{i,2} \lor O_1)\land (\neg \ell_{i,3} \lor O_1) &\land \overbrace{(\neg(\ell_{i,4} \lor F) \lor O_1)}^{C_{i,const}} \\
&\land \underbrace{(\neg O_1 \lor \ell_{i,3} \lor (\ell{i,4} \lor (F)))}_{C_i,recursive}
\end{aligned}
\label{eq:tseitin}\end{equation}

Doing so yields two components for which we have to show that they
contain at most 3 literals. The first of which represents a constant
blow-up of conjuncts

\begin{equation}
\begin{aligned}
C_{i,const} &= \neg (\ell_{i,4} \lor F) \lor O_1 \\
&= (\neg \ell_{i,4} \land \neg F) \lor O_1 \\
&= (\neg \ell_{i,4} \lor O_1) \land (\neg F \lor O_1) \\
&= (\neg \ell_{i,4} \lor O_1) \land (\neg (\bigvee_j^A \ell_{i,j} ) \lor O_1) \\
&= (\neg \ell_{i,4} \lor O_1) \land ((\bigwedge_j^A \neg \ell_{i,j} ) \lor O_1) \\
&= (\neg \ell_{i,4} \lor O_1) \land (\bigwedge_j^A \neg \ell_{i,j} \lor O_1) \\
\end{aligned}
\label{eq:conjuncts}\end{equation}

Note that {[}\ref{eq:conjuncts}{]} makes entensive use of the
distributivity of conjuncts and disjuncts to expand \(C_{i,const}\) into
sub-clauses that are short enough.

The other remaining clause is \(C_{i,recursive}\), for which it remains
to be shown that the formula is a disjunction with at most 3 literals.
This term is the original expression \(C_i\) without the disjuncts
\(\ell_{i,1}\) and \(\ell_{i,2}\). The expansion described in
{[}\ref{eq:equivalent-formula}{]} and {[}\ref{eq:tseitin}{]} can thus be
applied again until all clauses have been reduced to form an
equi-satisfiable formula in CNF whose clauses have at most 3 literals.

\end{document}