diff --git a/.hlint.yaml b/.hlint.yaml
--- a/.hlint.yaml
+++ b/.hlint.yaml
@@ -1,3 +1,5 @@
+- arguments: [--cpp-define=HLINT, --cpp-ansi]
+
 - ignore:
     name: Use camelCase
 
diff --git a/.travis.yml b/.travis.yml
--- a/.travis.yml
+++ b/.travis.yml
@@ -4,7 +4,7 @@
 #
 # For more information, see https://github.com/haskell-CI/haskell-ci
 #
-# version: 0.3.20190425
+# version: 0.3.20190521
 #
 language: c
 dist: xenial
@@ -119,7 +119,6 @@
   - cat $CABALHOME/config
   - rm -fv cabal.project cabal.project.local cabal.project.freeze
   - travis_retry ${CABAL} v2-update -v
-  - if [ $HCNUMVER -eq 80801 ] ; then ${CABAL} v2-install -w ${HC} -j2 hlint --constraint='hlint ==2.1.*' | color_cabal_output ; fi
   # Generate cabal.project
   - rm -rf cabal.project cabal.project.local cabal.project.freeze
   - touch cabal.project
@@ -130,7 +129,7 @@
     echo "  flags: +examples"                  >> cabal.project
     echo ""                                    >> cabal.project
     echo "write-ghc-environment-files: always" >> cabal.project
-  - "for pkg in $($HCPKG list --simple-output); do echo $pkg | sed 's/-[^-]*$//' | grep -vE -- '^(ersatz)$' | sed 's/^/constraints: /' | sed 's/$/ installed/' >> cabal.project.local; done"
+  - "for pkg in $($HCPKG list --simple-output); do echo $pkg | sed 's/-[^-]*$//' | (grep -vE -- '^(ersatz)$' || true) | sed 's/^/constraints: /' | sed 's/$/ installed/' >> cabal.project.local; done"
   - cat cabal.project || true
   - cat cabal.project.local || true
   - if [ -f "./configure.ac" ]; then (cd "." && autoreconf -i); fi
@@ -156,7 +155,7 @@
     echo "  flags: +examples"                  >> cabal.project
     echo ""                                    >> cabal.project
     echo "write-ghc-environment-files: always" >> cabal.project
-  - "for pkg in $($HCPKG list --simple-output); do echo $pkg | sed 's/-[^-]*$//' | grep -vE -- '^(ersatz)$' | sed 's/^/constraints: /' | sed 's/$/ installed/' >> cabal.project.local; done"
+  - "for pkg in $($HCPKG list --simple-output); do echo $pkg | sed 's/-[^-]*$//' | (grep -vE -- '^(ersatz)$' || true) | sed 's/^/constraints: /' | sed 's/$/ installed/' >> cabal.project.local; done"
   - cat cabal.project || true
   - cat cabal.project.local || true
   # Building with tests and benchmarks...
@@ -164,10 +163,6 @@
   - ${CABAL} v2-build -w ${HC} ${TEST} ${BENCH} all | color_cabal_output
   # Testing...
   - ${CABAL} v2-test -w ${HC} ${TEST} ${BENCH} all | color_cabal_output
-  # HLint..
-  - if [ $HCNUMVER -eq 80801 ] ; then (cd ersatz-* && hlint --cpp-ansi --cpp-define=HLINT src) ; fi
-  - if [ $HCNUMVER -eq 80801 ] ; then (cd ersatz-* && hlint --cpp-ansi --cpp-define=HLINT examples/sudoku) ; fi
-  - if [ $HCNUMVER -eq 80801 ] ; then (cd ersatz-* && hlint --cpp-ansi --cpp-define=HLINT examples/regexp-grid) ; fi
   # cabal check...
   - (cd ersatz-* && ${CABAL} -vnormal check)
   # haddock...
diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,7 @@
+0.4.7 [2019.06.01]
+------------------
+* Add `anyminisat` and `trySolvers`
+
 0.4.6 [2019.05.20]
 ------------------
 * Add support for `cryptominisat5`
diff --git a/ersatz.cabal b/ersatz.cabal
--- a/ersatz.cabal
+++ b/ersatz.cabal
@@ -1,5 +1,5 @@
 name:           ersatz
-version:        0.4.6
+version:        0.4.7
 license:        BSD3
 license-file:   LICENSE
 author:         Edward A. Kmett, Eric Mertens, Johan Kiviniemi
diff --git a/src/Ersatz/Solver.hs b/src/Ersatz/Solver.hs
--- a/src/Ersatz/Solver.hs
+++ b/src/Ersatz/Solver.hs
@@ -24,9 +24,13 @@
 import Ersatz.Solver.Minisat
 
 #if __GLASGOW_HASKELL__ < 710
-solveWith :: (Monad m, Alternative n, MonadPlus n, HasSAT s, Default s, Codec a) => Solver s m -> StateT s m a -> m (Result, n (Decoded a))
+solveWith ::
+  (Monad m, Alternative n, MonadPlus n, HasSAT s, Default s, Codec a) =>
+  Solver s m -> StateT s m a -> m (Result, n (Decoded a))
 #else
