Marking algorithm

The marking algorithm (also underlining algorithm ) is an algorithm for checking Horn formulas for satisfiability . In contrast to general propositional formulas, for which it is assumed that no polynomial time algorithm exists (see satisfiability problem in propositional logic ), a polynomial time algorithm is known with this marking algorithm on the set of Horn formulas, which represent a subset of the propositional formulas (an implementation in linear time is possible).

Horn formulas

→ Main article : Horn formula

Horn formulas are a conjunction of Horn clauses. Horn clauses are special clauses that have at most one positive literal . Horn clauses can also be represented as implications according to the rules of propositional logic . The following table gives an overview of the two possible types of a Horn clause and an example in the form of disjunction and implication.

Type	Disjunction	implication
1	${\displaystyle \neg x_{1}\vee \neg x_{2}\vee \ldots \vee \neg x_{n}}$	${\displaystyle x_{1}\wedge x_{2}\wedge \ldots \wedge x_{n}\rightarrow 0}$
2	${\displaystyle \neg x_{1}\vee \neg x_{2}\vee \ldots \vee \neg x_{n}\vee y}$	${\displaystyle x_{1}\wedge x_{2}\wedge \ldots \wedge x_{n}\rightarrow y}$

The variable can also be 0 for clauses of type 2. In this case, the clause is also called a fact. Horn formulas that only contain clauses of type 1 are trivially satisfiable. By assigning 0 to the variable, the entire statement becomes true. Horn formulas that only have clauses of type 2 can be fulfilled by assigning 1 to all variables. ${\displaystyle n}$

algorithm

Be any Horn formula. The following algorithm indicates whether it can be fulfilled or not. ( Marking means marking every occurrence of a variable in .) ${\displaystyle \phi }$ ${\displaystyle \phi }$ ${\displaystyle \phi }$

• Step 1:
  • If no facts exist:
    • Output "satisfiable".
  • Otherwise:
    • Mark all the facts.
• Step 2:
  • If no clause from type 2 exists, so that all are marked: ${\displaystyle \psi }$ ${\displaystyle \phi }$ ${\displaystyle x_{i}}$
    • Output "satisfiable".
  • If a clause of exists of type 1, so that all are marked: ${\displaystyle \psi }$ ${\displaystyle \phi }$ ${\displaystyle x_{i}}$
    • Output "unsatisfiable".
  • If a clause of exists of type 2, so that all but are not marked y: ${\displaystyle \psi }$ ${\displaystyle \phi }$ ${\displaystyle x_{i}}$
    • Mark A.
    • Go to step 2.
  • Otherwise:
    • Output "satisfiable".

If the algorithm ends with the output satisfiable , you get an assignment that satisfies by assigning true to all marked variables and false to the remaining variables . ${\displaystyle \phi }$

Motivation of the algorithm: The algorithm marks all variables that inevitably have to be assigned true (namely first the variables in the facts, and then in the clauses that represent an implication and where the variables on the left-hand side of the implication are already all with are true ). If there is no contradiction, the formula can be fulfilled.

Web links

• Online Java program that applies the marking algorithm to formulas