shnarazk / mios

A SAT solver written in Haskell.
https://gitlab.com/satisfiability01/mios/
GNU General Public License v3.0
39 stars 3 forks source link

Segmentation fault when used as a library #89

Open potocpav opened 5 years ago

potocpav commented 5 years ago

On complicated problems, mios works fine when used as an executable like this:

$ stack run mios162 -- sudoku.dimacs
SATISFIABLE, saved to .ans_sudoku.dimacs for sudoku.dimacs

Example problem: https://gist.github.com/potocpav/97c84a24a45797b44a63a565295aec8b

It, however, fails on the same file when used as a library:

import SAT.Mios.Util.DIMACS.Reader
import SAT.Mios (CNFDescription(..), solveSAT)

main :: IO ()
main = do
    clauses <- clauseListFromFile "sudoku.dimacs"
    let nVars = (maximum . map abs $ concat clauses)
    let descr = CNFDescription nVars (length clauses) "file"
    l <- solveSAT descr clauses
    print l

This sometimes shows Segmentation fault (core dumped), sometimes this:

simple: Data.Vector.Mutable: uninitialised element
CallStack (from HasCallStack):
  error, called at ./Data/Vector/Mutable.hs:188:17 in vector-0.12.0.2-AoZ9EwUsgIW1yrOc105QXH:Data.Vector.Mutable

On large problems (>10k variables) it fails reliably. For less complicated problems (~2000 variables), the failures are intermittent. For small problems (~10 variables), it works.