-solveWith :: (Monad m, MonadPlus n, HasSAT s, Default s, Codec a) => Solver s m -> StateT s m a -> m (Result, n (Decoded a))
+solveWith ::
+  (Monad m, MonadPlus n, HasSAT s, Default s, Codec a) =>
+  Solver s m -> StateT s m a -> m (Result, n (Decoded a))
 #endif
 solveWith solver m = do
   (a, problem) <- runStateT m def
diff --git a/src/Ersatz/Solver/Common.hs b/src/Ersatz/Solver/Common.hs
--- a/src/Ersatz/Solver/Common.hs
+++ b/src/Ersatz/Solver/Common.hs
@@ -10,11 +10,17 @@
 module Ersatz.Solver.Common
   ( withTempFiles
   , resultOf
+
+  -- * Support for trying many solvers
+  , trySolvers
+  , NoSolvers(..)
   ) where
 
+import Control.Exception (Exception(..), throwIO)
 import Control.Monad.IO.Class
 import Ersatz.Solution
 import System.Exit (ExitCode(..))
+import System.IO.Error (isDoesNotExistError, tryIOError)
 import System.IO.Temp (withSystemTempDirectory)
 
 withTempFiles :: MonadIO m
@@ -32,3 +38,25 @@
 resultOf (ExitFailure 10) = Satisfied
 resultOf (ExitFailure 20) = Unsatisfied
 resultOf _                = Unsolved
+
+-- | This error is thrown by 'trySolvers' when no solvers are found.
+newtype NoSolvers = NoSolvers [IOError] deriving Show
+
+instance Exception NoSolvers where
+  displayException _ = "no ersatz solvers were found"
+
+-- | Try a list of solvers in order. When a solver fails due to
+-- a missing executable the next solver will be tried. Throws
+-- 'NoSolvers' exception if none of the given solvers were installed.
+trySolvers :: [Solver s IO] -> Solver s IO
+trySolvers solvers problem = foldr runSolver noSolvers solvers []
+  where
+    noSolvers = throwIO . NoSolvers . reverse
+
+    runSolver solver next es =
+      do res <- tryIOError (solver problem)
+         case res of
+           Left e
+             | isDoesNotExistError e -> next (e:es)
+             | otherwise             -> ioError e
+           Right x                   -> return x
diff --git a/src/Ersatz/Solver/Minisat.hs b/src/Ersatz/Solver/Minisat.hs
--- a/src/Ersatz/Solver/Minisat.hs
+++ b/src/Ersatz/Solver/Minisat.hs
@@ -16,6 +16,7 @@
   , minisatPath
   , cryptominisat5
   , cryptominisat5Path
+  , anyminisat
   ) where
 
 import Data.ByteString.Builder
@@ -31,6 +32,10 @@
 
 import qualified Data.ByteString.Char8 as B
 import Data.List ( foldl' )
+
+-- | Hybrid 'Solver' that tries to use: 'cryptominisat5', 'cryptominisat', and 'minisat'
+anyminisat :: Solver SAT IO
+anyminisat = trySolvers [cryptominisat5, cryptominisat, minisat]
 
 -- | 'Solver' for 'SAT' problems that tries to invoke the @minisat@ executable from the @PATH@
 minisat :: MonadIO m => Solver SAT m
diff --git a/tests/Moore.hs b/tests/Moore.hs
--- a/tests/Moore.hs
+++ b/tests/Moore.hs
@@ -38,7 +38,7 @@
 
 mainf d k n s = do
   putStrLn $ unwords [ "degree <=", show d, "diameter <=", show k, "nodes ==", show n, "symmetry ==", show s ]
-  (s, mg) <- solveWith cryptominisat5 $ moore d k n s
+  (s, mg) <- solveWith anyminisat $ moore d k n s
   case (s, mg) of
      (Satisfied, Just g) -> do printA g ; return True
      _ -> do return False
diff --git a/tests/Speed.hs b/tests/Speed.hs
--- a/tests/Speed.hs
+++ b/tests/Speed.hs
@@ -14,7 +14,7 @@
 
 mainf n = do
   putStrLn $ unwords [ "n",  show n ]
-  (s, mgs) <- solveWith cryptominisat5 $ do
+  (s, mgs) <- solveWith anyminisat $ do
       gs <- replicateM n exists
       forM_ (zip gs $ tail gs) $ \ (x,y) -> assert ( x /== y )
       return (gs :: [Bit])
diff --git a/tests/Z001.hs b/tests/Z001.hs
--- a/tests/Z001.hs
+++ b/tests/Z001.hs
@@ -15,7 +15,7 @@
 import Control.Monad.State
 
 main = do
-  (Satisfied, Just ms) <- solveWith cryptominisat5 $ do
+  (Satisfied, Just ms) <- solveWith anyminisat $ do
     [ Restricted a, Restricted b ]
         :: [ Restricted 5 (NBV 3) ] <- replicateM 2 unknown
     -- assert $ gt (a^2 * b^2) (b^3 * a^3)