msakai / toysolver

My sandbox for experimenting with solver algorithms.

toysolver

Hackage:

Dev:

It provides solver implementations of various problems including SAT, SMT, Max-SAT, PBS (Pseudo Boolean Satisfaction), PBO (Pseudo Boolean Optimization), MILP (Mixed Integer Linear Programming) and non-linear real arithmetic.

In particular it contains moderately-fast pure-Haskell SAT solver 'toysat'.

Installation

See INSTALL.md.

Usage

This package includes several commands.

toysolver

Arithmetic solver for the following problems:

• Mixed Integer Liner Programming (MILP or MIP)
• Boolean SATisfiability problem (SAT)
• PB
  • Pseudo Boolean Satisfaction (PBS)
  • Pseudo Boolean Optimization (PBO)
  • Weighted Boolean Optimization (WBO)
• Max-SAT families
  • Max-SAT
  • Partial Max-SAT
  • Weighted Max-SAT
  • Weighted Partial Max-SAT
• Real Closed Field

Usage:

toysolver [OPTION...] [file.lp|file.mps]
toysolver --lp [OPTION...] [file.lp|file.mps]
toysolver --sat [OPTION...] [file.cnf]
toysolver --pb [OPTION...] [file.opb]
toysolver --wbo [OPTION...] [file.wbo]
toysolver --maxsat [OPTION...] [file.cnf|file.wcnf]

-h  --help           show help
-v  --version        show version number
    --solver=SOLVER  mip (default), omega-test, cooper, cad, old-mip, ct

toysat

SAT-based solver for the following problems:

• SAT
  • Boolean SATisfiability problem (SAT)
  • Minimally Unsatisfiable Subset (MUS)
  • Group-Oriented MUS (GMUS)
• PB
  • Pseudo Boolean Satisfaction (PBS)
  • Pseudo Boolean Optimization (PBO)
  • Weighted Boolean Optimization (WBO)
• Max-SAT families
  • Max-SAT
  • Partial Max-SAT
  • Weighted Max-SAT
  • Weighted Partial Max-SAT
• Integer Programming (all variables must be bounded)

Usage:

toysat [file.cnf|-]
toysat --sat [file.cnf|-]
toysat --mus [file.gcnf|file.cnf|-]
toysat --pb [file.opb|-]
toysat --wbo [file.wbo|-]
toysat --maxsat [file.cnf|file.wcnf|-]
toysat --lp [file.lp|file.mps|-]

PB'12 competition result:

• toysat placed 2nd in PARTIAL-BIGINT-LIN and SOFT-BIGINT-LIN categories
• toysat placed 4th in PARTIAL-SMALLINT-LIN and SOFT-SMALLINT-LIN categories
• toysat placed 8th in OPT-BIGINT-LIN category

toysmt

SMT solver based on toysat.

Usage:

toysmt [file.smt2]

Currently only QF_UF, QF_RDL, QF_LRA, QF_UFRDL and QF_UFLRA logic are supported.

toyfmf

SAT-based finite model finder for first order logic (FOL).

Usage:

toyfmf [file.tptp] [size]

toyconvert

Converter between various problem files.

Usage:

toyconvert -o [outputfile] [inputfile]

Supported formats:

• Input formats: .cnf .wcnf .opb .wbo .gcnf .lp .mps
• Output formats: .cnf .wcnf .opb .wbo .lsp .lp .mps .smp .smt2 .ys

Bindings

• ersatz-toysat - toysat backend driver for ersatz
• satchmo-toysat - toysat backend driver for satchmo

Spin-off projects and packages

• bytestring-encoding
• data-interval
• extended-reals
• finite-field
• MIP
• OptDir
• pseudo-boolean
• sign

toysolver's Issues

cabal install toysolver

~/$ cabal install toysolver
~/$ wget https://raw.githubusercontent.com/msakai/toysolver/master/samples/lp/Sudoku.lp

~/.cabal/bin/$ ./toysolver --lp Sudoku.lp
Segmentation fault (core dumped)

basically reading lp file won't work in toysat toysolver or toyconvert

./toysolver --sat aaa.cnf works
./toysat aaa.cnf works

