dbueno / funsat

An efficient, embeddable DPLL SAT solver in Haskell

This URL has Read+Write access

funsat / funsat.cabal
100644 88 lines (79 sloc) 3.068 kb
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
Name: funsat
Version: 0.6.1
Cabal-Version: >= 1.2
Description:
 
    Funsat is a native Haskell SAT solver that uses modern techniques for
    solving SAT instances. Current features include two-watched literals,
    conflict-directed learning, non-chronological backtracking, a VSIDS-like
    dynamic variable ordering, and restarts. Our goal is to facilitate
    convenient embedding of a reasonably fast SAT solver as a constraint
    solving backend in other applications.
 
    Currently along this theme we provide unsatisfiable core generation (see
    "Funsat.Resolution") and a logical circuit interface (see "Funsat.Circuit").
 
    New in 0.6: circuits and BSD3 license.
 
Synopsis: A modern DPLL-style SAT solver
Homepage: http://github.com/dbueno/funsat
Category: Algorithms
Stability: beta
License: BSD3
License-file: LICENSE
Author: Denis Bueno
Maintainer: Denis Bueno <dbueno@gmail.com>
Build-type: Simple
Extra-source-files: README CHANGES
 
 
Executable funsat
 Main-is: Main.hs
 Ghc-options: -funbox-strict-fields
                      -Wall -fwarn-tabs
                      -fno-warn-name-shadowing
                      -fno-warn-orphans
 Extensions: CPP, ScopedTypeVariables
 CPP-options: -DTESTING
 Hs-source-dirs: . src tests
 Other-modules:
                      Control.Monad.MonadST
                      Funsat.FastDom
                      Funsat.Monad
                      Funsat.Resolution
                      Funsat.Solver
                      Funsat.Types
                      Funsat.Utils
                      Text.Tabular
                      Properties
 
 Build-Depends: base,
                      random,
                      containers,
                      pretty,
                      mtl,
                      array,
                      QuickCheck < 2,
                      parse-dimacs >= 1.2 && < 2,
                      bitset < 1,
                      bimap >= 0.2 && < 0.3,
                      fgl,
                      time
 
Library
 Exposed-modules: Control.Monad.MonadST
                      Funsat.Circuit
                      Funsat.Monad
                      Funsat.Resolution
                      Funsat.Solver
                      Funsat.Types
                      Text.Tabular
 Other-modules: Funsat.FastDom Funsat.Utils
 Ghc-options: -funbox-strict-fields
                      -Wall -fwarn-tabs
                      -fno-warn-name-shadowing
                      -fno-warn-orphans
 Extensions: CPP, ScopedTypeVariables
 Hs-source-dirs: src
 Build-Depends: base,
                      containers,
                      pretty,
                      mtl,
                      array,
                      QuickCheck < 2,
                      parse-dimacs >= 1.2 && < 2,
                      bitset < 1,
                      bimap >= 0.2 && < 0.3,
                      fgl