diff --git a/Data/Boolean/SatSolver.hs b/Data/Boolean/SatSolver.hs
--- a/Data/Boolean/SatSolver.hs
+++ b/Data/Boolean/SatSolver.hs
@@ -23,7 +23,7 @@
 
   newSatSolver, isSolved, 
 
-  lookupVar, assertTrue, branchOnVar, selectBranchVar, solve
+  lookupVar, assertTrue, branchOnVar, selectBranchVar, solve, isSolvable
 
   ) where
 
@@ -92,6 +92,15 @@
 solve solver
   | isSolved solver = return solver
   | otherwise = branchOnUnbound (selectBranchVar solver) solver >>= solve
+
+-- |
+-- This predicate tells whether the stored constraints are
+-- solvable. Use with care! This might be an inefficient operation. It
+-- tries to find a solution using backtracking and returns @True@ if
+-- and only if that fails.
+-- 
+isSolvable :: SatSolver -> Bool
+isSolvable = not . null . solve
 
 
 -- private helper functions
diff --git a/incremental-sat-solver.cabal b/incremental-sat-solver.cabal
--- a/incremental-sat-solver.cabal
+++ b/incremental-sat-solver.cabal
@@ -1,5 +1,5 @@
 Name:          incremental-sat-solver
-Version:       0.1.4
+Version:       0.1.5
 Cabal-Version: >= 1.6
 Synopsis:      Simple, Incremental SAT Solving as a Library
 Description:   This Haskell library provides an implementation of the