Boolean formula: part2

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|

Boolean formula: part2

Dmitry Bogatov
Hello!  I have following code:

buildFormulas :: [Variable] -> Int -> [Formula]
buildFormulas vars 0 = map Var vars
buildFormulas vars n = join $
    forM [0 .. n - 1 ] $ \i -> do
        x <- buildFormulas vars i
        y <- buildFormulas vars (n - i - 1)
        z <- buildFormulas vars (n - 1)
        let t1 = case z of
              (Negation _) -> []
              _ -> [Negation z]
        t1 ++ [conj x y, impl x y, disj x y]

It is correct, typechecks, but it is insanely slow (calculating
take 35 (buildFormulas [P, Q, R] 5) hangs my computer).

My guess is that it builds too much before returning first results.
Can you suggest more efficent way enumerate formulas of set of variables?




--
Best regards, Dmitry Bogatov <[hidden email]>,
Free Software supporter, esperantisto and netiquette guardian.
GPG: 54B7F00D

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

attachment0 (853 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Boolean formula: part2

Dmitry Bogatov
* Dmitry Bogatov <[hidden email]> [2014-09-17 23:48:49+0400]
Sorry for followup, I found that problem is not in this function per-se,
but in filtering one. Since I require formula to be complicated enough,
I have to filter out simple ones, and simple ones gets constructed
before any more complicated. I get all formulas only about P before
it even touches Q. How can I speed things up?

-- Set of hacks, that tries to formalize my opinion what
-- good formula is.
goodFormula :: Formula -> Bool
goodFormula = \case
  (Function2 t x y) -> x /= y && goodFormula x && goodFormula y
                       && case (x, y) of
                           (Negation u, Negation v) -> u /= v
                           (Negation u, y) -> u /= y
                           (x, Negation v) -> x /=v
                           (Function2 t' u' v', _) -> t' /= t' || ((y /= u') && (y /= v'))
                           _ -> True
  (Negation x) -> goodFormula x
  _ -> True

flenght :: Formula -> Int
flenght fmt = case value fmt of
  Right _ -> 0
  Left l -> length (toList l)

main = do
  -- mapM_ print $ take  (buildFormulas [P, Q, R] 7)
  print $ filter (\f -> goodFormula f && flenght f == 3) (buildFormulas [P, Q, R] 4) !! 1
  -- print $ (buildFormulas [P, Q, R] 5) !! 1

> Hello!  I have following code:
>
> buildFormulas :: [Variable] -> Int -> [Formula]
> buildFormulas vars 0 = map Var vars
> buildFormulas vars n = join $
>     forM [0 .. n - 1 ] $ \i -> do
>         x <- buildFormulas vars i
>         y <- buildFormulas vars (n - i - 1)
>         z <- buildFormulas vars (n - 1)
>         let t1 = case z of
>               (Negation _) -> []
>               _ -> [Negation z]
>         t1 ++ [conj x y, impl x y, disj x y]
>
> It is correct, typechecks, but it is insanely slow (calculating
> take 35 (buildFormulas [P, Q, R] 5) hangs my computer).
>
> My guess is that it builds too much before returning first results.
> Can you suggest more efficent way enumerate formulas of set of
> variables?




--
Best regards, Dmitry Bogatov <[hidden email]>,
Free Software supporter, esperantisto and netiquette guardian.
GPG: 54B7F00D

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe

attachment0 (853 bytes) Download Attachment