satisfiability provide one of two important subclasses of satisfiability that are solvable in polynomial time; the other such subclass is 2-satisfiability. 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. 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. See also Unit propagation Boolean satisfiability problem 2-satisfiability References Further reading Logic in computer science P-complete problems Satisfiability problems