What does a square mean in a Boolean formula

Question

I am reading the paper Measuring the hardness of SAT instances by Ansótegui, Bonet, Levy and Manyà (Proc. 23rd AAAI Conf. on AI, pp. 222–228, 2008) (PDF) and I would like to know what the square symbol in the following means

Lemma 3 The space satisfies the following three properties:

1. $s(\Gamma \cup \{\Box\})$ = 0
2. For any unsatisfiable formula $\Gamma$, and any partial truth assignment $\phi$, we have $s(\phi(\Gamma))\leq s(\Gamma)$.
3. For any unsatisfiable formula $\Gamma$, if $\Box\notin\Gamma$, then there exists a variable $x$ and an assignment $\phi\colon\{x\}\to\{0,1\}$, such that $s(\phi(\Gamma))\leq s(\Gamma)-1$.

The space of a formula is the minimum measure on formulas that satisfy (1), (2) and (3). In other words, we could define the space as:³

$$s(\Gamma) = \min_{x, \overline{x}\in\Gamma, b\in\{0,1\}} \big\{ \max\{s([x\mapsto b](\Gamma))+1, s([x\mapsto\overline{b}](\Gamma))\}\;\big\}$$ when $\Box\notin\Gamma$, and $s(\Gamma\cup\{\Box\}) = 0$.

---

³ Note that, since $\Gamma$ is unsatisfiable, it either contains $\Box$ or it contains a variable with both signs.

Answer 1

Ran's comment is correct. This isn't standard notation in proof complexity (the relevant area of TCS), though it might be standard in SAT solving (the relevant applied area). It stands for the empty disjunction.

Semantically, the empty disjunction is the same as contradiction, but the former is a clause whereas the latter is a formula (or sometimes a constant). The usual symbol for contradiction is $\bot$, read bottom.