Horn-satisfiability

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

Horn formulas

Horn formulas are a conjunction of Horn clauses. Horn clauses are specific clauses with at most one positive literal. Horn clauses can be represented as implication 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.

The variable can be for clauses of type 2 also 0. Horn formulas containing only clauses of type 1 are trivially fulfilled. Through the assignment of variables to 0, the entire statement is true. Horn formulas that have only clauses of type 2, can be fulfilled by assigned all the variables with 1.

Algorithm

Be an arbitrary Horn formula. The following algorithm detects whether is satisfiable or not.

Motivation of the algorithm: The algorithm selects all the variables that need to be covered with zwangsläufigerweise true ( namely first the variables in the clauses that consist of only one positive literal, and then in the clauses which constitute an implication, and where the variables on the left side of the implication already are all occupied with true, the variable on the right side. ). If there is no violation, the formula is satisfiable.