~/.cabal/bin/$ ls -l
lrwxrwxrwx 1 ubuntu ubuntu 114 May 5 19:46 toyconvert -> ../store/ghc-8.8.4/toysolver-0.7.0-a2dd48b3ce6143ea169cfa73d74179abe5e7eeb05444e8361f8dc9863f6bf7c0/bin/toyconvert*
lrwxrwxrwx 1 ubuntu ubuntu 110 May 5 19:46 toyqbf -> ../store/ghc-8.8.4/toysolver-0.7.0-0e1deeee83edf2aa18bd4d7bf0ba4bc82d151ea40cbf44f0f5a25fdf2be1f160/bin/toyqbf*
lrwxrwxrwx 1 ubuntu ubuntu 110 May 5 19:46 toysat -> ../store/ghc-8.8.4/toysolver-0.7.0-82239a3f18744616363cb674ac3ededa4ccfa32e6a5d40a519eaafd95156fd0c/bin/toysat*
lrwxrwxrwx 1 ubuntu ubuntu 110 May 5 19:46 toysmt -> ../store/ghc-8.8.4/toysolver-0.7.0-b4ed3ad055453675c3f24f0a301dc551aa7ff1e1e8bd5e2dc91046bc301d6a84/bin/toysmt*
lrwxrwxrwx 1 ubuntu ubuntu 113 May 5 19:46 toysolver -> ../store/ghc-8.8.4/toysolver-0.7.0-dd1e9520e775b36ced274a980f682220c66a9125c74d89e3e0ef301d9f86a5e4/bin/toysolver*

It's not an issue

I can't thank you enough because you make haskell such a wonderful land to program in.

Thanks again for you amazing work. Showing to the world that Haskell is better than the rest.

Build failure in toysolver-0.0.5 with GHC 9.2

