Unified resolution

Unit resolution ( English unit propagation ) is a procedure in mathematical logic to simplify a set of clauses . In order to be able to apply a unit resolution, a so-called unit clause must be contained in the given set of clauses. A unitary clause is a clause that consists of only a single literal ; H. either from a variable or the negation of a variable. Unit resolution is used in the DPLL algorithm , among others , and is an important component of many SAT solvers .

method

Given a set of clauses with a unit clause . Then one simplifies the other clauses from the given set of clauses by two rules: ${\displaystyle \psi }$

1. Remove all clauses that contain (the standard clause itself is not removed). ${\displaystyle \psi }$
2. If a clause contains, remove that literal from the clause. ${\displaystyle \neg \psi }$

The simplified set of clauses is then logically equivalent to the original set of clauses.

Sometimes it is sufficient to generate a set of clauses that are equivalent to satisfiability . In this case, the first step is to remove the unit clause itself from the set of clauses.

In both cases, the new clauses are the logical consequences of the original set of clauses.

example

The following set of clauses is given:

${\displaystyle \{a\vee c,\neg c,b\vee c,a\vee \neg c\}}$

In this set of clauses there is a unit clause . If the clause were contained in the clause set, this would also be a unit clause. This set of clauses can be simplified by applying these two rules, where is the unitary clause . The result is the set of clauses: ${\displaystyle \neg c}$ ${\displaystyle c}$ ${\displaystyle \neg c}$

${\displaystyle \{a,b,\neg c\}}$

All clauses that contained were completely removed from the clause set. That was the clause . In addition, the literal has been removed from all clauses. This was done in the remaining two clauses and . The standard clause must be retained, otherwise the truthfulness of the statement would change. ${\displaystyle \neg c}$ ${\displaystyle a\vee \neg c}$ ${\displaystyle c}$ ${\displaystyle a\vee c}$ ${\displaystyle b\vee c}$

Correctness of the single resolution

Be clauses in which the single clause does not appear. Furthermore, there are clauses in which occurs and clauses in which occurs. ${\displaystyle \varphi =\varphi _{1}...\varphi _{n}}$ ${\displaystyle a}$ ${\displaystyle (\psi _{1}\vee a)...(\psi _{n}\vee a)}$ ${\displaystyle a}$ ${\displaystyle (\tau _{1}\vee \neg a)...(\tau _{n}\vee \neg a)}$ ${\displaystyle \neg a}$

If the antecendent is now , then the conjunction of the subsequent must be a semantic model of the conjunction of the antecedent. In other words: ${\displaystyle A=\{\varphi _{1},...,\varphi _{n},(\psi _{1}\vee a),...,(\psi _{n}\vee a),(\tau _{1}\vee \neg a),...,(\tau _{n}\vee \neg a),a\}}$ ${\displaystyle S=\{\varphi _{1},...,\varphi _{n},(\tau _{1}\vee \neg a),...,(\tau _{n}\vee \neg a),a\}}$ ${\displaystyle \textstyle A\vdash S\Rightarrow \bigwedge _{a\in A}a\models \bigwedge _{s\in S}s}$

Case : ${\displaystyle a=\perp }$

${\displaystyle \varphi \land (\psi _{1}\vee a)\land ...\land (\psi _{n}\vee a)\land (\tau _{1}\vee \neg a)\land ...\land (\tau _{n}\vee \neg a)\land a\;\equiv \;\perp \;\equiv \;\varphi \land \tau _{1}\land ...\land \tau _{n}\land a}$

because of ${\displaystyle \varphi \land \perp \equiv \perp }$

Case : ${\displaystyle a=\top }$

${\displaystyle \varphi \land (\psi _{1}\lor a)\land ...\land (\psi _{n}\lor a)\land (\tau _{1}\lor \neg a)\land ...\land (\tau _{n}\lor \neg a)\land a}$

${\displaystyle \equiv \varphi \land (\psi _{1}\lor \top )\land ...\land (\psi _{n}\lor \top )\land (\tau _{1}\lor \perp )\land ...\land (\tau _{n}\lor \perp )\land a}$

${\displaystyle \equiv \varphi \land \top \land ...\land \top \land \tau _{1}\land ...\land \tau _{n}\land a}$

${\displaystyle \equiv \varphi \land \tau _{1}\land ...\land \tau _{n}\land a}$

Comparison with resolution

• The second step of the unified resolution can be interpreted as a special case of resolution . Here one looks at a uniform clause and calculates all possible resolvents from this uniform clause. In the case of a single resolution, however, in contrast to the resolution procedure, the original clauses are discarded as soon as a simplified clause is formed.

• The first step of the unit resolution has no equivalent in the resolution process. In particular, in the resolution procedure only clauses are added, but clauses are never discarded.

• The resolution procedure is complete in the sense that it either shows or refutes the satisfiability of every propositional formula. In general, this does not apply to unit resolutions. However, the unit resolution is a complete procedure for the satisfiability of Horn formulas if it is applied iteratively for new unit clauses.

See also

• Resolution (logic)
• Calculus
• Horn formula
• Marking Algorithm - A related algorithm to test the satisfiability of Horn formulas.