5 kyu

Propositional SAT Problem

Description
Loading description...
Logic
Mathematics
Algorithms
  • Please sign in or sign up to leave a comment.
  • Voile Avatar

    Sample test needs to be updated:

    • It does not tell any useful information like the actual tests do
    • The last line is wrong: test.expect(m4 == {p} or m2 == {q} or m2 == {p, q}) should be test.expect(m4 == {p} or m4 == {q} or m4 == {p, q})
  • Voile Avatar

    name: string that represents the literal. Two literals with the same name are the same literal.

    Then Literal's __eq__ should be defined to allow this. Currently Literal('p') == Literal('p') gives False. Only every same-named instance in the input formula is equal to each other.

    • Dr Gabo Avatar

      Definitely an issue. Fixed it!

      Issue marked resolved by Dr Gabo 5 years ago
    • Blind4Basics Avatar

      warning: you need then to actually implement hash in the same way. For now, it works for the only same reason, but if you fixe the behavior for one, you have to fix it for the other too.

    • Voile Avatar

      __hash__? ;-)

    • Dr Gabo Avatar

      Don't worry, I also implemented the hash function accordingly.

    • Blind4Basics Avatar

      @Voile: ofc. ('didn't think I'd have to be blatant about that... ;p )

      @DrGabo: not good enough: you actually need to implement both functions for both classes. And to have something efficient enough, you'll need to store the string representation as a property, so that the hash won't become too much time cosuming

    • Dr Gabo Avatar

      To be honest, I don't know how I feel about defining equality for complex formulas, since I have to ignore commutativity and associativity to make an effective implementation. I did it for consistency reasons by comparing the string representation (it should be correct), but I'm not quite sure if it's for the best :/

    • Blind4Basics Avatar

      True. But considering that you're the one buildigng the trees, you can guarantee the consistency about that. :)

  • Blind4Basics Avatar

    Hi again,

    IMO, there's something fishy. Either in the description, or in the conception of the task ;o

    How are we supposed to use the formula instances? I'd assume a meaningful implementation of those would provide getters for leaves/values too. Like left/right/child for AND, OR and NEG, and symbol or something like that for the litterals. Do, there is no such things... Meaning for now, the only idea that comes to my mind is to print the formula and parse the string... Which seems pretty unnecessary/uninteresting thing here, considering we are provided with a tree in the first place... I'd honestly be tempted to hack the Formula class to solve the kata... :p

    Am I missing something?

    • Blind4Basics Avatar

      well, see my solution. I find the setup of your kata pretty weird... :o (but that's interesting)

    • Blind4Basics Avatar

      oh god... :/ I totally missed the description of args, actually... :/ But I'm not surprised I forgot about it: you didn't actually tell what it was (-> a list of children nodes)

    • Dr Gabo Avatar

      I didn't want to use that terminology (children nodes) because operands or subformulae are the accepted names in the field, but I will add a clarification to make it more clear.

      I'm glad you could solve it :)

      Question marked resolved by Dr Gabo 5 years ago
    • Blind4Basics Avatar

      especially, make it perfectly clear that this list can have any length (and/or operators!)

  • Blind4Basics Avatar

    Hi,

    • litteral should be is_litteral or the equivalent getter
    • since Litteral class does have only 1 single field, the Formula class should extend the Litteral one, not the opposite, shouldn't it?
  • Avanta Avatar

    In the sample test, I'd recommend putting each test immediately after the user's solution is computed. This makes it easier to for debugging / logging values, as each function call is grouped separately.