src/SAT.hs:2:28: warning:
    -XDoRec is deprecated: use -XRecursiveDo or pragma {-# LANGUAGE RecursiveDo #-} instead
  |
2 | {-# LANGUAGE BangPatterns, DoRec, ScopedTypeVariables, CPP, DeriveDataTypeable #-}
  |                            ^^^^^
[ 1 of 79] Compiling Algebra.Lattice.Boolean ( src/Algebra/Lattice/Boolean.hs, dist/build/Algebra/Lattice/Boolean.o, dist/build/Algebra/Lattice/Boolean.dyn_o )

src/Algebra/Lattice/Boolean.hs:54:10: error:
    • Variable not in scope: meet :: a -> a -> a
    • Perhaps you meant one of these:
        data constructor ‘Meet’ (imported from Algebra.Lattice),
        ‘meets’ (imported from Algebra.Lattice)
   |
54 | (.&&.) = meet
   |          ^^^^

src/Algebra/Lattice/Boolean.hs:58:10: error:
    • Variable not in scope: join :: a -> a -> a
    • Perhaps you meant one of these:
        data constructor ‘Join’ (imported from Algebra.Lattice),
        ‘joins’ (imported from Algebra.Lattice)
   |
58 | (.||.) = join
   |          ^^^^
cabal: Failed to build toysolver-0.0.5

Real-closed field solver

These are remarkably hard to find and it would be nice to have a clean one in Haskell.

build script should not ask for sudo password and install system wide deps

Hi, I find the build scripts "aggressive", asking for sudo passwords, modifying apt lists and performing system wide installs of deps without any warning or warning info. Perhaps you could modify the readme to list the ghc dep and change the script so that it does not function in sudo mode by default and just fails if deps are missing ?

one of the apps doesn't build on master

Build profile: -w ghc-8.6.3 -O1
In order, the following will be built (use -v for more details):
 - toysolver-0.6.0 (exe:toysmt) (first run)
Preprocessing executable 'toysmt' for toysolver-0.6.0..
cabal: can't find source for Smtlib/Parsers/CommonParsers in app/toysmt,
Smtlib,
/Users/carter/Desktop/repoScratcher/toysolver/dist-newstyle/build/x86_64-osx/ghc-8.6.3/toysolver-0.6.0/x/toysmt/build/toysmt/autogen,
/Users/carter/Desktop/repoScratcher/toysolver/dist-newstyle/build/x86_64-osx/ghc-8.6.3/toysolver-0.6.0/x/toysmt/build/global-autogen

toysat --pb not running for this input?

I am a bit confused with the output of toysat when used with --pb option with a particular instance. With the attached file in opb format, I don't see any results. The solver simply quits. How should I interpret it? [Note that, I am able to run other small testcases]

(oops I am not able to attach the testcase: Error says, I can only attach png/gif/jpg).

$./toysat --pb min.txt
...
c loop-0.3.0
c mtl-2.2.1
c multiset-0.3.0
c mwc-random-0.13.3.2
c old-locale-1.0.0.6
c parse_dimacs-1.3
c parsec-3.1.9
c prettyclass-1.0.0.0
c primes-0.2.1.0
c process-1.2.0.0
c pseudo-boolean-0.1.2.0
c queue-0.1.2
c sign-0.4.2
c stm-2.4.2
c temporary-1.4.2
c time-1.4.2
c type-level-numbers-0.1.1.1
c unbounded-delays-0.1.0.9
c unordered-containers-0.2.4.0
c vector-space-0.10.2
c command line = ["--pb","min.txt"]
c use --random-gen="508655808 1659196849 1072282525 3122131391 2423936777 1470284561 213976922 2135472621 656322979 1736236859 836210351 718055101 2439291645 698284455 1728478182 4200647059 780576319 1395652772 1809761089 1161594570 3393332917 1258869760 3303925131 3821121962 839083773 623863976 2922618724 4257593731 612410646 1831897773 3406159972 451678311 3100798560 270778209 3198629679 4013908656 958233189 292876876 2867125610 3819227241 458541713 317087768 1244229644 2295026626 3631368879 3199260981 496888532 3657224610 2695621227 809055206 3290211606 2697954526 2890414411 2404806155 600503903 3675319417 2407495405 350422873 1020310661 3124076876 3983772080 184343369 3473187996 3041176272 3402092637 2164500065 2273527990 1765178842 1167047973 3290728564 2159859327 415970822 1690776772 166261180 226758578 2392621182 4226447651 3783026362 3945561292 1033688798 2541519130 3872405237 1088028221 2145989806 3705750787 2501348722 2549116307 1289291783 1599799544 9362808 1224565366 3787978058 3447889198 2270723997 182538429 2791144496 1573000555 2029625764 1100056224 846765250 57413492 3580064767 1822544135 4096134418 3416820127 2431702436 3448232906 2151415644 803190017 1950330758 1973986151 3665564905 1466797908 2740103655 1553011071 2308927903 1302084616 1908443575 3559058450 2171481495 1819245345 123616344 1255356065 853921188 1081220811 2470076706 3240704868 2929925922 2027959876 3894361981 3230106602 3875057153 3873196943 3115822817 3596939265 4223093735 1093765989 2782501417 2918619252 1529541314 2943944454 3346408920 1751122346 1516570277 411496114 1726015395 133798522 3666797293 989976569 2524907507 1470666714 1004076047 1786675275 944337483 3960873041 3800640395 3234416482 2450253656 3426625219 577645587 1281486344 3237028168 49601347 2759874733 410018306 962625752 870648904 3019639816 1304511203 702205597 2466784589 2596166309 3105668713 435911710 2788389570 178234977 3521247614 281479117 3073375077 3587377144 3940073798 1292398691 2468063072 1491098614 125006015 1851870200 3304861472 3056320679 1892447432 1699234489 72923534 249208249 1313134150 3284884195 1043155944 145413631 1232452045 3846412899 2596913042 135206283 1920525154 3224256571 2606646866 2363165714 334320061 3118137870 2873535947 2663893723 1767274489 3805110432 197165836 2299009718 1229451936 124580119 686719293 1433257991 1026991935 3947179893 3287938108 3052292695 421871518 3890023557 13061487 2251739276 3997058609 3005574923 2721340470 548864857 3382230145 4268383098 895357657 938342390 1607099006 3209781642 1269171289 437798892 781217359 12647583 4284326039 3856519783 2624495589 1762546839 2987342026 21299414 3305424948 3220792733 2410508663 2138444733 3403377563 499398959 377265549 7301068 2535872731 815182677 911894205 162302098 255 362436" option to reproduce the execution
endOfInput

prop_getModel_evalFSym failure

prop_getModel_evalFSym failed on appveyor on windows-i386 platform.

https://ci.appveyor.com/project/msakai/toysolver/build/1.0.565

commit 703756f

    getModel evalFSym:                                    FAIL (0.86s)
      *** Failed! (after 53 tests): 
      Exception:
        .\Data\Vector\Generic.hs:245 ((!)): index out of bounds (-2147483648,32)
        CallStack (from HasCallStack):
          error, called at .\Data\Vector\Internal\Check.hs:87:5 in vector-0.12.0.1-692PQMDMB6pIQ1uGwefDcQ:Data.Vector.Internal.Check
      Use --quickcheck-replay '52 TFGenR 75DE47510B65717086C26948E0518578C5D1775D64E0478BF98C9FF94C5B9DF3 0 16777215 24 0' to reproduce.

Installation failed on Debian Linux

OS: Debian Jessy (same problem with Debian Lenny cabal 0.14.0/1.14.0, ghc 7.4.1)
cabal-install version 1.20.0.3 using version 1.20.0.2 of the Cabal library
ghc --version
The Glorious Glasgow Haskell Compilation System, version 7.6.3

Configuring toysolver-0.2.1...
Building toysolver-0.2.1...
Preprocessing library toysolver-0.2.1...

src/ToySolver/Text/PBFile.hs:56:18:
Could not find module `Data.ByteString.Builder'
Perhaps you meant
Data.ByteString.Lazy.Builder (from bytestring-0.10.0.2)
Data.ByteString.Unsafe (from bytestring-0.10.0.2)
Use -v to see a list of the files searched for.
Failed to install toysolver-0.2.1
cabal: Error: some packages failed to install:
toysolver-0.2.1 failed during the building phase. The exception was:
ExitFailure 1

The exactly same problem is also describe here :
fpco/streaming-commons#16

FYI : with toysolver version d28e3ef
Installation is OK with Debian Jessy.

add "SMT" tags on hackage

... to make it easier to find it on hackage.

Stack overflow on minimizeConflictClauseRecursive?

% bzcat ../PB10/normalized-PB10/DEC-SMALLINT-LIN/oliveras/j30/normalized-j3025_1-sat.opb.bz2 | dist/build/toysat/toysat +RTS -xc -RTS --pb -
<Main.mainPB,Main.main>c arch = x86_64
c os = darwin
c compiler = ghc 7.0
c Solving starts ...
<SAT.reasonOf,SAT.minimizeConflictClauseRecursive,SAT.analyzeConflict,SAT.search,SAT.solve,Main.solvePB,Main.mainPB,Main.main><SAT.reasonOf,SAT.minimizeConflictClauseRecursive,SAT.analyzeConflict,SAT.search,SAT.solve,Main.solvePB,Main.mainPB,Main.main>Stack space overflow: current size 8388608 bytes.
Use `+RTS -Ksize -RTS' to increase it.

Files:

• PB10/normalized-PB10/DEC-SMALLINT-LIN/oliveras/j30/normalized-j3025_1-sat.opb.bz2
• PB10/normalized-PB10/DEC-SMALLINT-LIN/oliveras/j30/normalized-j3029_6-sat.opb.bz2
• PB10/normalized-PB10/DEC-SMALLINT-LIN/oliveras/j30/normalized-j3029_8-unsat.opb.bz2
• PB10/normalized-PB10/DEC-SMALLINT-LIN/oliveras/j30/normalized-j3041_4-unsat.opb.bz2

prop_Simplex_explain failure

https://github.com/msakai/toysolver/runs/1807525242?check_suite_focus=true

Simplex explain:                                      FAIL
      *** Failed! Assertion failed (after 18 tests):
      (fromList [1,2,3],[OrdRel (fromTerms [(1746056284631 % 9826412301665,-1),(15203152363938 % 2590082592775,3)]) Lt (fromTerms [((-10805767966036066790492005) % 2717766383823209137090944,1),((-6954371332529) % 2556884703077,3)]),OrdRel (fromTerms [((-46318513084543) % 2825954452605,-1),((-84836161104808) % 6821232664449,3)]) Lt (fromTerms [((-32878986163057639423497343) % 6340282666298520092181187,-1),((-2102058562915) % 152354534193,2)]),OrdRel (fromTerms [(800927333029 % 343631592637,1)]) Eql (fromTerms [(12974358287795 % 1163880192697,1),((-26182414536409) % 2543710855391,2)]),OrdRel (fromTerms [((-83492509556885) % 8651844058708,1)]) Ge (fromTerms [((-356015815369) % 22673757336,2),((-27476085033935) % 4622007003834,3)]),OrdRel (fromTerms [((-39875095304489) % 3101412109143,-1),(28185656388712 % 2199966699027,2)]) Eql (fromTerms [])])
      Config {configPivotStrategy = PivotStrategyBlandRule, configEnableBoundTightening = True}
      Use --quickcheck-replay=155047 to reproduce.

Incorrect output from MIPSolverHL

Try the following program:

test :: OptResult Double
test =
  let a = var 1
      b = var 2
  in maximize (3*^a ^-^ b)
     [ Rel a Ge zeroV
     , Rel b Ge zeroV
     , Rel a Le (constant 1)
     , Rel (3*^b) Ge (4*^a)
     ]
     (IntSet.fromList [1,2])

The output is Optimum 0.0 (fromList [(1,0.0),(2,0.0)]). However, I expected Optimum 1.0 (fromList [(1,1.0),(2,2.0)]).

I am using the version on Hackage.

restriction to base <4.15

The current package (version 0.7.0) has an upper bound on base of <4.15 which precludes compilation with ghc 9 (which uses base 4.15 or higher). It seems that the packages works ok when compiled with "allow newer" relaxation of the upper bounds, which is, however, occasionally interacting with other packages.

could you check if the bounds can be liftet to <=4.16 to include the current versions of ghc (up to 9.2) and then upload to hackage a maintenance version 0.7.1.

thank you!

analyzeConflictHybrid error

https://travis-ci.org/msakai/toysolver/jobs/288872957

    solvePBNLC:                                           FAIL (0.05s)
      *** Failed! Exception: 'analyzeConflict: should not happen' (after 19 tests): 
      Use --quickcheck-replay '18 TFGenR A51EA4822CC21D39A3C9136AD1D9593B972C925606DA53AA201232173FC68C8C 0 68719345664 36 0' to reproduce.

toysat-ipasir segmentation fault on GHC-8.10.3

https://github.com/msakai/toysolver/runs/1811924685

Incompatibility with optparse-applicative-0.18.1.0 + ansi-wl-pprint-0.6.9

If we compile toysolver 0.8.1 with optparse-applicative-0.18.1.0 + ansi-wl-pprint-0.6.9, it fails with the following error:

/Users/sakai/src/toysolver/app/toyconvert.hs:198:22: error:
    • Couldn't match type ‘PP.Doc’
                     with ‘prettyprinter-1.7.1:Prettyprinter.Internal.Doc
                             prettyprinter-ansi-terminal-1.1.3:Prettyprinter.Render.Terminal.Internal.AnsiStyle’
      Expected: Options.Applicative.Help.Pretty.Doc
        Actual: PP.Doc
      NB: ‘prettyprinter-1.7.1:Prettyprinter.Internal.Doc’
            is defined in ‘Prettyprinter.Internal’
                in package ‘prettyprinter-1.7.1’
          ‘PP.Doc’
            is defined in ‘Text.PrettyPrint.ANSI.Leijen.Internal’
                in package ‘ansi-wl-pprint-0.6.9’
    • In the first argument of ‘Just’, namely ‘supportedFormatsDoc’
      In the first argument of ‘footerDoc’, namely
        ‘(Just supportedFormatsDoc)’
      In the second argument of ‘(<>)’, namely
        ‘footerDoc (Just supportedFormatsDoc)’
    |
198 |   <> footerDoc (Just supportedFormatsDoc)
    |                      ^^^^^^^^^^^^^^^^^^^

	ansi-wl-pprint-0.6.9	ansi-wl-pprint-1.0.2
optparse-applicative-0.17.1.0	OK	OK
optparse-applicative-0.18.1.0	NG (above error)	OK

Fail to install, particularly toysolver-0.6.0

I get everything installed until toysolver-0.6.0.
The error is

cabal: Entering directory '.'
Configuring toysolver-0.6.0...
Preprocessing library for toysolver-0.6.0..
Building library for toysolver-0.6.0..
Preprocessing executable 'toyconvert' for toysolver-0.6.0..
Building executable 'toyconvert' for toysolver-0.6.0..
Preprocessing executable 'toyqbf' for toysolver-0.6.0..
Building executable 'toyqbf' for toysolver-0.6.0..
Preprocessing executable 'toysat' for toysolver-0.6.0..
Building executable 'toysat' for toysolver-0.6.0..
Preprocessing executable 'toysmt' for toysolver-0.6.0..
cabal.real: can't find source for Smtlib/Parsers/CommonParsers in app/toysmt,
Smtlib, dist/build/toysmt/autogen, dist/build/global-autogen
cabal: Leaving directory '.'
cabal: Error: some packages failed to install:
toysolver-0.6.0-JkBmbHh9l5D16lXt1wYJQ2 failed during the building phase. The
exception was:
ExitFailure 1

The line "cabal.real: can't find source for Smtlib/Parsers/CommonParsers in app/toysmt" is causing the problem. How to deal with this? I am using Mac OS maverick.

Ambiguous occurrence ‘singleton

compiling with allow-newer and ghc 9.0.2 (base 4.15.1) I encountered the following error:

src/ToySolver/Data/LA.hs:302:43: error:
Ambiguous occurrence ‘singleton’
It could refer to
either ‘Data.List.singleton’,
imported from ‘Data.List’ at src/ToySolver/Data/LA.hs:70:1-16
(and originally defined in ‘base-4.15.1.0:Data.OldList’)
or ‘Data.Interval.singleton’,
imported from ‘Data.Interval’ at src/ToySolver/Data/LA.hs:75:1-20

I assume this is easy to resolve! Thank you!

release a toysolver to hackage that builds with 8.8 ... 8.0 please? :)

would be super handy!

https://github.com/haskell-CI/haskell-ci has some resources to help generate a full build range, though I / @hvr or others can probably help

conflict analysis bug

% toysat --maxsat file_rwpms_wcnf_L2_V150_C1000_H150_0.wcnf
c arch = x86_64
c os = darwin
c compiler = ghc 7.0
c Solving starts ...
c solving time = 0.003s
c #decision = 699
c #conflict = 0
c #restart = 0
o 1136
c Solving starts ...
c solving time = 0.011s
c #decision = 1110
c #conflict = 2
c #restart = 0
o 1135
c Solving starts ...
c solving time = 0.018s
c #decision = 1445
c #conflict = 2
c #restart = 0
o 1130
c Solving starts ...
c solving time = 0.022s
c #decision = 1715
c #conflict = 3
c #restart = 0
o 1126
c Solving starts ...
c solving time = 0.027s
c #decision = 2083
c #conflict = 5
c #restart = 0
o 1125
c Solving starts ...
c solving time = 0.036s
c #decision = 2561
c #conflict = 5
c #restart = 0
o 1118
c Solving starts ...
c solving time = 0.059s
c #decision = 2806
c #conflict = 13
c #restart = 0
o 1115
c Solving starts ...
toysat: analyzeConflict: should not happen: loop fromList [-92,586] fromList [-140,-129,-121,-100,-72,-59,-42,-11,81,142,153,155,164,168,175,176,188,189,199,211,212,214,216,222,223,227,228,229,232,238,239,240,242,247,249,250,251,255,256,260,262,266,268,270,283,299,307,313,315,316,321,339,345,346,348,349,350,352,353,356,365,366,367,370,375,379,381,383,388,390,394,400,404,408,415,428,431,435,437,446,448,449,454,455,461,466,468,472,476,479,491,492,494,495,496,499,501,507,513,517,522,528,534,536,537,538,540,541,543,544,545,551,553,563,565,567,573,574,577,582,583,588,590,591,592,596,597,598,599,601,612,619,624,625,632,634,642,643,654,657,660,669,670,673,675,680,681,682,685,687,692,713,714,715,720,729,730,748,750,753,755,762,768,771,773,774,777,782,783,784,785,789,793,807,809,813,819,826,827,829,830,836,840,842,848,849,853,855,861,862,863,864,870,873,875,876,877,878,880,882,883,885,886,887,889,890,897,898,902,906,908,911,920,928,932,933,935,938,948,960,962,966,967,969,971,977,984,991,992] fromList [-985,-972,-677,-92,-18,45,147,374,648,751,963] []

wrong optimum for normalized-minisat15_5_3_4_ic.opb

http://www.cril.univ-artois.fr/PB12/results/trace.php?idev=67&idjob=3724848