packages feed

puresat-0.1: puresat.cabal

cabal-version:      3.4
name:               puresat
version:            0.1
synopsis:           Pure Haskell SAT-solver
category:           Data
description:
  SAT Solver implemented in Haskell.

  PureSAT uses DPLL with non-chronological backtracking and learning of binaary clauses.
  Solver is in no-comparison to the state of the art solvers, but it's fast enough to solve sudoku.

homepage:           https://github.com/phadej/puresat
license:            BSD-3-Clause
license-file:       LICENSE
author:             Oleg Grenrus <oleg.grenrus@iki.fi>
maintainer:         Oleg Grenrus <oleg.grenrus@iki.fi>
copyright:          (c) 2024 Oleg Grenrus
build-type:         Simple
tested-with:        GHC ==9.6.6 || ==9.8.2 || ==9.10.1
extra-doc-files:    CHANGELOG.md

-- cabal-fmt: glob-files dimacs/**/*.cnf
extra-source-files:
  dimacs/aim/aim-100-1_6-no-1.cnf
  dimacs/aim/aim-100-1_6-no-2.cnf
  dimacs/aim/aim-100-1_6-no-3.cnf
  dimacs/aim/aim-100-1_6-no-4.cnf
  dimacs/aim/aim-100-1_6-yes1-1.cnf
  dimacs/aim/aim-100-1_6-yes1-2.cnf
  dimacs/aim/aim-100-1_6-yes1-3.cnf
  dimacs/aim/aim-100-1_6-yes1-4.cnf
  dimacs/aim/aim-100-2_0-no-1.cnf
  dimacs/aim/aim-100-2_0-no-2.cnf
  dimacs/aim/aim-100-2_0-no-3.cnf
  dimacs/aim/aim-100-2_0-no-4.cnf
  dimacs/aim/aim-100-2_0-yes1-1.cnf
  dimacs/aim/aim-100-2_0-yes1-2.cnf
  dimacs/aim/aim-100-2_0-yes1-3.cnf
  dimacs/aim/aim-100-2_0-yes1-4.cnf
  dimacs/aim/aim-100-3_4-yes1-1.cnf
  dimacs/aim/aim-100-3_4-yes1-2.cnf
  dimacs/aim/aim-100-3_4-yes1-3.cnf
  dimacs/aim/aim-100-3_4-yes1-4.cnf
  dimacs/aim/aim-100-6_0-yes1-1.cnf
  dimacs/aim/aim-100-6_0-yes1-2.cnf
  dimacs/aim/aim-100-6_0-yes1-3.cnf
  dimacs/aim/aim-100-6_0-yes1-4.cnf
  dimacs/aim/aim-200-1_6-no-1.cnf
  dimacs/aim/aim-200-1_6-no-2.cnf
  dimacs/aim/aim-200-1_6-no-3.cnf
  dimacs/aim/aim-200-1_6-no-4.cnf
  dimacs/aim/aim-200-1_6-yes1-1.cnf
  dimacs/aim/aim-200-1_6-yes1-2.cnf
  dimacs/aim/aim-200-1_6-yes1-3.cnf
  dimacs/aim/aim-200-1_6-yes1-4.cnf
  dimacs/aim/aim-200-2_0-no-1.cnf
  dimacs/aim/aim-200-2_0-no-2.cnf
  dimacs/aim/aim-200-2_0-no-3.cnf
  dimacs/aim/aim-200-2_0-no-4.cnf
  dimacs/aim/aim-200-2_0-yes1-1.cnf
  dimacs/aim/aim-200-2_0-yes1-2.cnf
  dimacs/aim/aim-200-2_0-yes1-3.cnf
  dimacs/aim/aim-200-2_0-yes1-4.cnf
  dimacs/aim/aim-200-3_4-yes1-1.cnf
  dimacs/aim/aim-200-3_4-yes1-2.cnf
  dimacs/aim/aim-200-3_4-yes1-3.cnf
  dimacs/aim/aim-200-3_4-yes1-4.cnf
  dimacs/aim/aim-200-6_0-yes1-1.cnf
  dimacs/aim/aim-200-6_0-yes1-2.cnf
  dimacs/aim/aim-200-6_0-yes1-3.cnf
  dimacs/aim/aim-200-6_0-yes1-4.cnf
  dimacs/aim/aim-50-1_6-no-1.cnf
  dimacs/aim/aim-50-1_6-no-2.cnf
  dimacs/aim/aim-50-1_6-no-3.cnf
  dimacs/aim/aim-50-1_6-no-4.cnf
  dimacs/aim/aim-50-1_6-yes1-1.cnf
  dimacs/aim/aim-50-1_6-yes1-2.cnf
  dimacs/aim/aim-50-1_6-yes1-3.cnf
  dimacs/aim/aim-50-1_6-yes1-4.cnf
  dimacs/aim/aim-50-2_0-no-1.cnf
  dimacs/aim/aim-50-2_0-no-2.cnf
  dimacs/aim/aim-50-2_0-no-3.cnf
  dimacs/aim/aim-50-2_0-no-4.cnf
  dimacs/aim/aim-50-2_0-yes1-1.cnf
  dimacs/aim/aim-50-2_0-yes1-2.cnf
  dimacs/aim/aim-50-2_0-yes1-3.cnf
  dimacs/aim/aim-50-2_0-yes1-4.cnf
  dimacs/aim/aim-50-3_4-yes1-1.cnf
  dimacs/aim/aim-50-3_4-yes1-2.cnf
  dimacs/aim/aim-50-3_4-yes1-3.cnf
  dimacs/aim/aim-50-3_4-yes1-4.cnf
  dimacs/aim/aim-50-6_0-yes1-1.cnf
  dimacs/aim/aim-50-6_0-yes1-2.cnf
  dimacs/aim/aim-50-6_0-yes1-3.cnf
  dimacs/aim/aim-50-6_0-yes1-4.cnf
  dimacs/ais/ais10.cnf
  dimacs/ais/ais12.cnf
  dimacs/ais/ais6.cnf
  dimacs/ais/ais8.cnf
  dimacs/bf/bf0432-007.cnf
  dimacs/bf/bf1355-075.cnf
  dimacs/bf/bf1355-638.cnf
  dimacs/bf/bf2670-001.cnf
  dimacs/blocksworld/anomaly.cnf
  dimacs/blocksworld/bw_large.a.cnf
  dimacs/blocksworld/bw_large.b.cnf
  dimacs/blocksworld/bw_large.c.cnf
  dimacs/blocksworld/huge.cnf
  dimacs/blocksworld/medium.cnf
  dimacs/bmc/bmc-ibm-1.cnf
  dimacs/bmc/bmc-ibm-2.cnf
  dimacs/bmc/bmc-ibm-3.cnf
  dimacs/bmc/bmc-ibm-4.cnf
  dimacs/bmc/bmc-ibm-5.cnf
  dimacs/dubois/dubois100.cnf
  dimacs/dubois/dubois20.cnf
  dimacs/dubois/dubois21.cnf
  dimacs/dubois/dubois22.cnf
  dimacs/dubois/dubois23.cnf
  dimacs/dubois/dubois24.cnf
  dimacs/dubois/dubois25.cnf
  dimacs/dubois/dubois26.cnf
  dimacs/dubois/dubois27.cnf
  dimacs/dubois/dubois28.cnf
  dimacs/dubois/dubois29.cnf
  dimacs/dubois/dubois30.cnf
  dimacs/dubois/dubois50.cnf
  dimacs/hanoi/hanoi4.cnf
  dimacs/hanoi/hanoi5.cnf
  dimacs/inductive-inference/ii16a1.cnf
  dimacs/inductive-inference/ii16a2.cnf
  dimacs/inductive-inference/ii16b1.cnf
  dimacs/inductive-inference/ii16b2.cnf
  dimacs/inductive-inference/ii16c1.cnf
  dimacs/inductive-inference/ii16c2.cnf
  dimacs/inductive-inference/ii16d1.cnf
  dimacs/inductive-inference/ii16d2.cnf
  dimacs/inductive-inference/ii16e1.cnf
  dimacs/inductive-inference/ii16e2.cnf
  dimacs/inductive-inference/ii8a1.cnf
  dimacs/inductive-inference/ii8a2.cnf
  dimacs/inductive-inference/ii8a3.cnf
  dimacs/inductive-inference/ii8a4.cnf
  dimacs/inductive-inference/ii8b1.cnf
  dimacs/inductive-inference/ii8b2.cnf
  dimacs/inductive-inference/ii8b3.cnf
  dimacs/inductive-inference/ii8b4.cnf
  dimacs/inductive-inference/ii8c1.cnf
  dimacs/inductive-inference/ii8c2.cnf
  dimacs/inductive-inference/ii8d1.cnf
  dimacs/inductive-inference/ii8d2.cnf
  dimacs/inductive-inference/ii8e1.cnf
  dimacs/inductive-inference/ii8e2.cnf
  dimacs/jnh/jnh1.cnf
  dimacs/jnh/jnh10.cnf
  dimacs/jnh/jnh11.cnf
  dimacs/jnh/jnh12.cnf
  dimacs/jnh/jnh13.cnf
  dimacs/jnh/jnh14.cnf
  dimacs/jnh/jnh15.cnf
  dimacs/jnh/jnh16.cnf
  dimacs/jnh/jnh17.cnf
  dimacs/jnh/jnh18.cnf
  dimacs/jnh/jnh19.cnf
  dimacs/jnh/jnh2.cnf
  dimacs/jnh/jnh20.cnf
  dimacs/jnh/jnh201.cnf
  dimacs/jnh/jnh202.cnf
  dimacs/jnh/jnh203.cnf
  dimacs/jnh/jnh204.cnf
  dimacs/jnh/jnh205.cnf
  dimacs/jnh/jnh206.cnf
  dimacs/jnh/jnh207.cnf
  dimacs/jnh/jnh208.cnf
  dimacs/jnh/jnh209.cnf
  dimacs/jnh/jnh210.cnf
  dimacs/jnh/jnh211.cnf
  dimacs/jnh/jnh212.cnf
  dimacs/jnh/jnh213.cnf
  dimacs/jnh/jnh214.cnf
  dimacs/jnh/jnh215.cnf
  dimacs/jnh/jnh216.cnf
  dimacs/jnh/jnh217.cnf
  dimacs/jnh/jnh218.cnf
  dimacs/jnh/jnh219.cnf
  dimacs/jnh/jnh220.cnf
  dimacs/jnh/jnh3.cnf
  dimacs/jnh/jnh301.cnf
  dimacs/jnh/jnh302.cnf
  dimacs/jnh/jnh303.cnf
  dimacs/jnh/jnh304.cnf
  dimacs/jnh/jnh305.cnf
  dimacs/jnh/jnh306.cnf
  dimacs/jnh/jnh307.cnf
  dimacs/jnh/jnh308.cnf
  dimacs/jnh/jnh309.cnf
  dimacs/jnh/jnh310.cnf
  dimacs/jnh/jnh4.cnf
  dimacs/jnh/jnh5.cnf
  dimacs/jnh/jnh6.cnf
  dimacs/jnh/jnh7.cnf
  dimacs/jnh/jnh8.cnf
  dimacs/jnh/jnh9.cnf
  dimacs/logistics/logistics.a.cnf
  dimacs/logistics/logistics.b.cnf
  dimacs/logistics/logistics.c.cnf
  dimacs/logistics/logistics.d.cnf
  dimacs/parity/par16-1-c.cnf
  dimacs/parity/par16-1.cnf
  dimacs/parity/par16-2-c.cnf
  dimacs/parity/par16-2.cnf
  dimacs/parity/par16-3-c.cnf
  dimacs/parity/par16-3.cnf
  dimacs/parity/par16-4-c.cnf
  dimacs/parity/par16-4.cnf
  dimacs/parity/par16-5-c.cnf
  dimacs/parity/par16-5.cnf
  dimacs/parity/par8-1-c.cnf
  dimacs/parity/par8-1.cnf
  dimacs/parity/par8-2-c.cnf
  dimacs/parity/par8-2.cnf
  dimacs/parity/par8-3-c.cnf
  dimacs/parity/par8-3.cnf
  dimacs/parity/par8-4-c.cnf
  dimacs/parity/par8-4.cnf
  dimacs/parity/par8-5-c.cnf
  dimacs/parity/par8-5.cnf
  dimacs/phole/hole10.cnf
  dimacs/phole/hole4.cnf
  dimacs/phole/hole6.cnf
  dimacs/phole/hole7.cnf
  dimacs/phole/hole8.cnf
  dimacs/phole/hole9.cnf
  dimacs/pret/pret150_25.cnf
  dimacs/pret/pret150_40.cnf
  dimacs/pret/pret150_60.cnf
  dimacs/pret/pret150_75.cnf
  dimacs/pret/pret60_25.cnf
  dimacs/pret/pret60_40.cnf
  dimacs/pret/pret60_60.cnf
  dimacs/pret/pret60_75.cnf
  dimacs/QG/qg1-07.cnf
  dimacs/QG/qg1-08.cnf
  dimacs/QG/qg2-07.cnf
  dimacs/QG/qg2-08.cnf
  dimacs/QG/qg3-08.cnf
  dimacs/QG/qg4-08.cnf
  dimacs/ssa/ssa0432-003.cnf
  dimacs/ssa/ssa2670-130.cnf
  dimacs/ssa/ssa2670-141.cnf
  dimacs/ssa/ssa6288-047.cnf
  dimacs/ssa/ssa7552-038.cnf
  dimacs/ssa/ssa7552-158.cnf
  dimacs/ssa/ssa7552-159.cnf
  dimacs/ssa/ssa7552-160.cnf

