Horn-satisfiability

Last updated

In formal logic, Horn-satisfiability, or HORNSAT, is the problem of deciding whether a given set of propositional Horn clauses is satisfiable or not. Horn-satisfiability and Horn clauses are named after Alfred Horn.

Contents

A Horn clause is a clause with at most one positive literal, called the head of the clause, and any number of negative literals, forming the body of the clause. A Horn formula is a propositional formula formed by conjunction of Horn clauses.

Horn satisfiability is actually one of the "hardest" or "most expressive" problems which is known to be computable in polynomial time, in the sense that it is a P-complete problem. [1]

The Horn satisfiability problem can also be asked for propositional many-valued logics. The algorithms are not usually linear, but some are polynomial; see Hähnle (2001 or 2003) for a survey. [2] [3]

Algorithm

The problem of Horn satisfiability is solvable in linear time. [4] The problem of deciding the truth of quantified Horn formulae can be also solved in polynomial time. [5] A polynomial-time algorithm for Horn satisfiability is recursive:

This algorithm also allows determining a truth assignment of satisfiable Horn formulae: all variables contained in a unit clause are set to the value satisfying that unit clause; all other literals are set to false. The resulting assignment is the minimal model of the Horn formula, that is, the assignment having a minimal set of variables assigned to true, where comparison is made using set containment.

Using a linear algorithm for unit propagation, the algorithm is linear in the size of the formula.

Examples

Trivial case

In the Horn formula

(¬a ∨ ¬b ∨ c) ∧
(¬b ∨ ¬c ∨ d) ∧
(¬f ∨ ¬a ∨ b) ∧
(¬e ∨ ¬c ∨ a) ∧
(¬e ∨ f) ∧
(¬d ∨ e) ∧
(¬b ∨ ¬c),

each clause has a negated literal. Therefore, setting each variable to false satisfies all clauses, hence it is a solution.

Solvable case

In the Horn formula

(¬a ∨ ¬b ∨ c) ∧
(¬b ∨ ¬c ∨ f) ∧
(¬f ∨ b) ∧
(¬e ∨ ¬c ∨ a) ∧
(f) ∧
(¬d ∨ e) ∧
(¬b ∨ ¬c),

one clause forces f to be true. Setting f to true and simplifying gives

(¬a ∨ ¬b ∨ c) ∧
(b) ∧
(¬e ∨ ¬c ∨ a) ∧
(¬d ∨ e) ∧
(¬b ∨ ¬c).

Now b must be true. Simplification gives

(¬a ∨ c) ∧
(¬e ∨ ¬c ∨ a) ∧
(¬d ∨ e) ∧
(¬c).

Now it is a trivial case, so the remaining variables can all be set to false. Thus, a satisfying assignment is

a = false,
b = true,
c = false,
d = false,
e = false,
f = true.

Unsolvable case

In the Horn formula

(¬a ∨ ¬b ∨ c) ∧
(¬b ∨ ¬c ∨ f) ∧
(¬f ∨ b) ∧
(¬e ∨ ¬c ∨ a) ∧
(f) ∧
(¬d ∨ e) ∧
(¬b),

one clause forces f to be true. Subsequent simplification gives

(¬a ∨ ¬b ∨ c) ∧
(b) ∧
(¬e ∨ ¬c ∨ a) ∧
(¬d ∨ e) ∧
(¬b).

Now b has to be true. Simplification gives

(¬a ∨ c) ∧
(¬e ∨ ¬c ∨ a) ∧
(¬d ∨ e) ∧
().

We obtained an empty clause, hence the formula is unsatisfiable.

Generalization

A generalization of the class of Horn formulae is that of renamable-Horn formulae, which is the set of formulae that can be placed in Horn form by replacing some variables with their respective negation. Checking the existence of such a replacement can be done in linear time; therefore, the satisfiability of such formulae is in P as it can be solved by first performing this replacement and then checking the satisfiability of the resulting Horn formula. [6] [7] [8] [9] Horn satisfiability and renamable Horn satisfiability provide one of two important subclasses of satisfiability that are solvable in polynomial time; the other such subclass is 2-satisfiability.

Dual-Horn SAT

A dual variant of Horn SAT is Dual-Horn SAT, in which each clause has at most one negative literal. Negating all variables transforms an instance of Dual-Horn SAT into Horn SAT. It was proven in 1951 by Horn that Dual-Horn SAT is in P. [ citation needed ]

See also

Related Research Articles

In logic and computer science, the Boolean satisfiability problem (sometimes called propositional satisfiability problem and abbreviated SATISFIABILITY, SAT or B-SAT) is the problem of determining if there exists an interpretation that satisfies a given Boolean formula. In other words, it asks whether the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. If this is the case, the formula is called satisfiable. On the other hand, if no such assignment exists, the function expressed by the formula is FALSE for all possible variable assignments and the formula is unsatisfiable. For example, the formula "a AND NOT b" is satisfiable because one can find the values a = TRUE and b = FALSE, which make (a AND NOT b) = TRUE. In contrast, "a AND NOT a" is unsatisfiable.

