# Polynomial Calculus Space and Resolution Width

[:link: **FOCS 2019**](https://conferences.computer.org/focs/2019/pdfs/FOCS2019-7pBwCpNH4Mz2L4MJWVl6Xp/7cpQGJYEFsceQxRIvfKPTo/7z604k5UcdLYt5kLZpdDKD.pdf)
*Nicola Galesi*
*Leszek A. Kolodziejczyk*
*Neil Thapen*

---

## Conjunctive Normal Form

\begin{align*}
(x_1 \vee \bar x_2) \wedge
(x_3 \vee \bar x_4 \vee x_5) \wedge
x_6
\\
\{
\{ x_1, \bar x_2 \},
\{ x_3, \bar x_4, x_5 \},
\{ x_6 \}
\}
\end{align*}

- ==boolean variable==: a 0/1 valued variable
- ==literal==: a boolean variable or its negation
- ==clause==: a disjunction/set of literals
- ==clause width==: number of literals in a clause
- ==$k$-clause==: a clause with width at most $k$
- ==CNF==: a conjunction/set of clauses
- ==$k$-CNF==: a CNF containing exactly $k$ clauses
- ==assignment==: a function that assigns variables values
- ==assignment width==: the cardinality of the domain of an assignment
- ==$k$-assignment==: an assignment with width at most $k$

> **Any sentence can be made into a CNF.**
> :::spoiler Proof
> Let $c_1,\dots,c_k$ be literals, and $C = c_1 \vee\cdots\vee c_k$.
> Let $P_1,\dots,P_n$ be clauses, and $P = P_1 \wedge\cdots\wedge P_n$.
> Let $Q_1,\dots,Q_m$ be clauses, and $Q = Q_1 \wedge\cdots\wedge Q_m$.
>
> || sentence(s) | CNF | reason |
> |:-:|:-:|:-:|:-:|
> |(1)| $C,P,Q,P \wedge Q$ | same | definition |
> |(2)| $\bar C$ | $$ \bigwedge_{i=1}^k \bar c_i $$ | De Morgan |
> |(3)| $P \vee Q$ | $$ \bigwedge_{i=1}^n \bigwedge_{j=1}^m (P_i \vee Q_j)$$ | distribution |
> |(4)| $\bar P$ | $$ \bigvee_{i=1}^n \bar P_i $$ | De Morgan, (1), (2) |
> |(5)| $P \Rightarrow Q$ | $\bar P \wedge Q$ | definition, (1), (4) |
> >|(6)| $P \Leftrightarrow Q$ | $(P \Rightarrow Q) \wedge (Q \Rightarrow P)$ | definition, (1), (5) |
> :::
> [color=brown]

## Resolution

$C_1,C_2$ are clauses, and $x$ is a literal.
$$
\frac
{C_1 \vee x \quad \bar x \vee C_2}
{C_1 \vee C_2}
\qquad
\frac
{C_1 \cup \{x\} \quad \{\bar x\} \cup C_2}
{C_1 \cup C_2}
$$

> **Resolution is a consequence of natural deduction.**
> :::spoiler Proof
> $$
> \displaystyle\frac {
> \displaystyle\frac {
> \displaystyle\frac {
> [\bar C_1]
> }{
> \bar C_1
> }
> \quad
> \displaystyle\frac {
> C_1 \vee x
> }{
> \bar C_1 \Rightarrow x
> }
> }{
> x
> }
> \quad
> \displaystyle\frac {
> \bar x \vee C_2
> }{
> x \Rightarrow C_2
> }
> }{
> \displaystyle\frac {
> C_2
> }{
> \displaystyle\frac {
> \bar C_1 \Rightarrow C_2
> }{
> C_1 \vee C_2
> }
> }
> [\Rightarrow\text{Intro.}]
> }
> $$
> :::
> [color=brown]

## Resolution Refutation