3
$\begingroup$

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:3

$$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$.


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

$\endgroup$
  • 2
    $\begingroup$ It looks like a NULL, that is, a contradiction (that can never be satisfied). It is indeed not well defined in the paper, but I'm not so sure it is a common notation. $\endgroup$ – Ran G. Sep 26 '15 at 15:39
5
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.