@hackage / toysolver

0.10.0 (Unreleased)

• SMT
  • Migrate toysmt from the Smtlib fork to the newly developed language-smtlib package (#206, #214)
    • The toysmt REPL now supports multi-line input (#206, #213)
  • Support define-const command in ToySolver.SMT.SMTLIB2Solver (#215)
  • Update the semantics of zero division on bitvectors to conform to SMT-LIB >=2.6 (#209)
  • toysmt now suppresses the prompt and does not use haskeline when stdin is not a terminal (#211)
  • Fix SMT model not to contain a bogus entry for an unused uninterpreted function (#216)
  • Modify the (get-model) command to return the definition of the zero-division function (/0) instead of the assertions about division by zero results (#217)
• Converter and toyconvert command
  • Do not produce obj<T constraint in wbo2pb when all interpretations are admissible (#157)
  • Optimize unconstrainPB a little (#159, #161)
  • Change ToySolver.SAT.Encoder.Integer to encode integer variables without introducing <= constraints (#162)
  • Store surplus expression instead of raw variables in inequalitiesToEqualitiesPB (#164)
  • Refactor ToySolver.SAT.Encoder.Integer (#167)
  • Improve inequalitiesToEqualitiesPB to produce more compact output (#168)
  • Extend normalizePB to transform constant terms in the objective function into non-constant terms (#169)
  • Support semi-integer variables in IP→PB conversion and improve error messages (#170)
  • Simplify JSON that represents PBSum (#171)
  • Scale objective function and constraints using rational instead of integer in IP→PB transformation (#172)
  • Linearize constant term in objective function when writing LP/MPS file (#185)
  • Add --[no-]mps-obj-name option to toyconvert (#188)
  • Rename --lp option to --mip and keep --lp as an alias (#189)
  • Optimize pb2ip and wbo2ip by not calling convVar repeatedly (#191)
• toysat
  • Conform to MaxSAT Evaluation 2024 (#177)
    • It outputs SATISFIABLE in MaxSAT mode if it finds a model but fails to prove optimality
    • Add --exit-code option to set exit code
• Dependencies
  • Stop supporting 32-bit Windows (#154)
  • Stop supporting GHC 9.4 and below (#156, #205)
  • Use pseudo-boolean-0.1.12.0 (#158)
  • Require aeson >=2.0, array >=0.5.6, hashable >=1.4.3, and optparse-applicative >=0.18 (#208)
  • Require language-smtlib >=0.2.0.0 (#206, #214)
• Misc
  • Add toysolver-check command to check solution (#174, #196)
  • Improve model output speed by printing using ByteString (#175)
  • Build statically linked Linux binaries (#194)
  • Use Cauchy's bounds instead of Lagrange's bounds as the bounds for all roots (#203)
  • Optimize divModMP by rewriting it from a full-reduction strategy to the standard textbook leading-term multivariate division algorithm (#212)

0.9.0 (2025-02-18)

• Converter updates
  • Add --dump-info option to toyconvert (#119, #120, #125)
  • Change the signs of QUBO-related converter's representation of offset (#126)
  • Change WBO2IPInfo not to store weights (#124)
  • Change SAT2KSATInfo, SimplifyMaxSAT2Info and SAT3ToMaxSAT2Info to be synonyms of TseitinInfo (#121, #123)
  • Use SAT.VarMap to represent definitions in SAT-related encoders/converters (#127)
  • Add instances for transforming objective function values between PB↔︎WBO conversion (#132)
  • Change ReversedTransformer, GCNF2MaxSATInfo, PBAsQUBOInfo, QUBO2IsingInfo, Ising2QUBOInfo from data to newtype (#134)
  • Fix mip2pb’s handling of indicator constraints (#137)
  • Add more converter instances (#138)
  • Restructure converter modules (#142)
  • Support SOS constraints over non-binary variables in mip2pb (#140)
  • Rename mip2pb to ip2pb
• Pseudo-boolean and cardinality constraint encoder updates
  • Consider polarity in encoding of pseudo-boolean and cardinality constraints (#88)
  • Add BC-CNF pseudo-boolean constraint encoder (#85)
  • Support specifying PB encoding strategy (#77)
• Dependencies
  • Support GHC 9.4 (#92), 9.6, 9.8, 9.10
  • Use prettyprinter package if optparse-applicative is >=0.18 (#106)
  • Upgrade MIP package to 0.2.* (#144)
• Misc
  • Do not rely on StarIsType extension (#84)
  • Add BuildForeignLibraries flag (#94)
  • Remove features that depend on OpenCL (#90)
  • Improve ToySolver.Graph module (#130, #150)

0.8.0 (2022-07-26)

• 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)

0.7.0 (2021-02-08)

• 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 reducethe 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

0.6.0 (2019-10-04)

• 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

0.5.0 (2017-10-09)

• new solvers:
  • ToySolver.BitVector
  • ToySolver.Combinatorial.BipartiteMatching
  • ToySolver.Combinatorial.HittingSet.DAA
  • ToySolver.Combinatorial.HittingSet.MARCO
  • ToySolver.Arith.DifferenceLogic
  • ToySolver.Graph.ShortestPath
  • ToySolver.QBF
• toysat
  • add --init-sp option to initialize variable state using survey propagation
  • allow using UBCSAT when solving PBO/WBO problems
• toysmt
  • support bit-vector logic
• toyconvert
  • pbconvert and lpconvert were merged into a single command toyconvert
  • add --ksat=NUMBER option to convert to k-SAT formula
  • add --linearlize and --linearizer-pb options
  • add --remove-usercuts option
• add new modules to ToySolver.Converter
  • ToySolver.Converter.GCNF2MaxSAT
  • ToySolver.Converter.MIP2PB
  • ToySolver.Converter.PBLinearlization
  • ToySolver.Converter.SAT2KSAT
• ToySolver.SAT
  • introduce type classes for adding constraints
  • ToySolver.SAT.Encoder.Tseitin: add XOR and Full-adder encoder
  • ToySolver.SAT.Encoder.PB: add functionality to encode PB constraint using adder networks and sorting networks
  • ToySolver.SAT.MUS.Enum: add GurvichKhachiyan1999 and MARCO to the MUS enumeration methods
  • implement learning rate based branching heuristics
  • add ToySolver.SAT.ExistentialQuantification
  • add ToySolver.SAT.Store.CNF and ToySolver.SAT.Store.PB
  • implement survey propagation as ToySolver.SAT.MessagePassing.SurveyPropagation
• Data.MIP
  • parameterize Problem type with coefficient type and use Scientific as default
  • introduce Status type
  • add solution file parsers: ToySolver.Data.MIP.Solution.{CBC,CPLEX,GLPK,Gurobi,SCIP}
  • add solver wrapper modules: ToySolver.MIP.Solver.{CBC,CPLEX,Glpsol,GurobiCl,LPSolve,SCIP}
• add a QDimacs parser as ToySolver.Text.QDimacs
• add ToySolver.Text.CNF, ToySolver.Text.QDimacs
• switch to use megaparsec
• use clock package for measuring duration
• add simple numberlink solver sample

0.4.0 (2016-06-25)

• add experimental SMT (Satisfiability Modulo Theories) solver 'toysmt', which supports theory of uninterpreted functions and linear real arithmetics.
• fix toysat to output model in Max-SAT format instead of PB/WBO format when solving Max-SAT problems
• add experimental getAssumptionsImplications functions to ToySolver.SAT module.
• add getFixedLiterals to ToySolver.SAT module.
• use 'mwc-random' package instead of 'random' package.
• introduce 'Config' data type in ToySolver.SAT to simplify configuration management.
• add subset-sum problem solver
• implement backtracking and explanation generation in simplex solver and congruence closure solver.

0.3.0 (2015-05-31)

• split OPB/WBO file library into a separate 'pseudo-boolean' library.