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

Re: AIMA source - Problem in DPLL implmentation

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