reading the satisfying assignment is way too slow

[jwaldmann]

(see test case in issue #16)

[jwaldmann]

Some improvement from

parseSolution' :: String -> IntMap Bool
parseSolution' s = case words s of
   "SAT" : ws -> IntMap.fromList
       $ map ( \ v -> (abs v, v > 0 )) 
       $ takeWhile (/= 0) $ map read ws
   _ -> IntMap.empty -- WRONG (should be Nothing)

in Ersatz.Solver.Minisat, but it's still not fast. Use bytestrings?

[jwaldmann]

For reference, profiling the above gives this:

           Speed +RTS -P -RTS 50000

        total time  =        2.12 secs   (2115 ticks @ 1000 us, 1 processor)
        total alloc = 1,660,659,976 bytes  (excludes profiling overheads)

COST CENTRE            MODULE                  %time %alloc  ticks     bytes

parseSolution'         Ersatz.Solver.Minisat    56.4   46.3   1192 769479408
runBit                 Ersatz.Bit                6.6    8.0    139 132797344
bLine                  Ersatz.Problem            6.4   13.9    135 230796736
bClause                Ersatz.Problem            3.7    3.4     79  55680896
formulaFromList        Ersatz.Internal.Formula   3.1    3.3     65  54061400
satClauses             Ersatz.Problem            2.9    4.1     61  67596136
stableMap.\            Ersatz.Problem            2.7    2.5     57  41144048
dimacs.clauses         Ersatz.Problem            2.4    2.1     51  35599904
mappend                Ersatz.Internal.Formula   1.7    1.7     35  28394784
runBit.\               Ersatz.Bit                1.4    2.4     29  39199216
parseSolutionFile      Ersatz.Solver.Minisat     1.3    1.5     28  24894520
formulaXor             Ersatz.Internal.Formula   1.3    1.7     28  28399448
solutionFrom.lookupLit Ersatz.Solution           1.1    0.0     24    800000
bLine0                 Ersatz.Problem            0.9    2.6     18  42399232
assert                 Ersatz.Bit                0.8    1.5     17  25199496

[jwaldmann]

with attoparsec:

parseSolution :: B.ByteString -> IntMap Bool
parseSolution s = case P.parseOnly ( assignment <* P.endOfInput ) s of
    Left err -> IntMap.empty -- WRONG
    Right ps -> IntMap.fromList ps

assignment :: P.Parser [(Int,Bool)]
assignment = P.string "SAT" *> P.skipSpace
   *> many ( do v <- P.signed P.decimal; guard $ v /= 0 ; P.skipSpace ; return (abs v, v > 0) )
   <* P.string "0" <* P.skipSpace

the above profile becomes:

           Speed +RTS -P -RTS 50000

        total time  =        1.01 secs   (1008 ticks @ 1000 us, 1 processor)
        total alloc = 1,031,508,160 bytes  (excludes profiling overheads)

COST CENTRE           MODULE                               %time %alloc  ticks     bytes

bLine                 Ersatz.Problem                        13.5   22.4    136 230796736
runBit                Ersatz.Bit                            13.2   10.3    133 105997880
bClause               Ersatz.Problem                         7.3    5.4     74  55680896
takeWhile1            Data.Attoparsec.ByteString.Internal    7.0    8.4     71  86245472
formulaFromList       Ersatz.Internal.Formula                6.4    5.2     65  54061400
stableMap.\           Ersatz.Problem                         4.7    3.9     47  40064176

[ekmett]

I've added you as a committer on this repository. You are hereby fully empowered to unilaterally improve our parser performance. =)

[glguy]

@jwaldmann Did your commits back in 2016 resolve the concerns expressed in this issue?

[jwaldmann]

I will re-check. These days, I am mostly using https://github.com/jwaldmann/ersatz-minisatapi

[jwaldmann]

should apply this patch to cryptominisat5 (and perhaps others) as well, see https://github.com/ekmett/ersatz/issues/16#issuecomment-754148295