diff --git a/AUTHORS.md b/AUTHORS.md
new file mode 100644
--- /dev/null
+++ b/AUTHORS.md
@@ -0,0 +1,12 @@
+Authors
+=======
+
+`ersatz` started as a one man project by [Edward Kmett](mailto:ekmett@gmail.com) [@ekmett](https://github.com/ekmett).
+However, it then languished for 3 years after Don Stewart [@donsbot](https://github.com/donsbot) released perfectly adequate bindings for yices.
+
+It revived by [Johan Kiviniemi](mailto:lens@johan.kiviniemi.name) [@ion1](https://github.com/ion1) after he
+shamed the original author into polishing it up and releasing it.
+
+Omission from this page is by no means an attempt to discount your contributions! Thank you for all of your help!
+
+-Edward Kmett
diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,3 @@
+0.1
+---
+* Repository Initialized
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,32 @@
+Copyright (c) 2010-2013 Edward Kmett
+Copyright (c) 2013 Johan Kiviniemi
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are
+met:
+
+    * Redistributions of source code must retain the above copyright
+      notice, this list of conditions and the following disclaimer.
+
+    * Redistributions in binary form must reproduce the above
+      copyright notice, this list of conditions and the following
+      disclaimer in the documentation and/or other materials provided
+      with the distribution.
+
+    * Neither the name of Edward Kmett nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,70 @@
+# Ersatz
+
+[![Build Status](https://secure.travis-ci.org/ekmett/ersatz.png)](http://travis-ci.org/ekmett/ersatz)
+
+Ersatz is a library for generating QSAT (CNF/QBF) problems using a monad. It takes care of generating the normal form, encoding your problem, marshaling the data to an external solver, and parsing and interpreting the result into Haskell types.
+
+What differentiates Ersatz is the use of observable sharing in the API.
+
+For instance to define a full adder:
+
+```haskell
+full_adder :: Bit -> Bit -> Bit -> (Bit, Bit)
+full_adder a b cin = (s2, c1 || c2)
+  where (s1,c1) = half_adder a b
+        (s2,c2) = half_adder s1 cin
+
+half_adder :: Bit -> Bit -> (Bit, Bit)
+half_adder a b = (a `xor` b, a && b)
+```
+
+as opposed to the following code in [satchmo](http://dfa.imn.htwk-leipzig.de/satchmo/):
+
+
+```haskell
+full_adder :: Boolean -> Boolean -> Boolean
+           -> SAT ( Boolean, Boolean )
+full_adder a b c = do
+  let s x y z = sum $ map fromEnum [x,y,z]
+  r <- fun3 ( \ x y z -> odd $ s x y z ) a b c
+  d <- fun3 ( \ x y z -> 1   < s x y z ) a b c
+  return ( r, d )
+
+half_adder :: Boolean -> Boolean
+           -> SAT ( Boolean, Boolean )
+half_adder a b = do
+  let s x y = sum $ map fromEnum [x,y]
+  r <- fun2 ( \ x y -> odd $ s x y ) a b
+  d <- fun2 ( \ x y -> 1   < s x y ) a b
+  return ( r, d )
+```
+
+This enables you to use the a much richer subset of Haskell than the purely monadic meta-language, and it becomes much easier to see that the resulting encoding is correct.
+
+To allocate fresh existentially or universally quantified variables or to assert that a Bit is true and add the attendant circuit with sharing to the current problem you use the SAT monad.
+
+```haskell
+verify_currying :: SAT m ()
+verify_currying = do
+  (x::Bit, y::Bit, z::Bit) <- forall
+  assert $ ((x && y) ==> z) === (x ==> y ==> z)
+```
+
+We can then hand that off to a SAT solver, and get back an answer:
+
+```haskell
+main = solveWith minisat verify_currying >>= print
+```
+
+Support is offered for decoding various Haskell datatypes from the
+solution provided by the SAT solver.
+
+Contact Information
+-------------------
+
+Contributions and bug reports are welcome!
+
+Please feel free to contact me through github or on the #haskell IRC channel on irc.freenode.net.
+
+-Edward Kmett
+
diff --git a/Setup.lhs b/Setup.lhs
new file mode 100644
--- /dev/null
+++ b/Setup.lhs
@@ -0,0 +1,44 @@
+#!/usr/bin/runhaskell
+\begin{code}
+{-# OPTIONS_GHC -Wall #-}
+module Main (main) where
+
+import Data.List ( nub )
+import Data.Version ( showVersion )
+import Distribution.Package ( PackageName(PackageName), PackageId, InstalledPackageId, packageVersion, packageName )
+import Distribution.PackageDescription ( PackageDescription(), TestSuite(..) )
+import Distribution.Simple ( defaultMainWithHooks, UserHooks(..), simpleUserHooks )
+import Distribution.Simple.Utils ( rewriteFile, createDirectoryIfMissingVerbose)
+import Distribution.Simple.BuildPaths ( autogenModulesDir )
+import Distribution.Simple.Setup ( BuildFlags(buildVerbosity), fromFlag)
+import Distribution.Simple.LocalBuildInfo ( withLibLBI, withTestLBI, LocalBuildInfo(), ComponentLocalBuildInfo(componentPackageDeps) )
+import Distribution.Verbosity ( Verbosity)
+import System.FilePath ( (</>) )
+
+main :: IO ()
+main = defaultMainWithHooks simpleUserHooks
+  { buildHook = \pkg lbi hooks flags -> do
+     generateBuildModule (fromFlag (buildVerbosity flags)) pkg lbi
+     buildHook simpleUserHooks pkg lbi hooks flags
+  }
+
+generateBuildModule :: Verbosity -> PackageDescription -> LocalBuildInfo -> IO ()
+generateBuildModule verbosity pkg lbi = do
+  let dir = autogenModulesDir lbi
+  createDirectoryIfMissingVerbose verbosity True dir
+  withLibLBI pkg lbi $ \_ libcfg -> do
+    withTestLBI pkg lbi $ \suite suitecfg -> do
+      rewriteFile (dir </> "Build_" ++ testName suite ++ ".hs") $ unlines
+        [ "module Build_" ++ testName suite ++ " where"
+        , "deps :: [String]"
+        , "deps = " ++ (show $ formatdeps (testDeps libcfg suitecfg))
+        ]
+  where
+    formatdeps = map (formatone . snd)
+    formatone p = case packageName p of
+      PackageName n -> n ++ "-" ++ showVersion (packageVersion p)
+
+testDeps :: ComponentLocalBuildInfo -> ComponentLocalBuildInfo -> [(InstalledPackageId, PackageId)]
+testDeps xs ys = nub $ componentPackageDeps xs ++ componentPackageDeps ys
+
+\end{code}
diff --git a/ersatz.cabal b/ersatz.cabal
new file mode 100644
--- /dev/null
+++ b/ersatz.cabal
@@ -0,0 +1,102 @@
+name:           ersatz
+version:        0.1
+license:        BSD3
+license-file:   LICENSE
+author:         Edward A. Kmett, Johan Kiviniemi
+maintainer:     Edward A. Kmett <ekmett@gmail.com>
+stability:      experimental
+homepage:       http://comonad.com/reader
+category:       Logic, Algorithms
+synopsis:       A monad for expressing SAT or QSAT problems using observable sharing.
+description:    A monad for expressing SAT or QSAT problems using observable sharing.
+  .
+  For example, we can express a full-adder with:
+  .
+  > full_adder :: Bit -> Bit -> Bit -> (Bit, Bit)
+  > full_adder a b cin = (s2, c1 || c2)
+  >   where (s1,c1) = half_adder a b
+  >         (s2,c2) = half_adder s1 cin
+  .
+  > half_adder :: Bit -> Bit -> (Bit, Bit)
+  > half_adder a b = (a `xor` b, a && b)
+copyright:      (c) 2010-2013 Edward Kmett, (c) 2013 Johan Kiviniemi
+build-type:     Custom
+cabal-version:  >= 1.10
+tested-with:    GHC == 7.6.2
+extra-source-files:
+  AUTHORS.md
+  README.md
+  CHANGELOG.md
+
+library
+  ghc-options: -Wall
+  hs-source-dirs: src
+  default-language: Haskell2010
+
+  build-depends:
+    array >= 0.2 && < 0.5,
+    base >= 4 && < 6,
+    containers >= 0.2.0.1,
+    data-default >= 0.5 && < 0.6,
+    ghc-prim,
+    mtl >= 1.1 && < 2.2,
+    process == 1.1.*,
+    temporary == 1.1.*,
+    transformers == 0.3.*,
+    unordered-containers == 0.2.*
+
+  exposed-modules:
+    Ersatz
+    Ersatz.Bit
+    Ersatz.Bits
+    Ersatz.Decoding
+    Ersatz.Equatable
+    Ersatz.Encoding
+    Ersatz.Internal.Circuit
+    Ersatz.Internal.Formula
+    Ersatz.Internal.Literal
+    Ersatz.Monad
+    Ersatz.Problem
+    Ersatz.Solution
+    Ersatz.Solver
+    Ersatz.Solver.Minisat
+    Ersatz.Variable
+
+  other-modules:
+    Ersatz.Internal.Parser
+    Ersatz.Internal.StableName
+
+test-suite properties
+  type: exitcode-stdio-1.0
+  ghc-options: -Wall
+  default-language: Haskell2010
+  build-depends:
+    ersatz,
+    base >= 4 && < 6,
+    mtl >= 1.1 && < 2.2,
+    transformers == 0.3.*,
+    containers >= 0.2.0.1,
+    array >= 0.2 && < 0.5,
+    data-reify >= 0.5 && < 0.7,
+    test-framework >= 0.2.4 && < 0.9,
+    test-framework-quickcheck >= 0.2.4 && < 0.4,
+    test-framework-hunit >= 0.2.4 && < 0.4,
+    QuickCheck >= 1.2.0.0 && < 2.6,
+    HUnit >= 1.2.2.1 && < 1.3
+
+  hs-source-dirs: tests
+  Main-is: properties.hs
+
+test-suite doctests
+  type:    exitcode-stdio-1.0
+  main-is: doctests.hs
+  default-language: Haskell2010
+  build-depends:
+    base < 5,
+    directory >= 1.0,
+    doctest >= 0.9.1,
+    filepath
+  ghc-options: -Wall -threaded
+  if impl(ghc<7.6.1)
+    ghc-options: -Werror
+  hs-source-dirs: tests
diff --git a/src/Ersatz.hs b/src/Ersatz.hs
new file mode 100644
--- /dev/null
+++ b/src/Ersatz.hs
@@ -0,0 +1,32 @@
+--------------------------------------------------------------------
+-- |
+-- Copyright :  (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013
+-- License   :  BSD3
+-- Maintainer:  Edward Kmett <ekmett@gmail.com>
+-- Stability :  experimental
+-- Portability: non-portable
+--
+--------------------------------------------------------------------
+module Ersatz
+  ( module Ersatz.Bit
+  , module Ersatz.Bits
+  , module Ersatz.Decoding
+  , module Ersatz.Equatable
+  , module Ersatz.Encoding
+  , module Ersatz.Monad
+  , module Ersatz.Problem
+  , module Ersatz.Solution
+  , module Ersatz.Solver
+  , module Ersatz.Variable
+  ) where
+
+import Ersatz.Bit
+import Ersatz.Bits
+import Ersatz.Decoding
+import Ersatz.Equatable
+import Ersatz.Encoding
+import Ersatz.Monad
+import Ersatz.Problem
+import Ersatz.Solution
+import Ersatz.Solver
+import Ersatz.Variable
diff --git a/src/Ersatz/Bit.hs b/src/Ersatz/Bit.hs
new file mode 100644
--- /dev/null
+++ b/src/Ersatz/Bit.hs
@@ -0,0 +1,284 @@
+{-# LANGUAGE TypeFamilies, TypeOperators, FlexibleInstances, DeriveDataTypeable, DeriveGeneric, DefaultSignatures, FlexibleContexts, UndecidableInstances #-}
+{-# OPTIONS_HADDOCK not-home #-}
+--------------------------------------------------------------------
+-- |
+-- Copyright :  (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013
+-- License   :  BSD3
+-- Maintainer:  Edward Kmett <ekmett@gmail.com>
+-- Stability :  experimental
+-- Portability: non-portable
+--
+--------------------------------------------------------------------
+module Ersatz.Bit
+  ( Bit(..)
+  , assert
+  , Boolean(..)
+  ) where
+
+import Prelude hiding ((&&),(||),not,and,or)
+import qualified Prelude
+
+import Control.Applicative
+import Data.Traversable (Traversable, traverse)
+import Data.Typeable
+import Ersatz.Decoding
+import Ersatz.Encoding
+import Ersatz.Monad
+import Ersatz.Internal.Circuit
+import Ersatz.Internal.Formula
+import Ersatz.Internal.Literal
+import Ersatz.Internal.StableName
+import Ersatz.Solution
+import Ersatz.Variable
+import GHC.Generics
+import System.IO.Unsafe
+
+infixr 3 &&, &&#
+infixr 2 ||, ||#
+infixr 0 ==>, ==>#
+
+-- Bit
+
+-- | A 'Bit' provides a reference to a possibly indeterminate boolean
+-- value that can be determined by an external SAT solver.
+newtype Bit = Bit (Circuit Bit)
+  deriving (Show, Typeable)
+
+instance Boolean Bit where
+  -- improve the stablemap this way
+  bool True  = true
+  bool False = false
+  true  = Bit (Var (lit True))
+  false = Bit (Var (lit False))
+  Bit (And as) && Bit (And bs) = and (as ++ bs)
+  Bit (And as) && b            = and (as ++ [b])
+  a            && Bit (And bs) = and (a : bs)
+  a            && b            = and [a,b]
+  Bit (Or as) || Bit (Or bs) = or (as ++ bs)
+  Bit (Or as) || b           = or (as ++ [b])
+  a           || Bit (Or bs) = or (a : bs)
+  a           || b           = or [a,b]
+  x ==> y = not x || y
+  not (Bit (Not c)) = c
+  not (Bit (Var b)) = Bit (Var (negateLit b))
+  not c        = Bit (Not c)
+  a `xor` b    = Bit (Xor a b)
+  and xs       = Bit (And xs)
+  or xs        = Bit (Or xs)
+  choose f t s = Bit (Mux f t s)
+
+instance Variable Bit where
+  exists = Bit . Var <$> exists
+  forall = Bit . Var <$> forall
+
+-- a Bit you don't assert is actually a boolean function that you can evaluate later after compilation
+instance Decoding Bit where
+  type Decoded Bit = Bool
+  decode sol b@(Bit c) 
+      = solutionStableName sol (unsafePerformIO (makeStableName' b))
+     -- The StableName didn’t have an associated literal with a solution,
+     -- recurse to compute the value.
+    <|> case c of
+          And cs  -> andMaybeBools $ decode sol <$> cs
+          Or cs   -> orMaybeBools  $ decode sol <$> cs
+          Xor x y -> xor <$> decode sol x <*> decode sol y
+          Mux cf ct cp -> do
+            p <- decode sol cp
+            decode sol $ if p then ct else cf
+          Not c'  -> not <$> decode sol c'
+          Var l   -> decode sol l
+    where
+      andMaybeBools :: [Maybe Bool] -> Maybe Bool
+      andMaybeBools mbs
+        | any not knowns = Just False  -- One is known to be false.
+        | null unknowns  = Just True   -- All are known to be true.
+        | otherwise      = Nothing     -- Unknown.
+        where
+          (unknowns, knowns) = partitionMaybes mbs
+
+      orMaybeBools :: [Maybe Bool] -> Maybe Bool
+      orMaybeBools mbs
+        | or knowns     = Just True   -- One is known to be true.
+        | null unknowns = Just False  -- All are known to be false.
+        | otherwise     = Nothing     -- Unknown.
+        where
+          (unknowns, knowns) = partitionMaybes mbs
+
+      partitionMaybes :: [Maybe a] -> ([()], [a])
+      partitionMaybes = foldr go ([],[])
+        where
+          go Nothing  ~(ns, js) = (():ns, js)
+          go (Just a) ~(ns, js) = (ns,    a:js)
+
+instance Encoding Bit where
+  type Encoded Bit = Bool
+  encode = bool
+
+-- | Assert claims that in any satisf given 'Bit' must be 'true' in any 
+-- satisfying interpretation of the current problem.
+assert :: MonadSAT m => Bit -> m ()
+assert b = do
+  l <- runBit b
+  assertFormula (formulaLiteral l)
+
+-- | Convert a 'Bit' to a 'Literal'.
+runBit :: MonadSAT m => Bit -> m Literal
+runBit (Bit (Not c)) = negateLiteral <$> runBit c
+runBit (Bit (Var (Lit l))) = return l
+runBit b@(Bit c) = generateLiteral b $ \out ->
+  assertFormula =<< case c of
+    And bs    -> formulaAnd out <$> traverse runBit bs
+    Or  bs    -> formulaOr  out <$> traverse runBit bs
+    Xor x y   -> formulaXor out <$> runBit x <*> runBit y
+    Mux x y p -> formulaMux out <$> runBit x <*> runBit y <*> runBit p
+    Var (Bool False) -> return $ formulaLiteral (negateLiteral out)
+    Var (Bool True)  -> return $ formulaLiteral out
+
+    -- Already handled above but GHC doesn't realize it.
+    Not _       -> error "Unreachable"
+    Var (Lit _) -> error "Unreachable"
+
+class GBoolean f where
+  gbool :: Bool -> f a
+  (&&#) :: f a -> f a -> f a
+  (||#) :: f a -> f a -> f a
+  (==>#) :: f a -> f a -> f a
+  gnot :: f a -> f a
+  gand :: [f a] -> f a
+  gor  :: [f a] -> f a
+  gxor :: f a -> f a -> f a
+
+instance GBoolean U1 where
+  gbool _    = U1
+  U1 &&# U1  = U1
+  U1 ||# U1  = U1
+  U1 ==># U1 = U1
+  gnot U1    = U1
+  gand _     = U1
+  gor  _     = U1
+  gxor _ _   = U1
+
+instance (GBoolean f, GBoolean g) => GBoolean (f :*: g) where
+  gbool x = gbool x :*: gbool x
+  (a :*: b) &&#  (c :*: d) = (a &&# c)  :*: (b &&# d)
+  (a :*: b) ||#  (c :*: d) = (a ||# c)  :*: (b ||# d)
+  (a :*: b) ==># (c :*: d) = (a ==># c) :*: (b ==># d)
+  gnot (a :*: b) = gnot a :*: gnot b
+  gand xs = gand (map (\(x :*: _) -> x) xs) :*: gand (map (\(_ :*: x) -> x) xs)
+  gor xs = gor (map (\(x :*: _) -> x) xs) :*: gor (map (\(_ :*: x) -> x) xs)
+  gxor (a :*: b) (c :*: d) = gxor a c :*: gxor b d
+
+instance Boolean a => GBoolean (K1 i a) where
+  gbool = K1 . bool
+  K1 a &&# K1 b = K1 (a && b)
+  K1 a ||# K1 b = K1 (a || b)
+  K1 a ==># K1 b = K1 (a ==> b)
+  gnot (K1 a) = K1 (not a)
+  gand as = K1 (and (map (\(K1 a) -> a) as))
+  gor as = K1 (or (map (\(K1 a) -> a) as))
+  gxor (K1 a) (K1 b) = K1 (xor a b)
+
+instance GBoolean a => GBoolean (M1 i c a) where
+  gbool = M1 . gbool
+  M1 a &&# M1 b = M1 (a &&# b)
+  M1 a ||# M1 b = M1 (a ||# b)
+  M1 a ==># M1 b = M1 (a ==># b)
+  gnot (M1 a) = M1 (gnot a)
+  gand as = M1 (gand (map (\(M1 a) -> a) as))
+  gor as = M1 (gor (map (\(M1 a) -> a) as))
+  gxor (M1 a) (M1 b) = M1 (gxor a b)
+
+-- | The normal 'Bool' operators in Haskell are not overloaded. This
+-- provides a richer set that are.
+--
+-- Instances for this class for product-like types can be automatically derived
+-- for any type that is an instance of @Generic@
+class Boolean t where
+  -- | Lift a 'Bool'
+  bool :: Bool -> t
+  default bool :: (Generic t, GBoolean (Rep t)) => Bool -> t
+  bool = to . gbool
+  -- |
+  -- @'true' = 'bool' 'True'@
+  true :: t
+  true = bool True
+  -- |
+  -- @'false' = 'bool' 'False'@
+  false :: t
+  false = bool False
+
+  -- | Logical conjunction.
+  (&&) :: t -> t -> t
+  default (&&) :: (Generic t, GBoolean (Rep t)) => t -> t -> t
+  x && y = to (from x &&# from y)
+
+  -- | Logical disjunction (inclusive or).
+  (||) :: t -> t -> t
+  default (||) :: (Generic t, GBoolean (Rep t)) => t -> t -> t
+  x || y = to (from x ||# from y)
+
+  -- | Logical implication.
+  (==>) :: t -> t -> t
+  default (==>) :: (Generic t, GBoolean (Rep t)) => t -> t -> t
+  x ==> y = to (from x ==># from y)
+
+  -- | Logical negation
+  not :: t -> t
+  default not :: (Generic t, GBoolean (Rep t)) => t -> t
+  not = to . gnot . from
+
+  -- | The logical conjunction of several values.
+  and :: [t] -> t
+  default and :: (Generic t, GBoolean (Rep t)) => [t] -> t
+  and = to . gand . map from
+
+  -- | The logical disjunction of several values.
+  or :: [t] -> t
+  default or :: (Generic t, GBoolean (Rep t)) => [t] -> t
+  or = to . gor . map from
+
+  -- | The negated logical conjunction of several values.
+  --
+  -- @'nand' = 'not' . 'and'@
+  nand :: [t] -> t
+  nand = not . and
+
+  -- | The negated logical disjunction of several values.
+  --
+  -- @'nor' = 'not' . 'or'@
+  nor :: [t] -> t
+  nor = not . or
+
+  -- | Exclusive-or
+  xor :: t -> t -> t
+  default xor :: (Generic t, GBoolean (Rep t)) => t -> t -> t
+  xor x y = to (from x `gxor` from y)
+
+  -- | Choose between two alternatives based on a selector bit.
+  choose :: t  -- ^ False branch
+         -> t  -- ^ True branch
+         -> t  -- ^ Predicate/selector branch
+         -> t
+  choose f t s = (f && not s) || (t && s)
+
+instance Boolean Bool where
+  bool = id
+  true = True
+  false = False
+
+  (&&) = (Prelude.&&)
+  (||) = (Prelude.||)
+  x ==> y = not x || y
+
+  not = Prelude.not
+
+  and = Prelude.and
+  or = Prelude.or
+
+  False `xor` False = False
+  False `xor` True  = True
+  True `xor` False  = True
+  True `xor` True   = False
+
+  choose f _ False = f
+  choose _ t True  = t
diff --git a/src/Ersatz/Bits.hs b/src/Ersatz/Bits.hs
new file mode 100644
--- /dev/null
+++ b/src/Ersatz/Bits.hs
@@ -0,0 +1,169 @@
+{-# LANGUAGE TypeFamilies, DeriveDataTypeable, DeriveGeneric #-}
+--------------------------------------------------------------------
+-- |
+-- Copyright :  (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013
+-- License   :  BSD3
+-- Maintainer:  Edward Kmett <ekmett@gmail.com>
+-- Stability :  experimental
+-- Portability: non-portable
+--
+--------------------------------------------------------------------
+module Ersatz.Bits
+  ( Bit1(..), Bit2(..), Bit3(..), Bit4(..), Bit5(..), Bit6(..), Bit7(..), Bit8(..)
+  ) where
+
+import Prelude hiding ((&&), (||), and, or, not)
+
+import Control.Applicative
+import Data.Bits (Bits, (.&.), (.|.), shiftL, shiftR)
+import Data.List (foldl')
+import Data.Typeable
+import Data.Word (Word8)
+import Ersatz.Bit
+import Ersatz.Decoding
+import Ersatz.Equatable
+import Ersatz.Encoding
+import Ersatz.Variable
+import GHC.Generics
+
+newtype Bit1 = Bit1 Bit deriving (Show,Typeable,Generic)
+data Bit2 = Bit2 Bit Bit deriving (Show,Typeable,Generic)
+data Bit3 = Bit3 Bit Bit Bit deriving (Show,Typeable,Generic)
+data Bit4 = Bit4 Bit Bit Bit Bit deriving (Show,Typeable,Generic)
+data Bit5 = Bit5 Bit Bit Bit Bit Bit deriving (Show,Typeable,Generic)
+data Bit6 = Bit6 Bit Bit Bit Bit Bit Bit deriving (Show,Typeable,Generic)
+data Bit7 = Bit7 Bit Bit Bit Bit Bit Bit Bit deriving (Show,Typeable,Generic)
+data Bit8 = Bit8 Bit Bit Bit Bit Bit Bit Bit Bit deriving (Show,Typeable,Generic)
+
+instance Boolean Bit1
+instance Boolean Bit2
+instance Boolean Bit3
+instance Boolean Bit4
+instance Boolean Bit5
+instance Boolean Bit6
+instance Boolean Bit7
+instance Boolean Bit8
+
+instance Equatable Bit1
+instance Equatable Bit2
+instance Equatable Bit3
+instance Equatable Bit4
+instance Equatable Bit5
+instance Equatable Bit6
+instance Equatable Bit7
+instance Equatable Bit8
+
+instance Variable Bit1
+instance Variable Bit2
+instance Variable Bit3
+instance Variable Bit4
+instance Variable Bit5
+instance Variable Bit6
+instance Variable Bit7
+instance Variable Bit8
+
+instance Decoding Bit1 where
+  type Decoded Bit1 = Word8
+  decode s (Bit1 a) = boolsToNum1 <$> decode s a
+
+instance Decoding Bit2 where
+  type Decoded Bit2 = Word8
+  decode s (Bit2 a b) = boolsToNum2 <$> decode s a <*> decode s b
+
+instance Decoding Bit3 where
+  type Decoded Bit3 = Word8
+  decode s (Bit3 a b c) = boolsToNum3 <$> decode s a <*> decode s b <*> decode s c
+
+instance Decoding Bit4 where
+  type Decoded Bit4 = Word8
+  decode s (Bit4 a b c d) = boolsToNum4 <$> decode s a <*> decode s b <*> decode s c <*> decode s d
+
+instance Decoding Bit5 where
+  type Decoded Bit5 = Word8
+  decode s (Bit5 a b c d e) = boolsToNum5 <$> decode s a <*> decode s b <*> decode s c <*> decode s d <*> decode s e
+
+instance Decoding Bit6 where
+  type Decoded Bit6 = Word8
+  decode s (Bit6 a b c d e f) = boolsToNum6 <$> decode s a <*> decode s b <*> decode s c <*> decode s d <*> decode s e <*> decode s f
+
+instance Decoding Bit7 where
+  type Decoded Bit7 = Word8
+  decode s (Bit7 a b c d e f g) = boolsToNum7 <$> decode s a <*> decode s b <*> decode s c <*> decode s d <*> decode s e <*> decode s f <*> decode s g
+
+instance Decoding Bit8 where
+  type Decoded Bit8 = Word8
+  decode s (Bit8 a b c d e f g h) = boolsToNum8 <$> decode s a <*> decode s b <*> decode s c <*> decode s d <*> decode s e <*> decode s f <*> decode s g <*> decode s h
+
+instance Encoding Bit1 where
+  type Encoded Bit1 = Word8
+  encode i = Bit1 a where (a:_) = bitsOf i
+
+instance Encoding Bit2 where
+  type Encoded Bit2 = Word8
+  encode i = Bit2 a b where (b:a:_) = bitsOf i
+
+instance Encoding Bit3 where
+  type Encoded Bit3 = Word8
+  encode i = Bit3 a b c where (c:b:a:_) = bitsOf i
+
+instance Encoding Bit4 where
+  type Encoded Bit4 = Word8
+  encode i = Bit4 a b c d where (d:c:b:a:_) = bitsOf i
+
+instance Encoding Bit5 where
+  type Encoded Bit5 = Word8
+  encode i = Bit5 a b c d e where (e:d:c:b:a:_) = bitsOf i
+
+instance Encoding Bit6 where
+  type Encoded Bit6 = Word8
+  encode i = Bit6 a b c d e f where (f:e:d:c:b:a:_) = bitsOf i
+
+instance Encoding Bit7 where
+  type Encoded Bit7 = Word8
+  encode i = Bit7 a b c d e f g where (g:f:e:d:c:b:a:_) = bitsOf i
+
+instance Encoding Bit8 where
+  type Encoded Bit8 = Word8
+  encode i = Bit8 a b c d e f g h where (h:g:f:e:d:c:b:a:_) = bitsOf i
+
+boolsToNum1 :: Bool -> Word8
+boolsToNum1 a = boolToNum a
+
+boolsToNum2 :: Bool -> Bool -> Word8
+boolsToNum2 a b = boolsToNum [a,b]
+
+boolsToNum3 :: Bool -> Bool -> Bool -> Word8
+boolsToNum3 a b c = boolsToNum [a,b,c]
+
+boolsToNum4 :: Bool -> Bool -> Bool -> Bool -> Word8
+boolsToNum4 a b c d = boolsToNum [a,b,c,d]
+
+boolsToNum5 :: Bool -> Bool -> Bool -> Bool -> Bool -> Word8
+boolsToNum5 a b c d e = boolsToNum [a,b,c,d,e]
+
+boolsToNum6 :: Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Word8
+boolsToNum6 a b c d e f = boolsToNum [a,b,c,d,e,f]
+
+boolsToNum7 :: Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Word8
+boolsToNum7 a b c d e f g = boolsToNum [a,b,c,d,e,f,g]
+
+boolsToNum8 :: Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Bool -> Word8
+boolsToNum8 a b c d e f g h = boolsToNum [a,b,c,d,e,f,g,h]
+
+bitsOf :: (Num a, Bits a) => a -> [Bit]
+bitsOf n = bool (numToBool (n .&. 1)) : bitsOf (n `shiftR` 1)
+{-# INLINE bitsOf #-}
+
+numToBool :: (Eq a, Num a) => a -> Bool
+numToBool 0 = False
+numToBool _ = True
+{-# INLINE numToBool #-}
+
+boolsToNum :: (Num a, Bits a) => [Bool] -> a
+boolsToNum = foldl' (\n a -> (n `shiftL` 1) .|. boolToNum a) 0
+{-# INLINE boolsToNum #-}
+
+boolToNum :: Num a => Bool -> a
+boolToNum False = 0
+boolToNum True  = 1
+{-# INLINE boolToNum #-}
diff --git a/src/Ersatz/Decoding.hs b/src/Ersatz/Decoding.hs
new file mode 100644
--- /dev/null
+++ b/src/Ersatz/Decoding.hs
@@ -0,0 +1,107 @@
+{-# LANGUAGE TypeFamilies, Rank2Types #-}
+--------------------------------------------------------------------
+-- |
+-- Copyright :  (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013
+-- License   :  BSD3
+-- Maintainer:  Edward Kmett <ekmett@gmail.com>
+-- Stability :  experimental
+-- Portability: non-portable
+--
+--------------------------------------------------------------------
+module Ersatz.Decoding
+  ( Decoding(..)
+  ) where
+
+import Control.Applicative
+import Data.Array
+import Data.HashMap.Lazy (HashMap)
+import Data.IntMap (IntMap)
+import Data.Map (Map)
+import Data.Sequence (Seq)
+import Data.Traversable
+import Data.Tree (Tree)
+import Ersatz.Internal.Literal
+import Ersatz.Solution
+
+class Decoding a where
+  type Decoded a :: *
+  -- | Return a value based on the solution if one can be determined.
+  decode :: Solution -> a -> Maybe (Decoded a)
+
+instance Decoding Literal where
+  type Decoded Literal = Bool
+  decode s l = solutionLiteral s l
+
+instance Decoding Lit where
+  type Decoded Lit = Bool
+  decode _ (Bool b) = Just b
+  decode s (Lit l)  = decode s l
+
+instance Decoding () where
+  type Decoded () = ()
+  decode _ () = Just ()
+
+instance (Decoding a, Decoding b) => Decoding (a,b) where
+  type Decoded (a,b) = (Decoded a, Decoded b)
+  decode s (a,b) = (,) <$> decode s a <*> decode s b
+
+instance (Decoding a, Decoding b, Decoding c) => Decoding (a,b,c) where
+  type Decoded (a,b,c) = (Decoded a, Decoded b, Decoded c)
+  decode s (a,b,c) = (,,) <$> decode s a <*> decode s b <*> decode s c
+
+instance (Decoding a, Decoding b, Decoding c, Decoding d) => Decoding (a,b,c,d) where
+  type Decoded (a,b,c,d) = (Decoded a, Decoded b, Decoded c, Decoded d)
+  decode s (a,b,c,d) = (,,,) <$> decode s a <*> decode s b <*> decode s c <*> decode s d
+
+instance (Decoding a, Decoding b, Decoding c, Decoding d, Decoding e) => Decoding (a,b,c,d,e) where
+  type Decoded (a,b,c,d,e) = (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e)
+  decode s (a,b,c,d,e) = (,,,,) <$> decode s a <*> decode s b <*> decode s c <*> decode s d <*> decode s e
+
+instance (Decoding a, Decoding b, Decoding c, Decoding d, Decoding e, Decoding f) => Decoding (a,b,c,d,e,f) where
+  type Decoded (a,b,c,d,e,f) = (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e, Decoded f)
+  decode s (a,b,c,d,e,f) = (,,,,,) <$> decode s a <*> decode s b <*> decode s c <*> decode s d <*> decode s e <*> decode s f
+
+instance (Decoding a, Decoding b, Decoding c, Decoding d, Decoding e, Decoding f, Decoding g) => Decoding (a,b,c,d,e,f,g) where
+  type Decoded (a,b,c,d,e,f,g) = (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e, Decoded f, Decoded g)
+  decode s (a,b,c,d,e,f,g) = (,,,,,,) <$> decode s a <*> decode s b <*> decode s c <*> decode s d <*> decode s e <*> decode s f <*> decode s g
+
+instance (Decoding a, Decoding b, Decoding c, Decoding d, Decoding e, Decoding f, Decoding g, Decoding h) => Decoding (a,b,c,d,e,f,g,h) where
+  type Decoded (a,b,c,d,e,f,g,h) = (Decoded a, Decoded b, Decoded c, Decoded d, Decoded e, Decoded f, Decoded g, Decoded h)
+  decode s (a,b,c,d,e,f,g,h) = (,,,,,,,) <$> decode s a <*> decode s b <*> decode s c <*> decode s d <*> decode s e <*> decode s f <*> decode s g <*> decode s h
+
+instance Decoding a => Decoding [a] where
+  type Decoded [a] = [Decoded a]
+  decode = traverse . decode
+
+instance (Ix i, Decoding e) => Decoding (Array i e) where
+  type Decoded (Array i e) = Array i (Decoded e)
+  decode = traverse . decode
+
+instance (Decoding a, Decoding b) => Decoding (Either a b) where
+  type Decoded (Either a b) = Either (Decoded a) (Decoded b)
+  decode s (Left  a) = Left  <$> decode s a
+  decode s (Right b) = Right <$> decode s b
+
+instance Decoding a => Decoding (HashMap k a) where
+  type Decoded (HashMap k a) = HashMap k (Decoded a)
+  decode = traverse . decode
+
+instance Decoding a => Decoding (IntMap a) where
+  type Decoded (IntMap a) = IntMap (Decoded a)
+  decode = traverse . decode
+
+instance Decoding a => Decoding (Map k a) where
+  type Decoded (Map k a) = Map k (Decoded a)
+  decode = traverse . decode
+
+instance Decoding a => Decoding (Maybe a) where
+  type Decoded (Maybe a) = Maybe (Decoded a)
+  decode = traverse . decode
+
+instance Decoding a => Decoding (Seq a) where
+  type Decoded (Seq a) = Seq (Decoded a)
+  decode = traverse . decode
+
+instance Decoding a => Decoding (Tree a) where
+  type Decoded (Tree a) = Tree (Decoded a)
+  decode = traverse . decode
diff --git a/src/Ersatz/Encoding.hs b/src/Ersatz/Encoding.hs
new file mode 100644
--- /dev/null
+++ b/src/Ersatz/Encoding.hs
@@ -0,0 +1,98 @@
+{-# LANGUAGE TypeFamilies, Rank2Types #-}
+--------------------------------------------------------------------
+-- |
+-- Copyright :  (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013
+-- License   :  BSD3
+-- Maintainer:  Edward Kmett <ekmett@gmail.com>
+-- Stability :  experimental
+-- Portability: non-portable
+--
+--------------------------------------------------------------------
+module Ersatz.Encoding
+  ( Encoding(..)
+  ) where
+
+import Data.Array
+import Data.HashMap.Lazy (HashMap)
+import Data.IntMap (IntMap)
+import Data.Map (Map)
+import Data.Sequence (Seq)
+import Data.Tree (Tree)
+import Ersatz.Internal.Literal
+
+class Encoding a where
+  type Encoded a :: *
+  encode :: Encoded a -> a
+
+instance Encoding Lit where
+  type Encoded Lit = Bool
+  encode = Bool
+
+instance Encoding () where
+  type Encoded () = ()
+  encode () = ()
+
+instance (Encoding a, Encoding b) => Encoding (a,b) where
+  type Encoded (a,b) = (Encoded a, Encoded b)
+  encode (a,b) = (encode a, encode b)
+
+instance (Encoding a, Encoding b, Encoding c) => Encoding (a,b,c) where
+  type Encoded (a,b,c) = (Encoded a, Encoded b, Encoded c)
+  encode (a,b,c) = (encode a, encode b, encode c)
+
+instance (Encoding a, Encoding b, Encoding c, Encoding d) => Encoding (a,b,c,d) where
+  type Encoded (a,b,c,d) = (Encoded a, Encoded b, Encoded c, Encoded d)
+  encode (a,b,c,d) = (encode a, encode b, encode c, encode d)
+
+instance (Encoding a, Encoding b, Encoding c, Encoding d, Encoding e) => Encoding (a,b,c,d,e) where
+  type Encoded (a,b,c,d,e) = (Encoded a, Encoded b, Encoded c, Encoded d, Encoded e)
+  encode (a,b,c,d,e) = (encode a, encode b, encode c, encode d, encode e)
+
+instance (Encoding a, Encoding b, Encoding c, Encoding d, Encoding e, Encoding f) => Encoding (a,b,c,d,e,f) where
+  type Encoded (a,b,c,d,e,f) = (Encoded a, Encoded b, Encoded c, Encoded d, Encoded e, Encoded f)
+  encode (a,b,c,d,e,f) = (encode a, encode b, encode c, encode d, encode e, encode f)
+
+instance (Encoding a, Encoding b, Encoding c, Encoding d, Encoding e, Encoding f, Encoding g) => Encoding (a,b,c,d,e,f,g) where
+  type Encoded (a,b,c,d,e,f,g) = (Encoded a, Encoded b, Encoded c, Encoded d, Encoded e, Encoded f, Encoded g)
+  encode (a,b,c,d,e,f,g) = (encode a, encode b, encode c, encode d, encode e, encode f, encode g)
+
+instance (Encoding a, Encoding b, Encoding c, Encoding d, Encoding e, Encoding f, Encoding g, Encoding h) => Encoding (a,b,c,d,e,f,g,h) where
+  type Encoded (a,b,c,d,e,f,g,h) = (Encoded a, Encoded b, Encoded c, Encoded d, Encoded e, Encoded f, Encoded g, Encoded h)
+  encode (a,b,c,d,e,f,g,h) = (encode a, encode b, encode c, encode d, encode e, encode f, encode g, encode h)
+
+instance Encoding a => Encoding [a] where
+  type Encoded [a] = [Encoded a]
+  encode = fmap encode
+
+instance (Ix i, Encoding e) => Encoding (Array i e) where
+  type Encoded (Array i e) = Array i (Encoded e)
+  encode = fmap encode
+
+instance (Encoding a, Encoding b) => Encoding (Either a b) where
+  type Encoded (Either a b) = Either (Encoded a) (Encoded b)
+  encode (Left  a) = Left  (encode a)
+  encode (Right b) = Right (encode b)
+
+instance Encoding a => Encoding (HashMap k a) where
+  type Encoded (HashMap k a) = HashMap k (Encoded a)
+  encode = fmap encode
+
+instance Encoding a => Encoding (IntMap a) where
+  type Encoded (IntMap a) = IntMap (Encoded a)
+  encode = fmap encode
+
+instance Encoding a => Encoding (Map k a) where
+  type Encoded (Map k a) = Map k (Encoded a)
+  encode = fmap encode
+
+instance Encoding a => Encoding (Maybe a) where
+  type Encoded (Maybe a) = Maybe (Encoded a)
+  encode = fmap encode
+
+instance Encoding a => Encoding (Seq a) where
+  type Encoded (Seq a) = Seq (Encoded a)
+  encode = fmap encode
+
+instance Encoding a => Encoding (Tree a) where
+  type Encoded (Tree a) = Tree (Encoded a)
+  encode = fmap encode
diff --git a/src/Ersatz/Equatable.hs b/src/Ersatz/Equatable.hs
new file mode 100644
--- /dev/null
+++ b/src/Ersatz/Equatable.hs
@@ -0,0 +1,68 @@
+{-# LANGUAGE TypeFamilies, TypeOperators, FlexibleInstances, DeriveDataTypeable, DeriveGeneric, DefaultSignatures, FlexibleContexts, UndecidableInstances #-}
+{-# OPTIONS_HADDOCK not-home #-}
+--------------------------------------------------------------------
+-- |
+-- Copyright :  (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013
+-- License   :  BSD3
+-- Maintainer:  Edward Kmett <ekmett@gmail.com>
+-- Stability :  experimental
+-- Portability: non-portable
+--
+--------------------------------------------------------------------
+module Ersatz.Equatable
+  ( Equatable(..)
+  ) where
+
+import Prelude hiding ((&&),(||),not,and,or)
+import qualified Prelude
+
+import Ersatz.Bit
+import GHC.Generics
+
+infix  4 ===, /==
+
+-- | Instances for this class for arbitrary types can be automatically derived from @Generic@.
+class Equatable t where
+  -- | Compare for equality within the SAT problem.
+  (===) :: t -> t -> Bit
+  default (===) :: (Generic t, GEquatable (Rep t)) => t -> t -> Bit
+  a === b = from a ===# from b
+
+  -- | Compare for inequality within the SAT problem.
+  (/==) :: t -> t -> Bit
+
+  a /== b = not (a === b)
+
+instance Equatable Bit where
+  a === b = not (xor a b)
+  (/==) = xor
+
+instance (Equatable a, Equatable b) => Equatable (a,b)
+instance (Equatable a, Equatable b, Equatable c) => Equatable (a,b,c)
+instance (Equatable a, Equatable b, Equatable c, Equatable d) => Equatable (a,b,c,d)
+instance (Equatable a, Equatable b, Equatable c, Equatable d, Equatable e) => Equatable (a,b,c,d,e)
+instance (Equatable a, Equatable b, Equatable c, Equatable d, Equatable e, Equatable f) => Equatable (a,b,c,d,e,f)
+instance (Equatable a, Equatable b, Equatable c, Equatable d, Equatable e, Equatable f, Equatable g) => Equatable (a,b,c,d,e,f,g)
+instance Equatable a => Equatable (Maybe a)
+instance Equatable a => Equatable [a]
+instance (Equatable a, Equatable b) => Equatable (Either a b)
+
+class GEquatable f where
+  (===#) :: f a -> f a -> Bit
+
+instance GEquatable U1 where
+  U1 ===# U1 = true
+
+instance (GEquatable f, GEquatable g) => GEquatable (f :*: g) where
+  (a :*: b) ===# (c :*: d) = (a ===# c) && (b ===# d)
+
+instance (GEquatable f, GEquatable g) => GEquatable (f :+: g) where
+  L1 a ===# L1 b = a ===# b
+  R1 a ===# R1 b = a ===# b
+  _ ===# _ = false
+
+instance GEquatable f => GEquatable (M1 i c f) where
+  M1 x ===# M1 y = x ===# y
+
+instance Equatable a => GEquatable (K1 i a) where
+  K1 a ===# K1 b = a === b
diff --git a/src/Ersatz/Internal/Circuit.hs b/src/Ersatz/Internal/Circuit.hs
new file mode 100644
--- /dev/null
+++ b/src/Ersatz/Internal/Circuit.hs
@@ -0,0 +1,55 @@
+{-# LANGUAGE DeriveDataTypeable #-}
+--------------------------------------------------------------------
+-- |
+-- Copyright :  (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013
+-- License   :  BSD3
+-- Maintainer:  Edward Kmett <ekmett@gmail.com>
+-- Stability :  experimental
+-- Portability: non-portable
+--
+--------------------------------------------------------------------
+module Ersatz.Internal.Circuit
+  ( Circuit(..)
+  ) where
+
+import Control.Applicative
+import Data.Foldable (Foldable, foldMap)
+import Data.Monoid
+import Data.Traversable (Traversable, traverse)
+import Data.Typeable
+import Ersatz.Internal.Literal
+
+-- | This is used to observe the directed graph with sharing of how multiple
+-- 'Ersatz.Bit.Bit' values are related.
+data Circuit c
+  = And [c]
+  | Or [c]
+  | Xor c c
+  | Mux c c c  -- ^ False branch, true branch, predicate/selector branch
+  | Not c
+  | Var !Lit
+  deriving (Show, Typeable)
+
+instance Functor Circuit where
+  fmap f (And as) = And (map f as)
+  fmap f (Or as) = Or (map f as)
+  fmap f (Xor a b) = Xor (f a) (f b)
+  fmap f (Mux a b c) = Mux (f a) (f b) (f c)
+  fmap f (Not a) = Not (f a)
+  fmap _ (Var l) = Var l
+
+instance Foldable Circuit where
+  foldMap f (And as) = foldMap f as
+  foldMap f (Or as) = foldMap f as
+  foldMap f (Xor a b) = f a <> f b
+  foldMap f (Mux a b c) = f a <> f b <> f c
+  foldMap f (Not a) = f a
+  foldMap _ Var{} = mempty
+
+instance Traversable Circuit where
+  traverse f (And as) = And <$> traverse f as
+  traverse f (Or as) = Or <$> traverse f as
+  traverse f (Xor a b) = Xor <$> f a <*> f b
+  traverse f (Mux a b c) = Mux <$> f a <*> f b <*> f c
+  traverse f (Not a) = Not <$> f a
+  traverse _ (Var l) = pure (Var l)
diff --git a/src/Ersatz/Internal/Formula.hs b/src/Ersatz/Internal/Formula.hs
new file mode 100644
--- /dev/null
+++ b/src/Ersatz/Internal/Formula.hs
@@ -0,0 +1,213 @@
+{-# LANGUAGE Rank2Types, GeneralizedNewtypeDeriving, TypeOperators, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, PatternGuards, DeriveDataTypeable, DefaultSignatures, TypeFamilies, BangPatterns #-}
+{-# OPTIONS_HADDOCK not-home #-}
+--------------------------------------------------------------------
+-- |
+-- Copyright :  (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013
+-- License   :  BSD3
+-- Maintainer:  Edward Kmett <ekmett@gmail.com>
+-- Stability :  experimental
+-- Portability: non-portable
+--
+--------------------------------------------------------------------
+module Ersatz.Internal.Formula
+  (
+  -- * Clauses
+    Clause(..), clauseLiterals
+  -- * Formulas
+  , Formula(..)
+  , formulaEmpty, formulaLiteral
+  , formulaNot, formulaAnd, formulaOr, formulaXor, formulaMux
+  ) where
+
+import Control.Applicative
+import Data.IntSet (IntSet)
+import qualified Data.IntSet as IntSet
+import qualified Data.List as List (intersperse)
+import Data.Monoid
+import Data.Set (Set)
+import qualified Data.Set as Set
+import Data.Typeable
+import Ersatz.Internal.Literal
+
+------------------------------------------------------------------------------
+-- Clauses
+------------------------------------------------------------------------------
+
+-- | A disjunction of possibly negated atoms. Negated atoms are represented
+-- by negating the identifier.
+newtype Clause = Clause { clauseSet :: IntSet }
+  deriving (Eq, Ord, Monoid, Typeable)
+
+-- | Extract the (possibly negated) atoms referenced by a 'Clause'.
+clauseLiterals :: Clause -> [Literal]
+clauseLiterals (Clause is) = Literal <$> IntSet.toList is
+
+------------------------------------------------------------------------------
+-- Formulas
+------------------------------------------------------------------------------
+
+-- | A conjunction of clauses
+newtype Formula = Formula { formulaSet :: Set Clause }
+  deriving (Eq, Ord, Monoid, Typeable)
+
+instance Show Formula where
+  showsPrec p = showParen (p > 2) . foldr (.) id
+              . List.intersperse (showString " & ") . map (showsPrec 3)
+              . Set.toList . formulaSet
+
+instance Show Clause where
+  showsPrec p = showParen (p > 1) . foldr (.) id
+              . List.intersperse (showString " | ") . map (showsPrec 2)
+              . IntSet.toList . clauseSet
+
+
+-- | A formula with no clauses
+formulaEmpty :: Formula
+formulaEmpty = Formula Set.empty
+
+-- | Assert a literal
+formulaLiteral :: Literal -> Formula
+formulaLiteral (Literal l) =
+  Formula (Set.singleton (Clause (IntSet.singleton l)))
+
+-- | The boolean /not/ operation
+--
+-- @
+-- O ≡ ¬A
+-- (O → ¬A) & (¬O → A)
+-- (¬O | ¬A) & (O | A)
+-- @
+formulaNot :: Literal  -- ^ Output
+           -> Literal  -- ^ Input
+           -> Formula
+formulaNot (Literal out) (Literal inp) = formulaFromList cls
+  where
+    cls = [ [-out, -inp], [out, inp] ]
+
+-- | The boolean /and/ operation
+--
+-- @
+-- O ≡ (A & B & C)
+-- (O → (A & B & C)) & (¬O → ¬(A & B & C))
+-- (¬O | (A & B & C)) & (O | ¬(A & B & C))
+-- (¬O | A) & (¬O | B) & (¬O | C) & (O | ¬A | ¬B | ¬C)
+-- @
+formulaAnd :: Literal    -- ^ Output
+           -> [Literal]  -- ^ Inputs
+           -> Formula
+formulaAnd (Literal out) inpLs = formulaFromList cls
+  where
+    cls = (out : map negate inps) : map (\inp -> [-out, inp]) inps
+    inps = map literalId inpLs
+
+-- | The boolean /or/ operation
+--
+-- @
+-- O ≡ (A | B | C)
+-- (O → (A | B | C)) & (¬O → ¬(A | B | C))
+-- (¬O | (A | B | C)) & (O | ¬(A | B | C))
+-- (¬O | A | B | C) & (O | (¬A & ¬B & ¬C))
+-- (¬O | A | B | C) & (O | ¬A) & (O | ¬B) & (O | ¬C)
+-- @
+formulaOr :: Literal    -- ^ Output
+          -> [Literal]  -- ^ Inputs
+          -> Formula
+formulaOr (Literal out) inpLs = formulaFromList cls
+  where
+    cls = (-out : inps)
+        : map (\inp -> [out, -inp]) inps
+    inps = map literalId inpLs
+
+-- | The boolean /xor/ operation
+--
+-- @
+-- O ≡ A ⊕ B
+-- O ≡ ((¬A & B) | (A & ¬B))
+-- (O → ((¬A & B) | (A & ¬B))) & (¬O → ¬((¬A & B) | (A & ¬B)))
+-- @
+--
+-- Left hand side:
+-- @
+-- O → ((¬A & B) | (A & ¬B))
+-- ¬O | ((¬A & B) | (A & ¬B))
+-- ¬O | ((¬A | A) & (¬A | ¬B) & (A | B) & (¬B | B))
+-- ¬O | ((¬A | ¬B) & (A | B))
+-- (¬O | ¬A | ¬B) & (¬O | A | B)
+-- @
+--
+-- Right hand side:
+--
+-- @
+-- ¬O → ¬((¬A & B) | (A & ¬B))
+-- O | ¬((¬A & B) | (A & ¬B))
+-- O | (¬(¬A & B) & ¬(A & ¬B))
+-- O | ((A | ¬B) & (¬A | B))
+-- (O | ¬A | B) & (O | A | ¬B)
+-- @
+--
+-- Result:
+--
+-- @
+-- (¬O | ¬A | ¬B) & (¬O | A | B) & (O | ¬A | B) & (O | A | ¬B)
+-- @
+formulaXor :: Literal  -- ^ Output
+           -> Literal  -- ^ Input
+           -> Literal  -- ^ Input
+           -> Formula
+formulaXor (Literal out) (Literal inpA) (Literal inpB) = formulaFromList cls
+  where
+    cls = [ [-out, -inpA, -inpB]
+          , [-out,  inpA,  inpB]
+          , [ out, -inpA,  inpB]
+          , [ out,  inpA, -inpB]
+          ]
+
+-- | The boolean /else-then-if/ or /mux/ operation
+--
+-- @
+-- O ≡ (F & ¬P) | (T & P)
+-- (O → ((F & ¬P) | (T & P))) & (¬O → ¬((F & ¬P) | (T & P)))
+-- @
+--
+-- Left hand side:
+--
+-- @
+-- O → ((F & ¬P) | (T & P))
+-- ¬O | ((F & ¬P) | (T & P))
+-- ¬O | ((F | T) & (F | P) & (T | ¬P) & (¬P | P))
+-- ¬O | ((F | T) & (F | P) & (T | ¬P))
+-- (¬O | F | T) & (¬O | F | P) & (¬O | T | ¬P)
+-- @
+--
+-- Right hand side:
+--
+-- @
+-- ¬O → ¬((F & ¬P) | (T & P))
+-- O | ¬((F & ¬P) | (T & P))
+-- O | (¬(F & ¬P) & ¬(T & P))
+-- O | ((¬F | P) & (¬T | ¬P))
+-- (O | ¬F | P) & (O | ¬T | ¬P)
+-- @
+--
+-- Result:
+--
+-- @
+-- (¬O | F | T) & (¬O | F | P) & (¬O | T | ¬P) & (O | ¬F | P) & (O | ¬T | ¬P)
+-- @
+formulaMux :: Literal  -- ^ Output
+           -> Literal  -- ^ False branch
+           -> Literal  -- ^ True branch
+           -> Literal  -- ^ Predicate/selector
+           -> Formula
+formulaMux (Literal out) (Literal inpF) (Literal inpT) (Literal inpP) =
+  formulaFromList cls
+  where
+    cls = [ [-out,  inpF,  inpT]
+          , [-out,  inpF,  inpP]
+          , [-out,  inpT, -inpP]
+          , [ out, -inpF,  inpP]
+          , [ out, -inpT, -inpP]
+          ]
+
+formulaFromList :: [[Int]] -> Formula
+formulaFromList = Formula . Set.fromList . map (Clause . IntSet.fromList)
diff --git a/src/Ersatz/Internal/Literal.hs b/src/Ersatz/Internal/Literal.hs
new file mode 100644
--- /dev/null
+++ b/src/Ersatz/Internal/Literal.hs
@@ -0,0 +1,44 @@
+{-# LANGUAGE DeriveDataTypeable #-}
+--------------------------------------------------------------------
+-- |
+-- Copyright :  (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013
+-- License   :  BSD3
+-- Maintainer:  Edward Kmett <ekmett@gmail.com>
+-- Stability :  experimental
+-- Portability: non-portable
+--
+--------------------------------------------------------------------
+module Ersatz.Internal.Literal
+  ( Literal(..)
+  , negateLiteral
+  , Lit(..)
+  , lit
+  , negateLit
+  ) where
+
+import Data.Typeable
+
+-- | A naked possibly-negated Atom, present in the target 'Ersatz.Solver.Solver'.
+newtype Literal = Literal { literalId :: Int } deriving (Eq,Ord,Typeable)
+
+instance Show Literal where
+  showsPrec i = showsPrec i . literalId
+  show = show . literalId
+  showList = showList . map literalId
+
+negateLiteral :: Literal -> Literal
+negateLiteral = Literal . negate . literalId
+
+-- | Literals with partial evaluation
+data Lit
+  = Lit  {-# UNPACK #-} !Literal
+  | Bool !Bool
+  deriving (Show, Typeable)
+
+-- | Lift a 'Bool' to a 'Lit'
+lit :: Bool -> Lit
+lit = Bool
+
+negateLit :: Lit -> Lit
+negateLit (Bool b) = Bool (not b)
+negateLit (Lit l) = Lit (negateLiteral l)
diff --git a/src/Ersatz/Internal/Parser.hs b/src/Ersatz/Internal/Parser.hs
new file mode 100644
--- /dev/null
+++ b/src/Ersatz/Internal/Parser.hs
@@ -0,0 +1,62 @@
+--------------------------------------------------------------------
+-- |
+-- Copyright :  (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013
+-- License   :  BSD3
+-- Maintainer:  Edward Kmett <ekmett@gmail.com>
+-- Stability :  experimental
+-- Portability: non-portable
+--
+-- A trivial, inefficient parser with no support for error reporting.
+--------------------------------------------------------------------
+module Ersatz.Internal.Parser
+  ( Parser
+  , runParser
+  , sepBy, sepBy1
+  , token, string
+  , integer, natural
+  , eof
+  , satisfy
+  ) where
+
+import Control.Applicative
+import Control.Monad.State
+import Data.Char (isDigit)
+import Data.Traversable (traverse)
+
+type Parser t a = StateT [t] [] a
+
+runParser :: Parser t a -> [t] -> [a]
+runParser = evalStateT
+
+sepBy :: Parser t a -> Parser t sep -> Parser t [a]
+sepBy p sep = sepBy1 p sep <|> pure []
+
+sepBy1 :: Parser t a -> Parser t sep -> Parser t [a]
+sepBy1 p sep = (:) <$> p <*> many (sep *> p)
+
+token :: Eq t => t -> Parser t t
+token t = satisfy (== t)
+
+string :: Eq t => [t] -> Parser t [t]
+string = traverse token
+
+integer :: (Integral i, Read i) => Parser Char i
+integer = negation <*> natural
+
+negation :: Num n => Parser Char (n -> n)
+negation  =  negate <$ token '-'
+         <|> pure id
+
+natural :: (Integral i, Read i) => Parser Char i
+natural = read <$> some (satisfy isDigit)
+
+eof :: Parser t ()
+eof = do
+  [] <- get
+  return ()
+
+satisfy :: (t -> Bool) -> Parser t t
+satisfy f = do
+  (t:ts) <- get
+  guard (f t)
+  t <$ put ts
diff --git a/src/Ersatz/Internal/StableName.hs b/src/Ersatz/Internal/StableName.hs
new file mode 100644
--- /dev/null
+++ b/src/Ersatz/Internal/StableName.hs
@@ -0,0 +1,23 @@
+{-# OPTIONS_HADDOCK not-home #-}
+--------------------------------------------------------------------
+-- |
+-- Copyright :  (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013
+-- License   :  BSD3
+-- Maintainer:  Edward Kmett <ekmett@gmail.com>
+-- Stability :  experimental
+-- Portability: non-portable
+--
+--------------------------------------------------------------------
+module Ersatz.Internal.StableName
+  ( StableName
+  , makeStableName'
+  ) where
+
+import System.Mem.StableName (StableName, makeStableName)
+import Unsafe.Coerce (unsafeCoerce)
+
+makeStableName' :: a -> IO (StableName ())
+makeStableName' a = a `seq` fmap coerceStableName (makeStableName a)
+  where
+    coerceStableName :: StableName a -> StableName ()
+    coerceStableName = unsafeCoerce
diff --git a/src/Ersatz/Monad.hs b/src/Ersatz/Monad.hs
new file mode 100644
--- /dev/null
+++ b/src/Ersatz/Monad.hs
@@ -0,0 +1,105 @@
+{-# LANGUAGE Rank2Types, GeneralizedNewtypeDeriving, TypeOperators, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, PatternGuards, DeriveDataTypeable, DefaultSignatures, TypeFamilies, BangPatterns #-}
+{-# OPTIONS_HADDOCK not-home #-}
+--------------------------------------------------------------------
+-- |
+-- Copyright :  (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013
+-- License   :  BSD3
+-- Maintainer:  Edward Kmett <ekmett@gmail.com>
+-- Stability :  experimental
+-- Portability: non-portable
+--
+--------------------------------------------------------------------
+module Ersatz.Monad
+  (
+  -- * The SAT Monad
+    SAT(..)
+  , MonadSAT(..)
+  ) where
+
+import Control.Applicative
+import Control.Monad
+import Control.Monad.Reader
+import Control.Monad.RWS.Strict as Strict
+import Control.Monad.RWS.Lazy as Lazy
+import Control.Monad.State.Lazy as Lazy
+import Control.Monad.State.Strict as Strict
+import Control.Monad.Writer.Lazy as Lazy
+import Control.Monad.Writer.Strict as Strict
+import Data.IntSet as IntSet
+import Data.HashMap.Strict as HashMap
+import Ersatz.Internal.Formula
+import Ersatz.Internal.Literal
+import Ersatz.Internal.StableName
+import Ersatz.Problem
+import System.IO.Unsafe
+
+newtype SAT m a = SAT { runSAT :: forall r. (a -> Problem -> m r) -> Problem -> m r }
+
+instance Functor (SAT m) where
+  fmap f (SAT m) = SAT $ \k -> m (k . f)
+  {-# INLINE fmap #-}
+
+instance Applicative (SAT m) where
+  pure a = SAT $ \k -> k a
+  {-# INLINE pure #-}
+
+  (<*>) = ap
+  {-# INLINE (<*>) #-}
+
+instance Monad (SAT m) where
+  return a = SAT $ \k -> k a
+  {-# INLINE return #-}
+
+  SAT m >>= f = SAT $ \k -> m (\a -> runSAT (f a) k)
+  {-# INLINE (>>=) #-}
+
+instance MonadTrans SAT where
+  lift m = SAT $ \k p -> do
+    a <- m
+    k a p
+  {-# INLINE lift #-}
+
+instance MonadIO m => MonadIO (SAT m) where
+  liftIO m = SAT $ \k p -> do
+    a <- liftIO m
+    k a p
+  {-# INLINE liftIO #-}
+
+class (Applicative m, Monad m) => MonadSAT m where
+  sat :: (Problem -> (a, Problem)) -> m a
+  default sat :: (MonadTrans t, MonadSAT n, m ~ t n) => (Problem -> (a, Problem)) -> m a
+  sat = lift . sat
+
+  literalExists :: m Literal
+  literalExists = sat $ \qbf -> let !qbfLastAtom' = qbfLastAtom qbf + 1 in
+    (Literal qbfLastAtom', qbf { qbfLastAtom = qbfLastAtom' })
+  {-# INLINE literalExists #-}
+
+  literalForall :: m Literal
+  literalForall = sat $ \qbf -> let !qbfLastAtom' = qbfLastAtom qbf + 1 in
+    ( Literal qbfLastAtom', qbf { qbfLastAtom = qbfLastAtom', qbfUniversals = IntSet.insert qbfLastAtom' (qbfUniversals qbf) })
+  {-# INLINE literalForall #-}
+
+  assertFormula :: Formula -> m ()
+  assertFormula formula = sat $ \qbf -> ((), qbf { qbfFormula = qbfFormula qbf <> formula })
+  {-# INLINE assertFormula #-}
+
+  generateLiteral :: a -> (forall n. Literal -> SAT n ()) -> m Literal
+  generateLiteral a f = sat $ \qbf -> case HashMap.lookup sn (qbfSNMap qbf) of
+    Just l  -> (l, qbf)
+    Nothing | !qbfLastAtom' <- qbfLastAtom qbf + 1, !l <- Literal qbfLastAtom' ->
+      runSAT (f l) (\_ s -> (l, s)) qbf { qbfSNMap = HashMap.insert sn l (qbfSNMap qbf), qbfLastAtom = qbfLastAtom' }
+    where sn = unsafePerformIO (makeStableName' a)
+  {-# INLINE generateLiteral #-}
+
+instance MonadSAT (SAT m) where
+  sat f = SAT $ \k s -> case f s of
+    (a, t) -> k a t
+
+instance MonadSAT m => MonadSAT (ReaderT r m)
+instance MonadSAT m => MonadSAT (Lazy.StateT s m)
+instance MonadSAT m => MonadSAT (Strict.StateT s m)
+instance (MonadSAT m, Monoid w) => MonadSAT (Lazy.WriterT w m)
+instance (MonadSAT m, Monoid w) => MonadSAT (Strict.WriterT w m)
+instance (MonadSAT m, Monoid w) => MonadSAT (Lazy.RWST r w s m)
+instance (MonadSAT m, Monoid w) => MonadSAT (Strict.RWST r w s m)
diff --git a/src/Ersatz/Problem.hs b/src/Ersatz/Problem.hs
new file mode 100644
--- /dev/null
+++ b/src/Ersatz/Problem.hs
@@ -0,0 +1,112 @@
+{-# LANGUAGE Rank2Types, GeneralizedNewtypeDeriving, TypeOperators, MultiParamTypeClasses, FunctionalDependencies, FlexibleInstances, PatternGuards, DeriveDataTypeable, DefaultSignatures, TypeFamilies, BangPatterns #-}
+{-# OPTIONS_HADDOCK not-home #-}
+--------------------------------------------------------------------
+-- |
+-- Copyright :  (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013
+-- License   :  BSD3
+-- Maintainer:  Edward Kmett <ekmett@gmail.com>
+-- Stability :  experimental
+-- Portability: non-portable
+--
+--------------------------------------------------------------------
+module Ersatz.Problem
+  (
+  -- * Formulas
+    Problem(qbfLastAtom, qbfFormula, qbfUniversals, qbfSNMap)
+  -- * QDIMACS pretty printing
+  , QDIMACS(..)
+  ) where
+
+import Data.Default
+import Data.HashMap.Lazy (HashMap)
+import qualified Data.HashMap.Lazy as HashMap
+import Data.IntSet (IntSet)
+import qualified Data.IntSet as IntSet
+import qualified Data.List as List (groupBy)
+import qualified Data.Set as Set
+import Data.Typeable
+import Ersatz.Internal.Formula
+import Ersatz.Internal.Literal
+import Ersatz.Internal.StableName
+
+------------------------------------------------------------------------------
+-- Problems
+------------------------------------------------------------------------------
+
+-- | A (quantified) boolean formula.
+data Problem = Problem
+  { qbfLastAtom   :: {-# UNPACK #-} !Int      -- ^ The id of the last atom allocated
+  , qbfFormula    :: !Formula                 -- ^ a set of clauses to assert
+  , qbfUniversals :: !IntSet                  -- ^ a set indicating which literals are universally quantified
+  , qbfSNMap      :: !(HashMap (StableName ()) Literal)  -- ^ a mapping used during 'Bit' expansion
+  -- , qbfNameMap    :: !(IntMap String)      -- ^ a map of literals to given names
+  } deriving Typeable
+
+-- TODO: instance Monoid Problem
+
+instance Default Problem where
+  def = Problem 0 (Formula Set.empty) IntSet.empty HashMap.empty
+
+instance Show Problem where
+  showsPrec p qbf = showParen (p > 10)
+                  $ showString "Problem .. " . showsPrec 11 (qbfFormula qbf) . showString " .."
+
+------------------------------------------------------------------------------
+-- Printing Problems
+------------------------------------------------------------------------------
+
+-- | (Q)DIMACS file format pretty printer
+--
+-- This is used to generate the problem statement for a given 'SAT' 'Ersatz.Solver.Solver'.
+class QDIMACS t where
+  qdimacs :: t -> String
+
+instance QDIMACS Literal where
+  qdimacs (Literal n) = show n
+
+instance QDIMACS Formula where
+  qdimacs (Formula cs) = unlines $ map qdimacs (Set.toList cs)
+
+instance QDIMACS Clause where
+  qdimacs (Clause xs) = unwords $ map show (IntSet.toList xs) ++ ["0"]
+
+instance QDIMACS Problem where
+  qdimacs (Problem vars formula@(Formula cs) qs _) =
+    unlines (header : map showGroup quantGroups) ++ qdimacs formula
+    where
+      header = unwords ["p", "cnf", show (vars + padding), show (Set.size cs) ]
+
+      -- "The innermost quantified set is always of type 'e'" per QDIMACS standard
+      padding | Just (n, _) <- IntSet.maxView qs, n == vars = 1
+              | otherwise                                   = 0
+                    -- no universals means we are a plan DIMACS file
+      quantGroups | IntSet.null qs = []
+                    -- otherwise, skip to the first universal and show runs
+                  | otherwise = List.groupBy eqQuant $ quants [head qlist..vars] qlist
+        where qlist = IntSet.toAscList qs
+
+      showGroup :: [Quant] -> String
+      showGroup xs = unwords $ q (head xs) : map (show . getQuant) xs
+
+      eqQuant :: Quant -> Quant -> Bool
+      eqQuant Exists{} Exists{} = True
+      eqQuant Forall{} Forall{} = True
+      eqQuant _ _ = False
+
+      q :: Quant -> String
+      q Exists{} = "e"
+      q Forall{} = "a"
+
+      quants :: [Int] -> [Int] -> [Quant]
+      quants [] _ = []
+      quants (i:is) []     = Exists i : quants is []
+      quants (i:is) jjs@(j:js)
+        | i == j    = Forall i : quants is js
+        | otherwise = Exists i : quants is jjs
+
+-- | An explicit prenex quantifier
+data Quant
+  = Exists { getQuant :: {-# UNPACK #-} !Int }
+  | Forall { getQuant :: {-# UNPACK #-} !Int }
+  deriving Typeable
+
diff --git a/src/Ersatz/Solution.hs b/src/Ersatz/Solution.hs
new file mode 100644
--- /dev/null
+++ b/src/Ersatz/Solution.hs
@@ -0,0 +1,63 @@
+{-# LANGUAGE Rank2Types, ImpredicativeTypes, DeriveDataTypeable #-}
+--------------------------------------------------------------------
+-- |
+-- Copyright :  (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013
+-- License   :  BSD3
+-- Maintainer:  Edward Kmett <ekmett@gmail.com>
+-- Stability :  experimental
+-- Portability: non-portable
+--
+--------------------------------------------------------------------
+module Ersatz.Solution
+  ( Solution(..), solutionFrom
+  , Result(..)
+  , Solver
+  ) where
+
+import Control.Applicative
+import qualified Data.HashMap.Lazy as HashMap
+import Data.IntMap (IntMap)
+import qualified Data.IntMap as IntMap
+import Data.Ix
+import Data.Typeable
+import Ersatz.Internal.Literal
+import Ersatz.Problem
+import System.Mem.StableName (StableName)
+
+data Solution = Solution
+  { solutionLiteral    :: Literal -> Maybe Bool
+  , solutionStableName :: StableName () -> Maybe Bool
+  } deriving Typeable
+
+solutionFrom :: IntMap Bool -> Problem -> Solution
+solutionFrom litMap qbf = Solution lookupLit lookupSN
+  where
+    lookupLit l | i >= 0    = IntMap.lookup i litMap
+                | otherwise = not <$> IntMap.lookup (-i) litMap
+      where i = literalId l
+
+    lookupSN sn = lookupLit =<< HashMap.lookup sn snMap
+
+    snMap = qbfSNMap qbf
+
+data Result
+  = Unsolved
+  | Unsatisfied
+  | Satisfied
+  deriving (Eq,Ord,Ix,Show,Read)
+
+instance Enum Result where
+  fromEnum Unsolved = (-1)
+  fromEnum Unsatisfied = 0
+  fromEnum Satisfied = 1
+
+  toEnum (-1) = Unsolved
+  toEnum 0 = Unsatisfied
+  toEnum 1 = Satisfied
+  toEnum _ = error "Enum.toEnum {Ersatz.Solution.Result}: argument of out range"
+
+instance Bounded Result where
+  minBound = Unsolved
+  maxBound = Satisfied
+
+type Solver m = Problem -> m (Result, IntMap Bool)
diff --git a/src/Ersatz/Solver.hs b/src/Ersatz/Solver.hs
new file mode 100644
--- /dev/null
+++ b/src/Ersatz/Solver.hs
@@ -0,0 +1,25 @@
+--------------------------------------------------------------------
+-- |
+-- Copyright :  (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013
+-- License   :  BSD3
+-- Maintainer:  Edward Kmett <ekmett@gmail.com>
+-- Stability :  experimental
+-- Portability: non-portable
+--
+--------------------------------------------------------------------
+module Ersatz.Solver
+  ( module Ersatz.Solver.Minisat
+  , solveWith
+  ) where
+
+import Data.Default
+import Ersatz.Decoding
+import Ersatz.Monad
+import Ersatz.Solution
+import Ersatz.Solver.Minisat
+
+solveWith :: (Monad m, Decoding a) => Solver m -> SAT m a -> m (Result, Maybe (Decoded a))
+solveWith solver m = do
+  (a, qbf) <- runSAT m (\a s -> return (a , s)) def
+  (res, litMap) <- solver qbf
+  return (res, decode (solutionFrom litMap qbf) a)
diff --git a/src/Ersatz/Solver/Minisat.hs b/src/Ersatz/Solver/Minisat.hs
new file mode 100644
--- /dev/null
+++ b/src/Ersatz/Solver/Minisat.hs
@@ -0,0 +1,86 @@
+--------------------------------------------------------------------
+-- |
+-- Copyright :  (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013
+-- License   :  BSD3
+-- Maintainer:  Edward Kmett <ekmett@gmail.com>
+-- Stability :  experimental
+-- Portability: non-portable
+--
+--------------------------------------------------------------------
+module Ersatz.Solver.Minisat
+  ( minisat
+  , cryptominisat
+  , minisatPath
+  ) where
+
+import Control.Applicative
+import Control.Exception (IOException, handle)
+import Control.Monad
+import Control.Monad.IO.Class
+import Data.IntMap (IntMap)
+import qualified Data.IntMap as IntMap
+import Ersatz.Internal.Parser
+import Ersatz.Problem (qdimacs)
+import Ersatz.Solution
+import System.Exit (ExitCode(..))
+import System.IO.Temp (withSystemTempDirectory)
+import System.Process (readProcessWithExitCode)
+
+
+minisat :: MonadIO m => Solver m
+minisat = minisatPath "minisat"
+
+cryptominisat :: MonadIO m => Solver m
+cryptominisat = minisatPath "cryptominisat"
+
+minisatPath :: MonadIO m => FilePath -> Solver m
+minisatPath path qbf = liftIO $
+  withSystemTempDirectory "ersatz" $ \dir -> do
+    let problemPath  = dir ++ "/problem.cnf"
+        solutionPath = dir ++ "/solution"
+
+    writeFile problemPath (qdimacs qbf)
+
+    (exit, _out, _err) <-
+      readProcessWithExitCode path [problemPath, solutionPath] []
+
+    sol <- parseSolutionFile solutionPath
+
+    return (resultOf exit, sol)
+
+resultOf :: ExitCode -> Result
+resultOf (ExitFailure 10) = Satisfied
+resultOf (ExitFailure 20) = Unsatisfied
+resultOf _                = Unsolved
+
+parseSolutionFile :: FilePath -> IO (IntMap Bool)
+parseSolutionFile path = handle handler $ do
+  parseSolution <$> readFile path
+  where
+    handler :: IOException -> IO (IntMap Bool)
+    handler _ = return IntMap.empty
+
+parseSolution :: String -> (IntMap Bool)
+parseSolution input =
+  case runParser solution input of
+    (s:_) -> s
+    _     -> IntMap.empty
+
+solution :: Parser Char (IntMap Bool)
+solution = do
+  _ <- string "SAT\n"
+  IntMap.fromList <$> values
+
+values :: Parser Char [(Int, Bool)]
+values  = (value `sepBy` token ' ')
+       <* string " 0"
+       <* (() <$ token '\n' <|> eof)
+
+value :: Parser Char (Int, Bool)
+value = do
+  i <- integer
+  guard (i /= 0)
+  return (toPair i)
+  where
+    toPair n | n >= 0    = ( n, True)
+             | otherwise = (-n, False)
diff --git a/src/Ersatz/Variable.hs b/src/Ersatz/Variable.hs
new file mode 100644
--- /dev/null
+++ b/src/Ersatz/Variable.hs
@@ -0,0 +1,64 @@
+{-# LANGUAGE DefaultSignatures, TypeOperators, FlexibleContexts, UndecidableInstances #-}
+--------------------------------------------------------------------
+-- |
+-- Copyright :  (c) Edward Kmett 2010-2013, Johan Kiviniemi 2013
+-- License   :  BSD3
+-- Maintainer:  Edward Kmett <ekmett@gmail.com>
+-- Stability :  experimental
+-- Portability: non-portable
+--
+--------------------------------------------------------------------
+module Ersatz.Variable
+  ( Variable(..)
+  ) where
+
+import Control.Applicative
+import Ersatz.Internal.Literal
+import Ersatz.Monad
+import GHC.Generics
+
+class GVariable f where
+  gexists :: MonadSAT m => m (f a)
+  gforall :: MonadSAT m => m (f a)
+
+instance GVariable U1 where
+  gexists = return U1
+  gforall = return U1
+
+instance (GVariable f, GVariable g) => GVariable (f :*: g) where
+  gexists = (:*:) <$> gexists <*> gexists
+  gforall = (:*:) <$> gforall <*> gforall
+
+instance Variable a => GVariable (K1 i a) where
+  gexists = K1 <$> exists
+  gforall = K1 <$> forall
+
+instance GVariable f => GVariable (M1 i c f) where
+  gexists = M1 <$> gexists
+  gforall = M1 <$> gforall
+
+-- | Instances for this class for product-like types can be automatically derived
+-- for any type that is an instance of @Generic@.
+class Variable t where
+  exists :: MonadSAT m => m t
+  default exists :: (MonadSAT m, Generic t, GVariable (Rep t)) => m t
+  exists = to <$> gexists
+
+  forall :: MonadSAT m => m t
+  default forall :: (MonadSAT m, Generic t, GVariable (Rep t)) => m t
+  forall = to <$> gforall
+
+instance Variable Lit where
+  exists = Lit <$> exists
+  forall = Lit <$> forall
+
+instance Variable Literal where
+  exists = literalExists
+  forall = literalForall
+
+instance (Variable a, Variable b) => Variable (a,b)
+instance (Variable a, Variable b, Variable c) => Variable (a,b,c)
+instance (Variable a, Variable b, Variable c, Variable d) => Variable (a,b,c,d)
+instance (Variable a, Variable b, Variable c, Variable d, Variable e) => Variable (a,b,c,d,e)
+instance (Variable a, Variable b, Variable c, Variable d, Variable e, Variable f) => Variable (a,b,c,d,e,f)
+instance (Variable a, Variable b, Variable c, Variable d, Variable e, Variable f, Variable g) => Variable (a,b,c,d,e,f,g)
diff --git a/tests/doctests.hsc b/tests/doctests.hsc
new file mode 100644
--- /dev/null
+++ b/tests/doctests.hsc
@@ -0,0 +1,72 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE ForeignFunctionInterface #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Main (doctests)
+-- Copyright   :  (C) 2012-13 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+-- Maintainer  :  Edward Kmett <ekmett@gmail.com>
+-- Stability   :  provisional
+-- Portability :  portable
+--
+-- This module provides doctests for a project based on the actual versions
+-- of the packages it was built with. It requires a corresponding Setup.lhs
+-- to be added to the project
+-----------------------------------------------------------------------------
+module Main where
+
+import Build_doctests (deps)
+import Control.Applicative
+import Control.Monad
+import Data.List
+import System.Directory
+import System.FilePath
+import Test.DocTest
+
+##if defined(i386_HOST_ARCH)
+##define USE_CP
+import Control.Applicative
+import Control.Exception
+import Foreign.C.Types
+foreign import stdcall "windows.h SetConsoleCP" c_SetConsoleCP :: CUInt -> IO Bool
+foreign import stdcall "windows.h GetConsoleCP" c_GetConsoleCP :: IO CUInt
+##elif defined(x64_64_HOST_ARCH)
+##define USE_CP
+import Control.Applicative
+import Control.Exception
+import Foreign.C.Types
+foreign import ccall "windows.h SetConsoleCP" c_SetConsoleCP :: CUInt -> IO Bool
+foreign import ccall "windows.h GetConsoleCP" c_GetConsoleCP :: IO CUInt
+##endif
+
+-- | Run in a modified codepage where we can print UTF-8 values on Windows.
+withUnicode :: IO a -> IO a
+##ifdef USE_CP
+withUnicode m = do
+  cp <- c_GetConsoleCP
+  (c_SetConsoleCP 65001 >> m) `finally` c_SetConsoleCP cp
+##else
+withUnicode m = m
+##endif
+
+main :: IO ()
+main = withUnicode $ getSources >>= \sources -> doctest $
+    "-isrc"
+  : "-idist/build/autogen"
+  : "-optP-include"
+  : "-optPdist/build/autogen/cabal_macros.h"
+  : "-hide-all-packages"
+  : "-Iincludes"
+  : map ("-package="++) deps ++ sources
+
+getSources :: IO [FilePath]
+getSources = filter (isSuffixOf ".hs") <$> go "src"
+  where
+    go dir = do
+      (dirs, files) <- getFilesAndDirectories dir
+      (files ++) . concat <$> mapM go dirs
+
+getFilesAndDirectories :: FilePath -> IO ([FilePath], [FilePath])
+getFilesAndDirectories dir = do
+  c <- map (dir </>) . filter (`notElem` ["..", "."]) <$> getDirectoryContents dir
+  (,) <$> filterM doesDirectoryExist c <*> filterM doesFileExist c
diff --git a/tests/properties.hs b/tests/properties.hs
new file mode 100644
--- /dev/null
+++ b/tests/properties.hs
@@ -0,0 +1,45 @@
+module Main where
+
+import Prelude hiding ((||),(&&))
+
+import Test.Framework (Test)
+import Test.Framework (defaultMain, testGroup)
+import Test.Framework.Providers.HUnit
+-- import Test.Framework.Providers.QuickCheck (testProperty)
+import Test.HUnit hiding (Test)
+-- import Test.QuickCheck hiding ((==>))
+
+import Ersatz
+
+main :: IO ()
+main = defaultMain tests
+
+ignore :: Functor f => f a -> f ()
+ignore = fmap (const ())
+
+tests :: [Test]
+tests =
+  [ testGroup "sat" $ zipWith (testCase . show) [1 :: Int ..] $
+      [ -- showSAT (return ()) @?= "p cnf 0 0\n"
+      -- , showSAT (ignore litExists) @?= "p cnf 1 0\n"
+      -- , showSAT (ignore litForall) @?= "p cnf 2 0\na 1\n"
+      -- , showSAT (do x <- forall; y <- exists; assertLits [x,y]) @?= "p cnf 2 1\na 1\ne 2\n1 2 0\n"
+      ]
+  ]
+
+full_adder :: Bit -> Bit -> Bit -> (Bit, Bit)
+full_adder a b cin = (s2, c1 || c2)
+  where (s1,c1) = half_adder a b
+        (s2,c2) = half_adder s1 cin
+
+half_adder :: Bit -> Bit -> (Bit, Bit)
+half_adder a b = (a `xor` b, a && b)
+
+{-
+currying_works :: SAT s ()
+currying_works = do
+  x <- forall
+  y <- forall
+  z <- forall
+  assert $ (x && y) ==> z === x ==> y ==> z
+-}