To show that a problem is polynomial-time solvable, an often-successful technique is to reduce it to 2SAT (that is the problem of deciding satisfiability of CNF formulas with every clause containing at most 2 literals).

On the other hand, I never seem to have success with reducing problems to Horn SAT (that is the problem for CNFs in which every clause contains at most 1 positive literal). This might not be too surprising given that the algorithm solving Horn SAT is (in some sense) more basic than the one for 2SAT, and because satisfiable Horn formulas have minimal models while most other problems don't.

Nevertheless, are there some examples of problems that are (most naturally) shown to be easy by reduction to Horn SAT?


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.