DPLL算法和访问节点数

Question

我正在实施 DPLL 算法来计算访问节点的数量。我设法实现了不计算访问节点的 DPLL，但我想不出任何解决计数问题的方法。主要问题是，当算法找到令人满意的估值并返回 True 时，递归从递归开始的那一刻起就向上滚动并返回计数器。在任何命令式语言中，我都会使用全局变量并在调用函数时立即递增它，但在 Haskell 中并非如此。

我在这里粘贴的代码并不代表我尝试解决计数问题，这只是我没有它的解决方案。我尝试使用 (True,Int) 之类的元组，但它总是从递归开始的那一刻起返回整数值。

这是我的实现，其中 (Node -> Variable) 是启发式函数，Sentence 是 CNF 中要满足的子句列表，[Variable] 是未分配的 Literals 列表，Model 只是一个真值评估。

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 monad。该助手的代码如下所示：

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 和状态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'