DPLL算法和访问节点数

Question

我正在实现DPLL算法来计算访问节点的数量。我设法实现了不计算访问节点的DPLL，但我想不出任何计算问题的解决方案。主要的问题是，当算法找到满意的评估并返回True时，递归从递归开始的那一刻开始卷起并返回计数器。在任何命令式语言中，我只会使用全局变量并在函数调用后尽快增加它，但在Haskell中并非如此。

我粘贴在这里的代码并不代表我试图解决计数问题，它只是我没有它的解决方案。我尝试使用诸如（True，Int）的元组，但它始终会在递归开始时返回整数值。

这是我的实现其中（节点 - >变量）是一个启发式函数，Sentence是CNF中的子句列表以满足，[变量]是未分配的文字列表，模型只是一个真值计算。

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 

我真的很感激任何关于如何计算访问节点的建议。谢谢。

编辑：

我允许使用的唯一库是System.Random，Data.Maybe和Data.List模块。

编辑：

的一种可能的解决方案，我试图执行是使用一个元组（BOOL，INT），其从DPPL函数返回值。该代码如下所示：

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) 

此方法的基本思想是在每次递归调用时递增计数器。但是，这种方法的问题是我不知道如何从OR语句中的递归调用中检索计数器。我甚至不确定这在Haskell中是否可行。

Answer 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) 

这是State monad的手动实现。但是，我不清楚你为什么要通过柜台。只需返回它。然后它是更简单的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 - 和调用函数会更简单，用一个少争论担心正确设置。

Answer 2

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

这可以进一步使用state monad优雅地重新表达。一般来说，haskell和state monad的教程非常好，是here。基本上a -> b到a -> Int -> (b, Int)的转换可以看作是a -> b到a -> State Int b的转换，只需给函数Int -> (b, Int)一个更好的名称即可。有一个非常好的blog，解释这些很好的抽象来自一个非常方便的方式。

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'