0

I'm implementing DPLL algorithm that counts the number of visited nodes. I managed to implement DPLL that doesn't count visited nodes but I can't think of any solutions to the problem of counting. The main problem is that as the algorithm finds satisfying valuation and returns True, the recursion rolls up and returns counter from the moment the recursion started. In any imperative language I would just use global variable and increment it as soon as function is invoked, but it is not the case in Haskell.

The code I pasted here does not represent my attempts to solve the counting problem, it is just my solution without it. I tried to use tuples such as (True,Int) but it will always return integer value from the moment the recursion started.

This is my implementation where (Node -> Variable) is a heuristic function, Sentence is list of clauses in CNF to be satisfied, [Variable] is a list of Literals not assigned and Model is just a truth valuation.

dpll' :: (Node -> Variable) -> Sentence -> [Variable] -> Model -> Bool
dpll' heurFun sentence vars model
  | satisfiesSentence model sentence  = True
  | falsifiesSentence model sentence  = False
  | otherwise         = applyRecursion
    where
      applyRecursion
        | pureSymbol /= Nothing = recurOnPureSymbol
        | unitSymbol /= Nothing = recurOnUnitSymbol
        | otherwise             = recurUsingHeuristicFunction
          where
            pureSymbol  = findPureSymbol vars sentence model
            unitSymbol  = findUnitClause sentence model
            heurVar = heurFun (sentence,(vars,model))
            recurOnPureSymbol =
              dpll' heurFun sentence (vars \\ [getVar pureSymbol]) ((formAssignment pureSymbol):model)
            recurOnUnitSymbol =
              dpll' heurFun sentence (vars \\ [getVar unitSymbol]) ((formAssignment unitSymbol):model)
            recurUsingHeuristicFunction = case vars of
              (v:vs) ->     (dpll' heurFun sentence (vars \\ [heurVar]) ((AS (heurVar,True)):model)
                        ||   dpll' heurFun sentence (vars \\ [heurVar]) ((AS (heurVar,False)):model))
              []     ->     False

I would really appreciate any advice on how to count the visited nodes. Thank you.

EDIT:

The only libraries I'm allowed to use are System.Random, Data.Maybe and Data.List.

EDIT:

One possible solution I tried to implement is to use a tuple (Bool,Int) as a return value from DPPL function. The code looks like:

dpll'' :: (Node -> Variable) -> Sentence -> [Variable] -> Model -> Int -> (Bool,Int)
dpll'' heurFun sentence vars model counter
  | satisfiesSentence model sentence  = (True,counter)
  | falsifiesSentence model sentence  = (False,counter)
  | otherwise         = applyRecursion
  where
    applyRecursion
      | pureSymbol /= Nothing = recurOnPureSymbol
      | unitSymbol /= Nothing = recurOnUnitSymbol
      | otherwise             = recurUsingHeuristicFunction
      where
        pureSymbol  = findPureSymbol vars sentence model
        unitSymbol  = findUnitClause sentence model
        heurVar = heurFun (sentence,(vars,model))
        recurOnPureSymbol =
          dpll'' heurFun sentence (vars \\ [getVar pureSymbol]) ((formAssignment pureSymbol):model) (counter + 1)
        recurOnUnitSymbol =
          dpll'' heurFun sentence (vars \\ [getVar unitSymbol]) ((formAssignment unitSymbol):model) (counter + 1)
        recurUsingHeuristicFunction = case vars of
          (v:vs)    ->    ((fst $ dpll'' heurFun sentence (vars \\ [heurVar]) ((AS (heurVar,True)):model) (counter + 1))
                      ||  (fst $ dpll'' heurFun sentence (vars \\ [heurVar]) ((AS (heurVar,False)):model) (counter + 1)),counter)
          []        -> (False,counter)

The basic idea of this approach is to increment the counter at each recursive call. However, the problem with this approach is that I have no idea how to retrieve counter from recursive calls in OR statement. I'm not even sure if this is possible in Haskell.

4

2 回答 2

1

case您可以使用或类似方法从递归调用中检索计数器。

recurUsingHeuristicFunction = case vars of
    v:vs -> case dpll'' heurFun sentence (vars \\ [heurVar]) (AS (heurVar,True):model) (counter + 1) of
        (result, counter') -> case dpll'' heurFun sentence (vars \\ [heurVar]) (AS (heurVar,False):model) counter' of
            (result', counter'') -> (result || result', counter'')
    []   -> (False,counter)

这是Statemonad 的手动实现。但是，我不清楚你为什么要经过柜台。就退货吧。然后它是更简单的Writer单子。这个助手的代码看起来像这样：

recurUsingHeuristicFunction = case vars of
    v:vs -> case dpll'' heurFun sentence (vars \\ [heurVar]) (AS (heurVar,True):model) of
        (result, counter) -> case dpll'' heurFun sentence (vars \\ [heurVar]) (AS (heurVar,False):model) of
            (result', counter') -> (result || result', counter + counter' + 1)
    []   -> (False,0)

其他结果将是类似的——返回0而不是counter和1而不是counter+1——并且对函数的调用会更简单，只需少一个参数来担心正确设置。

于 2017-03-13T21:56:39.790 回答
0

基本上你在命令式语言中描述为你的解决方案可以通过传递一个计数变量来建模，在你返回它时将变量添加到结果中（达到可满足赋值的递归底部），即a -> b你将创建的函数一个新功能a -> Int -> (b, Int)。参数是计数器的Int当前状态，结果丰富了计数器的更新状态。

这可以进一步使用state monad优雅地重新表达。一个非常好的关于 haskell 和 state monad 的教程在这里。基本上 to 的转换a -> b可以a -> Int -> (b, Int)看作是a -> bintoa -> State Int b的转换，只需给函数一个更好的名称即可Int -> (b, Int)。有一个非常好的博客以一种非常容易理解的方式解释了这些好的抽象来自哪里。

import Control.Monad.Trans.StateT

type Count = Int

dpllM :: (Node -> Variable) -> Sentence -> [Variable] -> Model -> State Count Bool
dpllM heurFun sentence vars model | ... = do
    -- do your thing
    modify (+1)
    -- do your thing

dpll' :: (Node -> Variable) -> Sentence -> [Variable] -> Model -> Bool
dpll' heurFun sentence vars model = runState (dpllM heurFun sentence vars model) 0

也许你想要类似的东西

f :: A -> Int -> (Bool, Int)
f a c =
    let a' = ...
        a'' = ...
        (b', c') = f a' c in f a'' c'
于 2017-03-13T20:13:58.800 回答