Horn-SAT asks whether a conjunction of Horn clauses is satisfiable.
The Horn-SAT forward-chaining algorithm starts with every variable false and repeatedly makes the conclusion of any enabled implication true. It reports failure if it enables a clause with no positive conclusion; otherwise the fixed point is the least satisfying assignment.

Ancestors (9)

  1. Horn clause
  2. Boolean satisfiability problem
  3. NP-completeness
  4. NP-hardness
  5. Polynomial-time many-one reduction
  6. Computational complexity theory
  7. Theoretical computer science
  8. Computer science
  9. Home

View article source

Discussion (0)

New discussion

There are no discussions about this article yet.

Articles by others on the same topic (0)

There are currently no matching articles.
See all articles in the same topic Create my own version