source-repository head
  type:     git
  location: https://github.com/phadej/puresat

flag exe
  description: Build executable
  default:     False
  manual:      True

common language
  default-language:   Haskell2010
  default-extensions:
    BangPatterns
    DeriveTraversable
    DerivingStrategies
    GADTs
    PatternSynonyms
    RankNTypes
    RoleAnnotations
    ScopedTypeVariables
    StandaloneDeriving
    StandaloneKindSignatures
    TypeApplications

library
  import:          language
  hs-source-dirs:  lib
  exposed-modules:
    Control.Monad.SAT
    PureSAT

  other-modules:   EST
  build-depends:
    , base
    , containers
    , puresat:internal

library internal
  import:          language
  hs-source-dirs:  src
  exposed-modules:
    PureSAT.Assert
    PureSAT.Base
    PureSAT.Boost
    PureSAT.Clause2
    PureSAT.LBool
    PureSAT.LCG
    PureSAT.Level
    PureSAT.LitSet
    PureSAT.LitTable
    PureSAT.LitVar
    PureSAT.Main
    PureSAT.PartialAssignment
    PureSAT.Prim
    PureSAT.Satisfied
    PureSAT.SparseMaxHeap
    PureSAT.SparseSet
    PureSAT.Stats
    PureSAT.Trail
    PureSAT.Utils
    PureSAT.VarSet
    PureSAT.Vec

  build-depends:
    , base        >=4.18.2.1 && <4.21
    , containers  >=0.6.7    && <0.8
    , primitive   ^>=0.9.0.0

