satchmo: SAT encoding monad

Example

import Prelude hiding ( not )

import Satchmo.Binary.Op.Fixed
import qualified Satchmo.Binary.Op.Flexible
import Satchmo.Solver.Minisat
import Satchmo.Boolean
import Satchmo.Code

import System.Environment

main :: IO ()
main = do
    [ n ] <- getArgs
    res <- solve $ do
        x <- Satchmo.Binary.Op.Flexible.constant $ read n
        a <- number $ width x
        notone a
        b <- number $ width x
        notone b
        ab <- times a b
        monadic assert [ equals ab x ]
        return $ decode [ a, b ]
    print res

notone f = do
    one <- Satchmo.Binary.Op.Flexible.constant 1
    e <- equals f one
    assert [ not e ]

More Documentation and Examples

also, see lecture notes for chapter Software zur SAT-Kodierung (in German) from my introductory course on Constraint Programming

Project structure

• satchmo (base package, provides API)
• backends
  • satchmo-backends provides interface to minisat, quantor, qube. (Solver will be started as external process)
    These solvers must be obtained and installed separately. Author and license of satchmo-* has no correlation to author and license of these individual solvers.
  • satchmo-funsat, uses funsat (as a library)
• satchmo-examples (show how to use API)

Install

cabal install [--global --root-cmd=sudo] satchmo
cabal install [--global --root-cmd=sudo] satchmo-backends

Release Status

see below for development sources

API documentation

Bugs, Feature Requests

Development source tree

git clone git://dfa.imn.htwk-leipzig.de/srv/git/satchmo.git
git clone git://dfa.imn.htwk-leipzig.de/srv/git/satchmo-backends.git
git clone git://dfa.imn.htwk-leipzig.de/srv/git/satchmo-examples.git

browse source trees: (gitweb)

History