patternMinor
What does a square mean in a Boolean formula
Viewed 0 times
booleanwhatmeandoessquareformula
Problem
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:
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)+1, s(x\mapsto\overline{b})\}\;\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.
Lemma 3 The space satisfies the following three properties:
- $s(\Gamma \cup \{\Box\})$ = 0
- For any unsatisfiable formula $\Gamma$, and any partial truth assignment $\phi$, we have $s(\phi(\Gamma))\leq s(\Gamma)$.
- 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)+1, s(x\mapsto\overline{b})\}\;\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.
Solution
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.
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.
Context
StackExchange Computer Science Q#47576, answer score: 5
Revisions (0)
No revisions yet.