library dimacs
  import:          language
  hs-source-dirs:  src-dimacs
  build-depends:
    , base
    , bytestring        ^>=0.11.5.3 || ^>=0.12.1.0
    , parsec            ^>=3.1.16.1
    , puresat:internal

  exposed-modules: PureSAT.DIMACS

executable puresat
  import:         language

  if !flag(exe)
    buildable: False

  hs-source-dirs: exe
  main-is:        puresat.hs
  build-depends:
    , base
    , optparse-applicative  ^>=0.18.1.0
    , puresat:dimacs
    , puresat:internal

test-suite puresat-test
  import:         language
  type:           exitcode-stdio-1.0
  hs-source-dirs: test
  main-is:        puresat-test.hs
  build-depends:
    , base
    , puresat
    , QuickCheck        ^>=2.15.0.1
    , tasty             ^>=1.5
    , tasty-quickcheck  ^>=0.11

test-suite puresat-small
  import:         language
  type:           exitcode-stdio-1.0
  hs-source-dirs: test
  main-is:        puresat-small.hs
  build-depends:
    , base
    , primitive
    , puresat

test-suite puresat-dimacs
  import:         language
  type:           exitcode-stdio-1.0
  hs-source-dirs: test
  main-is:        puresat-dimacs.hs
  build-depends:
    , base
    , filepath
    , minisat
    , primitive
    , puresat:dimacs
    , puresat:internal
    , tasty             ^>=1.5
    , tasty-hunit

test-suite sat-simple-sudoku
  import:         language
  type:           exitcode-stdio-1.0
  hs-source-dirs: examples
  ghc-options:    -rtsopts
  main-is:        sat-simple-sudoku.hs
  build-depends:
    , base
    , puresat