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

Re: AIMA source - Problem in DPLL implmentation

Expand Messages
  • 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 1 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 2 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 3 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.