In Boolean logic, a formula is in conjunctive normal form (CNF) or clausal normal form if it is a conjunction of one or more clauses, where a clause is a disjunction of literals; otherwise put, it is a product of sums or an AND of ORs. As a canonical normal form, it is useful in automated theorem proving and circuit theory.

In mathematical logic and logic programming, a Horn clause is a logical formula of a particular rule-like form that gives it useful properties for use in logic programming, formal specification, universal algebra and model theory. Horn clauses are named for the logician Alfred Horn, who first pointed out their significance in 1951.

In computer science, 2-satisfiability, 2-SAT or just 2SAT is a computational problem of assigning values to variables, each of which has two possible values, in order to satisfy a system of constraints on pairs of variables. It is a special case of the general Boolean satisfiability problem, which can involve constraints on more than two variables, and of constraint satisfaction problems, which can allow more than two choices for the value of each variable. But in contrast to those more general problems, which are NP-complete, 2-satisfiability can be solved in polynomial time.

In computational complexity theory, the Cook–Levin theorem, also known as Cook's theorem, states that the Boolean satisfiability problem is NP-complete. That is, it is in NP, and any problem in NP can be reduced in polynomial time by a deterministic Turing machine to the Boolean satisfiability problem.

<span class="mw-page-title-main">Method of analytic tableaux</span>

In proof theory, the semantic tableau is a decision procedure for sentential and related logics, and a proof procedure for formulae of first-order logic. An analytic tableau is a tree structure computed for a logical formula, having at each node a subformula of the original formula to be proved or refuted. Computation constructs this tree and uses it to prove or refute the whole formula. The tableau method can also determine the satisfiability of finite sets of formulas of various logics. It is the most popular proof procedure for modal logics.

The closed-world assumption (CWA), in a formal system of logic used for knowledge representation, is the presumption that a statement that is true is also known to be true. Therefore, conversely, what is not currently known to be true, is false. The same name also refers to a logical formalization of this assumption by Raymond Reiter. The opposite of the closed-world assumption is the open-world assumption (OWA), stating that lack of knowledge does not imply falsity. Decisions on CWA vs. OWA determine the understanding of the actual semantics of a conceptual expression with the same notations of concepts. A successful formalization of natural language semantics usually cannot avoid an explicit revelation of whether the implicit logical backgrounds are based on CWA or OWA.

In mathematical logic and automated theorem proving, resolution is a rule of inference leading to a refutation-complete theorem-proving technique for sentences in propositional logic and first-order logic. For propositional logic, systematically applying the resolution rule acts as a decision procedure for formula unsatisfiability, solving the Boolean satisfiability problem. For first-order logic, resolution can be used as the basis for a semi-algorithm for the unsatisfiability problem of first-order logic, providing a more practical method than one following from Gödel's completeness theorem.

Unit propagation (UP) or Boolean Constraint propagation (BCP) or the one-literal rule (OLR) is a procedure of automated theorem proving that can simplify a set of clauses.

The Davis–Putnam algorithm was developed by Martin Davis and Hilary Putnam for checking the validity of a first-order logic formula using a resolution-based decision procedure for propositional logic. Since the set of valid first-order formulas is recursively enumerable but not recursive, there exists no general algorithm to solve this problem. Therefore, the Davis–Putnam algorithm only terminates on valid formulas. Today, the term "Davis–Putnam algorithm" is often used synonymously with the resolution-based propositional decision procedure that is actually only one of the steps of the original algorithm.

<span class="mw-page-title-main">DPLL algorithm</span> Type of search algorithm

In logic and computer science, the Davis–Putnam–Logemann–Loveland (DPLL) algorithm is a complete, backtracking-based search algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e. for solving the CNF-SAT problem.

MAX-3SAT is a problem in the computational complexity subfield of computer science. It generalises the Boolean satisfiability problem (SAT) which is a decision problem considered in complexity theory. It is defined as:

In computational complexity theory, the maximum satisfiability problem (MAX-SAT) is the problem of determining the maximum number of clauses, of a given Boolean formula in conjunctive normal form, that can be made true by an assignment of truth values to the variables of the formula. It is a generalization of the Boolean satisfiability problem, which asks whether there exists a truth assignment that makes all clauses true.

In mathematical logic, a tautology is a formula or assertion that is true in every possible interpretation. An example is "x=y or x≠y". Similarly, "either the ball is green, or the ball is not green" is always true, regardless of the colour of the ball.

