DPLL algorithm and number of visited nodes

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.

You can retrieve the counter from the recursive call using case or similar.

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)

This is a manual implementation of the State monad. However, it's not clear to me why you are passing in a counter at all. Just return it. Then it is the simpler Writer monad instead. The code for this helper would look something like this:

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)

Other results would be similar -- returning 0 instead of counter and 1 instead of counter+1 -- and the call to the function would be simpler, with one fewer argument to worry about setting up correctly.