我正在实现一个计算访问节点数量的DPLL算法。我已经成功实现了不计算访问节点的DPLL算法，但对于如何计算节点数量的问题，我还没有找到任何解决方案。主要问题在于，当算法找到一个满足的估值并返回True时，递归会回溯并返回递归开始时的计数器。在任何命令式语言中，我会使用全局变量并在函数被调用时增加计数器，但在Haskell中情况并非如此。
我在这里粘贴的代码并不代表我尝试解决计数问题的尝试，这只是我没有计数功能的解决方案。我尝试使用像(True,Int)这样的元组，但它总是会返回递归开始时的整数值。
这是我的实现，其中(Node -> Variable)是一个启发式函数，Sentence是需要满足的CNF子句列表，[Variable]是未分配的文字列表，Model只是一个真值估值。
dpll' :: (Node -> Variable) -> Sentence -> [Variable] -> Model -> Booldpll' 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中是否可能。
回答：
你可以使用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——并且函数调用将更简单，只需少一个需要正确设置的参数即可。
