document.168

Clause tableaux[edit]
When applied to sets of clauses (rather than of arbitrary formulae), tableaux methods allow for a number of efficiency improvements. A first-order clause is a formula \forall x_1,\ldots,x_n L_1 \vee \cdots \vee L_m that does not contain free variables and such that each L_i is a literal. The universal quantifiers are often omitted for clarity, so that for example P(x,y) \vee Q(f(x)) actually means \forall x,y .  P(x,y) \vee Q(f(x)). Note that, if taken literally, these two formulae are not the same as for satisfiability: rather, the satisfiability P(x,y) \vee Q(f(x)) is the same as that of \exists x,y . P(x,y) \vee Q(f(x)). That free variables are universally quantified is not a consequence of the definition of first-order satisfiability; it is rather used as an implicit common assumption when dealing with clauses.
The only expansion rules that are applicable to a clause are (\forall) and (\vee); these two rules can be replaced by their combination without losing completeness. In particular, the following rule corresponds to applying in sequence the rules (\forall) and (\vee) of the first-order calculus with unification.
(C) \frac{L_1 \vee \cdots \vee L_n}{L_1'|\cdots|L_n'} where L_1' \vee \cdots \vee L_n' is obtained by replacing every variable with a new one in L_1 \vee \cdots \vee L_n
When the set to be checked for satisfiability is only composed of clauses, this and the unification rules are sufficient to prove unsatisfiability. In other worlds, the tableau calculi composed of (C) and (\sigma) is complete.
Since the clause expansion rule only generates literals and never new clauses, the clauses to which it can be applied are only clauses of the input set. As a result, the clause expansion rule can be further restricted to the case where the clause is in the input set.
(C) \frac{L_1 \vee \cdots \vee L_n}{L_1'|\cdots|L_n'} where L_1' \vee \cdots \vee L_n' is obtained by replacing every variable with a
new one in L_1 \vee \cdots \vee L_n, which is a clause of the input set
Since this rule directly exploit the clauses in the input set there is no need to initialize the tableau to the chain of the input clauses. The initial tableau can therefore be initialize with the single node labeled true; this label is often omitted as implicit. As a result of this further simplification, every node of the tableau (apart from the root) is labeled with a literal.
A number of optimizations can be used for clause tableau. These optimization are aimed at reducing the number of possible tableaux to be explored when searching for a closed tableau as described in the "Searching for a closed tableau" section above.
Connection tableau[edit]
Connection is a condition over tableau that forbids expanding a branch using clauses that are unrelated to the literals that are already in the branch. Connection can be defined in two ways:
strong connectedness 
when expanding a branch, use an input clause only if it contains a literal that can be unified with the negation of the literal in the current leaf
weak connectedness 
allow the use of clauses that contain a literal that unifies with the negation of a literal on the branch
Both conditions apply only to branches consisting not only of the root. The second definition allows for the use of a clause containing a literal that unifies with the negation of a literal in the branch, while the first only further constraint that literal to be in leaf of the current branch.
If clause expansion is restricted by connectedness (either strong or weak), its application produces a tableau in which substitution can applied to one of the new leaves, closing its branch. In particular, this is the leaf containing the literal of the clause that unifies with the negation of a literal in the branch (or the negation of the literal in the parent, in case of strong connection).
Both conditions of connectedness lead to a complete first-order calculus: if a set of clauses is unsatisfiable, it has a closed connected (strongly or weakly) tableau. Such a closed tableau can be found by searching in the space of tableaux as explained in the "Searching for a closed tableau" section. During this search, connectedness eliminates some possible choices of expansion, thus reducing search. In other worlds, while the tableau in a node of the tree can be in general expanded in several different ways, connection may allow only few of them, thus reducing the number of resulting tableaux that need to be further expanded.
This can be seen on the following (propositional) example. The tableau made of a chain true - a for the set of clauses \{a, \neg a \vee b, \neg c \vee d, \neg b\} can be in general expanded using each of the four input clauses, but connection only allows the expansion that uses \neg a \vee b. This means that the tree of tableaux has four leaves in general but only one if connectedness is imposed. This means that connectedness leaves only one tableau to try to expand, instead of the four ones to consider in general. In spite of this reduction of choices, the completeness theorem implies that a closed tableau can be found if the set is unsatisfiable.
The connectedness conditions, when applied to the propositional (clausal) case, make the resulting calculus non-confluent. As an example, \{a, b, \neg b\} is unsatisfiable, but applying (C) to a generates the chain true - a, which is not closed and to which no other expansion rule can be applied without violating either strong or weak connectedness. In the case of weak connectedness, confluence holds provided that the clause used for expanding the root is relevant to unsatisfiability, that is, it is contained in a minimally unsatisfiable subset of the set of clauses. Unfortunately, the problem of checking whether a clause meets this condition is itself a hard problem. In spite of non-confluence, a closed tableau can be found using search, as presented in the "Searching for a closed tableau" section above. While search is made necessary, connectedness reduces the possible choices of expansion, thus making search more efficient.
Regular tableaux[edit]
A tableau is regular if no literal occurs twice in the same branch. Enforcing this condition allows for a reduction of the possible choices of tableau expansion, as the clauses that would generate a non-regular tableau cannot be expanded.
These disallowed expansion steps are however useless. If B is a branch containing a literal L, and C is a clause whose expansion violates regularity, then C contains L. In order to close the tableau, one needs to expand and close, among others, the branch where B - L, where L occurs twice. However, the formulae in this branch are exactly the same as the formulae of B alone. As a result, the same expansion steps that close B - L also close B. This means that expanding C was unnecessary; moreover, if C contained other literals, its expansion generated other leaves that needed to be closed. In the propositional case, the expansion needed to close these leaves are completely useless; in the first-order case, they may only affect the rest of the tableau because of some unifications; these can however be combined to the substitutions used to close the rest of the tableau.