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 形式がヘッダー内の句と変数の数を想定していることです。これにより、素朴な実装が十分に怠惰になるのを防ぎます。次の 2 つの可能性があります。

実用的な方法は、最初に句を一時的な場所に書き込むことです。その後、番号がわかるので、それらを実際のファイルに書き込み、一時ファイルの内容を追加します。

句の生成に副作用がなく (DIMACSMモナドによって提供される効果以外に) 十分に高速である場合は、よりきれいなアプローチが可能です: 2 回実行します。最初に句を破棄して数値を計算し、ヘッダー行を出力し、ジェネレーターをもう一度。現在、条項を印刷しています。

(これは、 SAT-Britneyの実装に関する私の経験からのものです。そこでは、2 番目のアプローチを採用しました。これは、そのコンテキストの他の要件により適しているためです。)

また、あなたのコードでaddAllは、十分に怠惰ではありません。リストは、(ある意味で) 句cを書いた後でも保持する必要があります。MonadWriterこれは別のスペース リークです。addプリミティブ操作として実装してからaddAll = mapM_ add.

于 2012-10-30T14:41:36.373 に答える
3

Joachim Breitner's answer で説明されているように、厳密なバージョンのモナドが使用され、ファイルに書き込むDIMACSM前に変数と句の数が必要なため、問題は十分に怠惰ではありませんでした。ByteString解決策は、モナドの遅延バージョンを使用して、それらを 2 回実行することです。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 に答える