In computational complexity theory, a branch of computer science, Schaefer's dichotomy theorem, proved by Thomas Jerome Schaefer, states necessary and sufficient conditions under which a finite set S of relations over the Boolean domain yields polynomial-time or NP-complete problems when the relations of S are used to constrain some of the propositional variables. It is called a dichotomy theorem because the complexity of the problem defined by S is either in P or is NP-complete, as opposed to one of the classes of intermediate complexity that is known to exist by Ladner's theorem.

In computational complexity theory, the language TQBF is a formal language consisting of the true quantified Boolean formulas. A (fully) quantified Boolean formula is a formula in quantified propositional logic where every variable is quantified, using either existential or universal quantifiers, at the beginning of the sentence. Such a formula is equivalent to either true or false. If such a formula evaluates to true, then that formula is in the language TQBF. It is also known as QSAT.

MAXEkSAT is a problem in computational complexity theory that is a maximization version of the Boolean satisfiability problem 3SAT. In MAXEkSAT, each clause has exactly k literals, each with distinct variables, and is in conjunctive normal form. These are called k-CNF formulas. The problem is to determine the maximum number of clauses that can be satisfied by a truth assignment to the variables in the clauses.

In computer science, the Sharp Satisfiability Problem is the problem of counting the number of interpretations that satisfy a given Boolean formula, introduced by Valiant in 1979. In other words, it asks in how many ways the variables of a given Boolean formula can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. For example, the formula is satisfiable by three distinct boolean value assignments of the variables, namely, for any of the assignments, , and, we have

In computer science, conflict-driven clause learning (CDCL) is an algorithm for solving the Boolean satisfiability problem (SAT). Given a Boolean formula, the SAT problem asks for an assignment of variables so that the entire formula evaluates to true. The internal workings of CDCL SAT solvers were inspired by DPLL solvers. The main difference between CDCL and DPLL is that CDCL's backjumping is non-chronological.

<span class="mw-page-title-main">Planar SAT</span>

In computer science, the planar 3-satisfiability problem (abbreviated PLANAR 3SAT or PL3SAT) is an extension of the classical Boolean 3-satisfiability problem to a planar incidence graph. In other words, it asks whether the variables of a given Boolean formula—whose incidence graph consisting of variables and clauses can be embedded on a plane—can be consistently replaced by the values TRUE or FALSE in such a way that the formula evaluates to TRUE. If this is the case, the formula is called satisfiable. On the other hand, if no such assignment exists, the function expressed by the formula is FALSE for all possible variable assignments and the formula is unsatisfiable. For example, the formula "a AND NOT b" is satisfiable because one can find the values a = TRUE and b = FALSE, which make (a AND NOT b) = TRUE. In contrast, "a AND NOT a" is unsatisfiable.

References

  1. ↑ Stephen Cook; Phuong Nguyen (2010). Logical foundations of proof complexity. Cambridge University Press. p. 224. ISBN   978-0-521-51729-4. (Author's 2008 draft version, see p.213f)
  2. ↑ Reiner Hähnle (2001). "Advanced many-valued logics". In Dov M. Gabbay, Franz Günthner (ed.). Handbook of philosophical logic. Vol. 2 (2nd ed.). Springer. p. 373. ISBN   978-0-7923-7126-7.
  3. ↑ Reiner Hähnle (2003). "Complexity of Many-valued Logics". In Melvin Fitting, Ewa Orłowska (ed.). Beyond two: theory and applications of multiple-valued logic. Springer. ISBN   978-3-7908-1541-2.
  4. ↑ Dowling, William F.; Gallier, Jean H. (1984), "Linear-time algorithms for testing the satisfiability of propositional Horn formulae", Journal of Logic Programming, 1 (3): 267–284, doi: 10.1016/0743-1066(84)90014-1 , MR   0770156
  5. ↑ Buning, H.K.; Karpinski, Marek; Flogel, A. (1995). "Resolution for Quantified Boolean Formulas". Information and Computation. Elsevier. 117 (1): 12–18. doi: 10.1006/inco.1995.1025 .
  6. ↑ Lewis, Harry R. (1978). "Renaming a set of clauses as a Horn set". Journal of the ACM . 25 (1): 134–135. doi: 10.1145/322047.322059 . MR   0468315..
  7. ↑ Aspvall, Bengt (1980). "Recognizing disguised NR(1) instances of the satisfiability problem". Journal of Algorithms. 1 (1): 97–103. doi:10.1016/0196-6774(80)90007-3. MR   0578079.
  8. ↑ Hébrard, Jean-Jacques (1994). "A linear algorithm for renaming a set of clauses as a Horn set". Theoretical Computer Science . 124 (2): 343–350. doi:10.1016/0304-3975(94)90015-9. MR   1260003..
  9. ↑ Chandru, Vijaya; Collette R. Coullard; Peter L. Hammer; Miguel Montañez; Xiaorong Sun (2005). "On renamable Horn and generalized Horn functions". Annals of Mathematics and Artificial Intelligence. 1 (1–4): 33–47. doi:10.1007/BF01531069.

Further reading

This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.