0.8.1 ----- * Support GHC 9.4 0.8.0 ----- * 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 ----- * add `toysat-ipasir` foreign library which implements [IPASIR](https://github.com/biotomas/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](https://github.com/biotomas/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](http://hackage.haskell.org/package/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 ----- * 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 `gzip`ped 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 ----- * 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` * suport 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 ----- * add experimental SMT (Satisfiablity 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 configulation management. * add subset-sum problem solver * implement backracking and explanation generation in simplex solver and congruence closure solver. 0.3.0 ----- * split OPB/WBO file library into a serarate 'pseudo-boolean' library.