World's most popular travel blog for travel bloggers.

[Answers] What does a square mean in a Boolean formula

, , No Comments
Problem Detail: 

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.

Asked By : juaninf

Answered By : Yuval Filmus

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.

Best Answer from StackOverflow

Question Source :

3.2K people like this

 Download Related Notes/Documents


Post a Comment

Let us know your responses and feedback