8

我正在构建一些中等大小的DIMACS文件，但是使用下面使用的方法，与生成的文件的大小相比，内存使用量相当大，并且在我需要生成的一些较大的文件上遇到了out of memory问题。

import Control.Monad.State.Strict
import Control.Monad.Writer.Strict
import qualified Data.ByteString.Lazy.Char8 as B
import Control.Monad
import qualified Text.Show.ByteString as BS
import Data.List

main = printDIMACS "test.cnf" test

test = do
  xs <- freshs 100000
  forM_ (zip xs (tail xs))
    (\(x,y) -> addAll [[negate x, negate y],[x,y]])

type Var = Int
type Clause = [Var]

data DIMACSS = DS{
  nextFresh :: Int,
  numClauses :: Int
} deriving (Show)

type DIMACSM a = StateT DIMACSS (Writer B.ByteString) a

freshs :: Int -> DIMACSM [Var] 
freshs i = do
  next <- gets nextFresh
  let toRet = [next..next+i-1]
  modify (\s -> s{nextFresh = next+i}) 
  return toRet

fresh :: DIMACSM Int
fresh = do
  i <- gets nextFresh
  modify (\s -> s{nextFresh = i+1}) 
  return i

addAll :: [Clause] -> DIMACSM ()
addAll c = do
  tell 
    (B.concat . 
    intersperse (B.pack " 0\n") . 
    map (B.unwords . map BS.show) $ c)
  tell (B.pack " 0\n")
  modify (\s -> s{numClauses = numClauses s + length c})

add h = addAll [h]

printDIMACS :: FilePath -> DIMACSM a -> IO ()
printDIMACS file f = do
  writeFile file ""
  appendFile file (concat ["p cnf ", show i, " ", show j, "\n"])
  B.appendFile file b
   where
     (s,b) = runWriter (execStateT f (DS 1 0))
     i = nextFresh s - 1
     j = numClauses s

我想保留从句的单子结构，因为它非常方便，但我需要克服记忆问题。如何优化上述程序，使其不使用太多内存？

4

2 回答 2

9

如果您想要良好的内存行为，您需要确保在生成子句时写出它们，而不是使用惰性或更明确的方法（例如管道、枚举器、管道）将它们收集到内存中并直接转储它们之类的。

这种方法的主要障碍是 DIMACS 格式需要标题中的子句和变量的数量。这可以防止幼稚的实现变得足够懒惰。有两种可能：

务实的做法是先将子句写入临时位置。之后数字是已知的，因此您将它们写入真实文件并附加临时文件的内容。

如果子句的生成没有副作用（除了你的DIMACSMmonad 提供的效果）并且足够快，那么更漂亮的方法是可能的：运行两次，首先丢弃子句并只计算数字，打印标题行，运行再次生成器；现在打印条款。

（这是我实施SAT-Britney的经验，我采用了第二种方法，因为它更符合该上下文中的其他要求。）

此外，在您的代码中，addAll还不够懒惰：即使在编写（在某种意义上）子句c之后，也需要保留列表。MonadWriter这是另一个空间泄漏。我建议您将其实现add为原始操作，然后addAll = mapM_ add.

于 2012-10-30T14:41:36.373 回答
3

正如 Joachim Breitner 的回答中所解释的那样，问题在于DIMACSM不够懒惰，既因为使用了严格版本的 monad，也因为在将变量和子句ByteString写入文件之前需要变量和子句的数量。解决方案是使用 Monad 的惰性版本并执行两次。事实证明，也有必要WriterT成为外单子：

import Control.Monad.State
import Control.Monad.Writer

...

type DIMACSM a = WriterT B.ByteString (State DIMACSS) a

...

printDIMACS :: FilePath -> DIMACSM a -> IO ()
printDIMACS file f = do
  writeFile file ""
  appendFile file (concat ["p cnf ", show i, " ", show j, "\n"])
  B.appendFile file b
   where
     s = execState (execWriterT f) (DS 1 0)
     b = evalState (execWriterT f) (DS 1 0)
     i = nextFresh s - 1
     j = numClauses s
于 2012-10-30T19:05:16.157 回答