# Thread: Can anyone help me make a directed graph for this algorithm?

1. Show how to implement the stingy algorithm for Horn formula satisfiability in time that is linear in length of the formula (the no. of occurrences of literals in it.)
Use a directed graph, with one node per variable to represent the implications.)
(This is exercise 5.32 in the book Algorithms byS. Dasgupta, C.H. Papadimitriou, and U.V. Vazirani)Below is an efficient algorithm I got from Logic for Computer Scientists/Propositional Logic/Horn clauses - Wikibooks, open books for an open world that is O(l).
Deciding Satisfiability of Horn Formulae
1. If there is a subformula of the kind label every occurrence of A in F.
2. Apply the following rules until none of them is applicable:
• If is a subformula and are all labeled and B is not labeled then label every occurrence of B in F.
• If is a subformula and are all labeled then Stop: Unsatisfiable
3. Stop: Satisfiable The assignment iff A is labeled is a model.

2.

3. It looks like homework. Is it?

4. yup.. its a very hard homework.. we were never taught on how to make directed graphs...

 Bookmarks
##### Bookmarks
 Posting Permissions
 You may not post new threads You may not post replies You may not post attachments You may not edit your posts   BB code is On Smilies are On [IMG] code is On [VIDEO] code is On HTML code is Off Trackbacks are Off Pingbacks are Off Refbacks are On Terms of Use Agreement