Toysolver Versions Save

• Support GHC 9.4

• Separate Formula type from ToySolver.SAT.Encoder.Tseitin into ToySolver.SAT.Formula (#74)
• Use megaparsec as default PB parser and add --pb-fast-parser option to use attoparsec (#71)
• Update lower bounds of dependency packages
• Add --maxsat-compact-v-line option for printing MaxSAT solution in the new compact format (#65)
• Fix ToySolver.SAT.Printer and its toysat's output for Max-SAT problems (#64)
• Support new WCNF file format (#63)
• Use bytestring-encoding-0.1.1.0 because bytestring-encoding-0.1.0.0 has a memory corruption bug (#62)
• Remove deprecated API (#56)
• Support GHC-9.2 (#76) and stop supporting GHC 8.0, 8.2, and 8.4 (#50)

Release description* add toysat-ipasir foreign library which implements IPASIR API for incremental SAT solving.

• ToySolver.SAT
  • Restructure SAT solver modules under ToySolver.SAT.Solver.*
  • add SequentialCounter, ParallelCounter and Totalizer as methods for encoding cardinality constraints
  • add PackedLit type to reduce memory footprint
  • use structure of array (SOA) approach to reduce memory footprint
  • add setLearnCallback/clearLearnCallback and setTerminateCallback/clearTerminateCallback which correspond to IPASIR's ipasir_set_learn() and ipasir_set_terminate().
  • add clearLogger
  • change getFailedAssumptions and getAssumptionsImplications to return IntSet instead of [Int]
• separate ToySolver.Data.MIP.* into new MIP package's Numeric.Optimization.MIP.*
• add ToySolver.Data.Polynomial.Interpolation.Hermite
• add ToySolver.Graph.Base and ToySolver.Graph.MaxCut
• add ToySolver.Converter.SAT2MIS
• ToySolver.Graph.ShortestPath: fix vertex type to Int instead of arbitrary Hashable type
• stop supporting GHC-7.10
• add ExtraBoundsChecking flag for debugging

• new solvers:
  • ToySolver.SAT.SLS.ProbSAT and sample probsat program
• new converters:
  • ToySolver.Converter.NAESAT
  • ToySolver.Converter.SAT2MaxCut
  • ToySolver.Converter.SAT2MaxSAT: SAT and 3-SAT to Max-2-SAT converter
  • ToySolver.Converter.QBF2IPC
  • ToySolver.Converter.QUBO: QUBO↔IsingModel converter
• new file format API:
  • merge ToySolver.Text.MaxSAT, ToySolver.Text.GCNF, ToySolver.Text.QDimacs, and ToySolver.Text.CNF info ToySolver.FileFormat and ToySolver.FileFormat.CNF
  • allow reading/writing gzipped CNF/WCNF/GCNF/QDimacs/LP/MPS files
• rename modules:
  • ToySolver.Arith.Simplex2 to ToySolver.Arith.Simplex
  • ToySolver.Arith.MIPSolver2 to ToySolver.Arith.MIP
  • ToySolver.Data.Var to ToySolver.Data.IntVar
• ToySolver.SAT:
  • add cancel function for interruption
  • introduce PackedClause type
• ToySolver.Arith.Simplex
  • introduce Config data type
  • implement bound tightening
• switch from System.Console.GetOpt to optparse-applicative
• stop supporting GHC-7.8

ToySolver version 0.4.0 release.

The highlight of this release is the introduction of SMT (Satisfiablity Modulo Theories) solver 'toysmt'. At the moment, toysmt is very experimental and only supports the theory of uninterpreted functions and the theory of linear real arithmetic.