Posted by Moonfruit

Announcements | Last Post | |
---|---|---|

SoC Curricula | 09/30/2017 01:08PM | |

Demarcation or scoping of examinations and assessment | 02/13/2017 07:59AM | |

School of Computing Short Learning Programmes | 11/24/2014 08:37AM | |

Unisa contact information | 07/28/2011 01:28PM |

Horn Formula March 18, 2008 03:37PM |
Registered: 12 years ago Posts: 18 Rating: 0 |

Re: Horn Formula March 21, 2008 03:51PM |
Registered: 13 years ago Posts: 39 Rating: 0 |

Marking it means exactly that. Write out the formula, in full on paper, and when the algorithm tells you to mark a clause, do so either by placing a tick above that clause, or underlining it, or highlighting, you get the idea.

For example, take the formula (p_{2} ^ p_{3} ^ p_{5} -> p_{13}) ^ (T -> p_{5}) ^ (p_{5} ^ p_{11} -> _). T stands for tautology, and _ for contradiction, else have a look at the third equation on page 66 if my symbology makes no sense to you.

Right, step 1 says mark all T's, so after this step, our equations looks as follows:

(p_{2} ^ p_{3} ^ p_{5} -> p_{13}) ^ (__T__ -> p_{5}) ^ (p_{5} ^ p_{11} -> _)

Step 2 says (in essence) that if everything on the left-hand side of -> is marked, then mark the right-hand side too.

So, now our formula look like this

(p_{2} ^ p_{3} ^ p_{5} -> p_{13}) ^ (__T -> p___{5}) ^ (p_{5} ^ p_{11} -> _)

Reading the fine print under the description of the algorithm in the book ,we see that if you mark p_{5} in one place, then ALL p_{5}'s must be marked. So:

(p_{2} ^ p_{3} ^ __p___{5} -> p_{13}) ^ (__T -> p___{5}) ^ (__p___{5} ^ p_{11} -> _)

Step 3 says as soon as step 2 can no longer be repeated (and if no _'s are marked), move to step 4.

In step 4, _ is not marked, so we exit the algorithm as satisfiable. If p_{11} was marked though, then we would have had an unsatisfiable formula.

There you go! This is how I interpret it. If I'm wrong, hopefully someone else will point out my misunderstanding, else I hope this helps you...

Now, you can kindly return the favour and help me out on my query, which I'll post in the next 5 minutes

For example, take the formula (p

Right, step 1 says mark all T's, so after this step, our equations looks as follows:

(p

Step 2 says (in essence) that if everything on the left-hand side of -> is marked, then mark the right-hand side too.

So, now our formula look like this

(p

Reading the fine print under the description of the algorithm in the book ,we see that if you mark p

(p

Step 3 says as soon as step 2 can no longer be repeated (and if no _'s are marked), move to step 4.

In step 4, _ is not marked, so we exit the algorithm as satisfiable. If p

There you go! This is how I interpret it. If I'm wrong, hopefully someone else will point out my misunderstanding, else I hope this helps you...

Now, you can kindly return the favour and help me out on my query, which I'll post in the next 5 minutes

Re: Horn Formula April 25, 2008 09:22AM |
Registered: 14 years ago Posts: 88 Rating: 0 |

Re: Horn Formula April 25, 2008 09:32AM |
Registered: 13 years ago Posts: 39 Rating: 0 |

Re: Horn Formula April 25, 2008 10:18AM |
Registered: 14 years ago Posts: 88 Rating: 0 |

sorry,

u wrote "In step 4, _ is not marked, so we exit the algorithm as satisfiable. If p11 was marked though, then we would have had an unsatisfiable formula."

according to what i've marked, p11 was not marked, then we have satisfiable formula, so my quetion is, how come the book says we have unsatisfiable formula?

u wrote "In step 4, _ is not marked, so we exit the algorithm as satisfiable. If p11 was marked though, then we would have had an unsatisfiable formula."

according to what i've marked, p11 was not marked, then we have satisfiable formula, so my quetion is, how come the book says we have unsatisfiable formula?

Re: Horn Formula April 25, 2008 10:43AM |
Registered: 13 years ago Posts: 39 Rating: 0 |

Where does the book say it's unsatisfiable? I'm looking on pg 66. The first three equations are Horm formulas, the following four are not.

THe algorithm...

1. It marks if it occurs in that list.

2. If there is a conjunct P1 Ã¢Ë†Â§ P2 Ã¢Ë†Â§ Ã‚Â· Ã‚Â· Ã‚Â· Ã¢Ë†Â§ Pki Ã¢â€ â€™ P of Ãâ€ such that all Pj with 1 Ã¢â€°Â¤ j Ã¢â€°Â¤ ki are marked, mark P as well and go to 2. Otherwise (= there is no conjunct

P1 Ã¢Ë†Â§ P2 Ã¢Ë†Â§ Ã‚Â· Ã‚Â· Ã‚Â· Ã¢Ë†Â§ Pki Ã¢â€ â€™ P such that all Pj are marked) go to 3.

3. If Ã¢Å Â¥ is marked, print out Ã¢â‚¬ËœThe Horn formula Ãâ€ is unsatisfiable.Ã¢â‚¬â„¢ and stop. Otherwise,

go to 4.

4. Print out Ã¢â‚¬ËœThe Horn formula Ãâ€ is satisfiable.Ã¢â‚¬â„¢ and stop.

Step 3 says if Ã¢Å Â¥ is marked (which in our example it isn't), print unsatisifiable Otherwise goto 4. So, we go to 4

Step 4 says: Satisfiable

Am I missing something?

THe algorithm...

1. It marks if it occurs in that list.

2. If there is a conjunct P1 Ã¢Ë†Â§ P2 Ã¢Ë†Â§ Ã‚Â· Ã‚Â· Ã‚Â· Ã¢Ë†Â§ Pki Ã¢â€ â€™ P of Ãâ€ such that all Pj with 1 Ã¢â€°Â¤ j Ã¢â€°Â¤ ki are marked, mark P as well and go to 2. Otherwise (= there is no conjunct

P1 Ã¢Ë†Â§ P2 Ã¢Ë†Â§ Ã‚Â· Ã‚Â· Ã‚Â· Ã¢Ë†Â§ Pki Ã¢â€ â€™ P such that all Pj are marked) go to 3.

3. If Ã¢Å Â¥ is marked, print out Ã¢â‚¬ËœThe Horn formula Ãâ€ is unsatisfiable.Ã¢â‚¬â„¢ and stop. Otherwise,

go to 4.

4. Print out Ã¢â‚¬ËœThe Horn formula Ãâ€ is satisfiable.Ã¢â‚¬â„¢ and stop.

Step 3 says if Ã¢Å Â¥ is marked (which in our example it isn't), print unsatisifiable Otherwise goto 4. So, we go to 4

Step 4 says: Satisfiable

Am I missing something?

Re: Horn Formula April 25, 2008 11:09AM |
Registered: 14 years ago Posts: 88 Rating: 0 |

Sorry, only registered users may post in this forum.