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

AIMA source - Problem in DPLL implmentation

Expand Messages
  • talk2ravig
    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
    Message 1 of 5 , Sep 15, 2004
    • 0 Attachment
      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, *looks* like it s a bug . I ll look into it (and correct the code ) . Thanks, Ravi
      Message 2 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 3 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 4 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 5 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.