Loading ...
Sorry, an error occurred while loading the content.

Re: AIMA source - Problem in DPLL implmentation

Expand Messages
  • magesmail
    hi, *looks* like it s a bug . I ll look into it (and correct the code ) . Thanks, Ravi
    Message 1 of 5 , Sep 16, 2004
    • 0 Attachment
      hi,
      *looks* like it's a bug . I'll look into it (and correct the code ) .
      Thanks,
      Ravi



      --- In aima-talk@yahoogroups.com, "talk2ravig" <ravindrag@g...> wrote:
      >
      > I was checking out the DPLL implementation in Java. For a small
      > formula having just 2 variables it ran into StackOverflow!! Following
      > is the formula for which I got the error.
      >
      > ((A OR (NOT A)) AND (A OR B))
      >
      > Is this a bug or am I missing something?
      >
      > Thanks,
      > Ravi
    • talk2ravig
      Hi Ravi, Thanks. I did spend little time trying to go through the code to see if there is anything I can fix myself. But haven t been able to give sufficient
      Message 2 of 5 , Sep 17, 2004
      • 0 Attachment
        Hi Ravi,

        Thanks. I did spend little time trying to go through the code to see
        if there is anything I can fix myself. But haven't been able to give
        sufficient time to that.
        Initially I suspected OR statement but found that it happens with
        pure AND statements as well e.g., ((A AND (NOT A)) AND B)

        Regards,
        Ravi


        --- In aima-talk@yahoogroups.com, "magesmail" <magesmail@y...> wrote:
        > hi,
        > *looks* like it's a bug . I'll look into it (and correct the
        code ) .
        > Thanks,
        > Ravi
        >
        >
        >
        > --- In aima-talk@yahoogroups.com, "talk2ravig" <ravindrag@g...>
        wrote:
        > >
        > > I was checking out the DPLL implementation in Java. For a small
        > > formula having just 2 variables it ran into StackOverflow!!
        Following
        > > is the formula for which I got the error.
        > >
        > > ((A OR (NOT A)) AND (A OR B))
        > >
        > > Is this a bug or am I missing something?
        > >
        > > Thanks,
        > > Ravi
      • talk2ravig
        Hi Ravi, I could fix the problem by doing the following changes to the code. Not completely sure whether it breaks something else! In the findPureSymbol()
        Message 3 of 5 , Sep 18, 2004
        • 0 Attachment
          Hi Ravi,

          I could fix the problem by doing the following changes to the code.
          Not completely sure whether it breaks something else!

          In the findPureSymbol() method of the DPLLSatisfiable class before
          returning a new binding (new SymbolValuePair) a check is made (lines
          162 and 166) to ensure that the symbol if present in
          allPositiveSymbols *should not* be present in the allNegativeSymbols
          and the other way. This check was causing the method to return NULL
          for the examples I gave.

          I commented-out the second condition of both the IFs (line 163 and
          167) and it *seems* to have fixed the problem.

          Was there any specific reason this check was in place? Are there any
          negative side-effects of the change proposed above?

          Thanks,
          Ravi


          --- In aima-talk@yahoogroups.com, "magesmail" <magesmail@y...> wrote:
          > hi,
          > *looks* like it's a bug . I'll look into it (and correct the
          code ) .
          > Thanks,
          > Ravi
          >
          >
          >
          > --- In aima-talk@yahoogroups.com, "talk2ravig" <ravindrag@g...>
          wrote:
          > >
          > > I was checking out the DPLL implementation in Java. For a small
          > > formula having just 2 variables it ran into StackOverflow!!
          Following
          > > is the formula for which I got the error.
          > >
          > > ((A OR (NOT A)) AND (A OR B))
          > >
          > > Is this a bug or am I missing something?
          > >
          > > Thanks,
          > > Ravi
        • magesmail
          Hi Ravi (G) , (For those reading these emails there are TWO ravi s here . the person who discovered the bug and solved it is RaviG .The person who maintains
          Message 4 of 5 , Sep 23, 2004
          • 0 Attachment
            Hi Ravi (G) ,
            (For those reading these emails there are TWO ravi's here . the person
            who discovered the bug and solved it is RaviG .The person who
            maintains the code is RaviM .This is RaviM speaking !)

            First I'll address your bug fix and why this may not be adressing the
            true problem . Second, I will explain when you can expect the bug fix
            to occur . Third, I will try to explain how to use the unit tests to
            make sure you don't break anything when you change existing code .

            ****************************
            1.The bug fix you suggested
            *****************************

            First of all, let me congratulate you on your efforts to fix the bug .
            This is HIGHLY appreciated .

            You said ...

            >In the findPureSymbol() method of the DPLLSatisfiable class before
            > returning a new binding (new SymbolValuePair) a check is made (lines
            > 162 and 166) to ensure that the symbol if present in
            > allPositiveSymbols *should not* be present in the allNegativeSymbols
            > and the other way. This check was causing the method to return NULL
            > for the examples I gave.
            >
            > I commented-out the second condition of both the IFs (line 163 and
            > 167) and it *seems* to have fixed the problem.


            The reason why this may NOT be a good fix is that a "pure symbol" by
            definition(see section 7.6 - A complete Backtracking algorithm - page
            221 in my edition ) is a "symbol that ALWAYS appears with the SAME
            sign in all clauses "(emphasis mine). This is why there is a check to
            see that the symbol is present only in one collection.If a symbol is
            present in both positiveSymbols and negativeSymbols it is by
            definition not a pure symbol and hence the check.

            Now , having said that, there is DEFINITELY a deeper bug here, perhaps
            in how symbols are assigned to the collections .I wrote this code a
            year ago and looking at it now i can see how it can be written better .

            I haven't looked at the bug yet (see below for a fuller explanation)
            but WILL be fixing it in the coming days.

            ********************************
            So when can you expect a fix ?
            ********************************

            First, some context .
            I have just sent the second release of the code to Peter who should be
            putting up the code on the aima website soon.This involves a major
            rewrite of the SEARCH code and the addition of some FIRST ORDER logic
            code .Unfortunately, i had left the propositional code (and the
            adversarial search code) untouched for this release which means that
            the bug you pointed out will still be present for this release of the
            code .

            I am now working on release 3 which would involve a rewrite at the
            propositional logic code(and the games code) .In my opinion, the
            prepositional logic code is not as well tested as it should be and i
            will be focussing on this in the coming couple of weeks . I am
            extremely grateful for your bug report. I *guarantee* that this bug
            will be fixed on a priority basis . If you would like a "pre
            release" version of the new code (the code on the website is the
            "official version" ) send a mail to me at magesmail@... and i'll
            do the needful .

            *************************************************************
            How can you change code and be (fairly) sure you haven't broken anything ?
            ****************************************************************

            Short answer : use a TestCase to isolate the bug.This will fail as
            long as the bgug persists . Change code till it passes . Run ALL other
            testcases to make sure you aven't broken anything

            Long answer :




            To check whether evrything works fine after a code change ,
            first ,
            (a)write a new unit test
            and (b) run all the existing unit tests . While the test coverage
            is not 100 % this step gives you some comfort that you haven't broken
            existing functionality.

            The unit tests for DPLLSatisfiable are in class DpllTest .

            (a) add a unit test for eg :
            public void testDpllWorksWithRaviGSentence() {
            String buggySentence = "((A OR (NOT A)) AND (A OR B))";
            assertEquals(true, dpll.isSatisfiable(buggySentence));
            }
            now if you use the junit library(www.junit.org) to run this test, it
            will fail with a heap overflow (this is the bug you reported) . Now
            you can change the code till the heap overflow does not occur when
            you run the test . (remember the test can still fail if the sentence
            you provide is not dpllSatisfiable.This is ok just change the
            assertTrue to assertFalse )

            After this, run all the tests (AllTests.java) with junit.If all the
            tests pass, you will not have broken anything covered by the tests.For
            relase two the test coverage is 70 % of the code ,( up from omething
            like 15 % for release1 ) and will continue to go up for further releases .


            Thanks and regards,

            Ravi Mohan







            --- In aima-talk@yahoogroups.com, "talk2ravig" <ravindrag@g...> wrote:
            > Hi Ravi,
            >
            > I could fix the problem by doing the following changes to the code.
            > Not completely sure whether it breaks something else!
            >
            > In the findPureSymbol() method of the DPLLSatisfiable class before
            > returning a new binding (new SymbolValuePair) a check is made (lines
            > 162 and 166) to ensure that the symbol if present in
            > allPositiveSymbols *should not* be present in the allNegativeSymbols
            > and the other way. This check was causing the method to return NULL
            > for the examples I gave.
            >
            > I commented-out the second condition of both the IFs (line 163 and
            > 167) and it *seems* to have fixed the problem.
            >
            > Was there any specific reason this check was in place? Are there any
            > negative side-effects of the change proposed above?
            >
            > Thanks,
            > Ravi
            >
            >
            > --- In aima-talk@yahoogroups.com, "magesmail" <magesmail@y...> wrote:
            > > hi,
            > > *looks* like it's a bug . I'll look into it (and correct the
            > code ) .
            > > Thanks,
            > > Ravi
            > >
            > >
            > >
            > > --- In aima-talk@yahoogroups.com, "talk2ravig" <ravindrag@g...>
            > wrote:
            > > >
            > > > I was checking out the DPLL implementation in Java. For a small
            > > > formula having just 2 variables it ran into StackOverflow!!
            > Following
            > > > is the formula for which I got the error.
            > > >
            > > > ((A OR (NOT A)) AND (A OR B))
            > > >
            > > > Is this a bug or am I missing something?
            > > >
            > > > Thanks,
            > > > Ravi
          Your message has been successfully submitted and would be delivered to recipients shortly.