DPLL 算法和访问的节点数

Question

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

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

这是我的实现，其中(节点 -> 变量)是一个启发式函数，句子是 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.May和Data.List。

编辑：

我尝试实现的一种可能的解决方案是使用元组(布尔值，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语句中的递归调用中检索计数器。我什至不确定这在哈斯克尔是否可能。

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)

这是Statemonad 的手动实现。但是，我根本不清楚你为什么要在柜台里通过。只需将其退回即可。然后它是更简单的Writermonad。此帮助程序的代码如下所示：

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参数是计数器的当前状态，结果通过计数器的更新状态进行丰富。

这可以使用状态 monad 进一步优雅地重新表达。这里有一个非常好的关于哈斯克尔和状态 monad 的教程。基本上，a -> b到a -> Int -> (b, Int)的转换可以看作是a -> b到a -> 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'