diff --git a/build.xml b/build.xml
index 29bb6a77891cd073ddfa1e3ada337e304b55af45..94e104395c90b0b9fdce5ac46e29f41e7b43984e 100644
--- a/build.xml
+++ b/build.xml
@@ -10,6 +10,7 @@
 	<property name="main.class" value="de.stups.probkodkod.KodkodInteraction"/>
 	<property name="lib" value="lib"/>
 	<property name="kodkod" value="${lib}/kodkod.jar"/>
+	<property name="sat4j" value="${lib}/org.sat4j.core.jar"/>
 	<property name="prolog" value="${lib}/prolog.jar"/>
 	<property name="junit" value="${lib}/junit-4.8.2.jar"/>
 	<property name="uptodate" value="uptodate"/>
@@ -20,18 +21,21 @@
 	<target name="init"> 
 		<mkdir dir="${build}"/>
 		<mkdir dir="${jar}"/>
+	</target>
+	
+	<target name="is_uptodate">
 		<uptodate property="parser.uptodate">
 			<srcfiles dir="${src}" includes="*.grammar"/>
 			<mapper type="merge" to="../${parser}/${uptodate}"/>
 		</uptodate>
 	</target>
 	
-	<target name="clear">
+	<target name="clear" depends="init">
 		<delete> <fileset dir="${build}" includes="**/*"/> </delete>
 		<delete includeemptydirs="yes"> <fileset dir="${parser}" includes="**/*"/> </delete>
 	</target>
 	
-	<target name="parser" depends="init" unless="parser.uptodate" description="Generate the parser classes">
+	<target name="parser" depends="is_uptodate,init" unless="parser.uptodate" description="Generate the parser classes">
 		<delete> <fileset dir="${parser}" includes="**/*"/> </delete>
 		<sablecc src="${src}" includes="*.grammar" outputdirectory="${parser}"/>
 		<touch file="${parser}/${uptodate}"/>
@@ -74,6 +78,7 @@
 			<classpath location="${kodkod}"/>
 			<classpath location="${prolog}"/>
 			<classpath location="${junit}"/>
+			<classpath location="${sat4j}"/>
 			<classpath location="${jar}"/>
 			<jvmarg value="-Djava.library.path=${lib}"/>
 			<formatter type="plain" usefile="true" />
diff --git a/lib/org.sat4j.core.jar b/lib/org.sat4j.core.jar
new file mode 100644
index 0000000000000000000000000000000000000000..9e0f01e366b546e7523146f07c0db34f39708930
Binary files /dev/null and b/lib/org.sat4j.core.jar differ
diff --git a/src/de/stups/probkodkod/KodkodSession.java b/src/de/stups/probkodkod/KodkodSession.java
index 75ca5a75ebfd4001d7d5b5403c4a85eea8e83f88..059492f39c9f83d8243ff5e1b9536e0defdf635f 100644
--- a/src/de/stups/probkodkod/KodkodSession.java
+++ b/src/de/stups/probkodkod/KodkodSession.java
@@ -21,6 +21,8 @@ import de.prob.prolog.output.IPrologTermOutput;
  * 
  */
 public class KodkodSession {
+	private final SATFactory SOLVER = SolverChecker.determineSatFactory();
+
 	private final Logger logger = Logger.getLogger(KodkodSession.class
 			.getName());
 	private final Map<String, ImmutableProblem> problems = new HashMap<String, ImmutableProblem>();
@@ -33,7 +35,7 @@ public class KodkodSession {
 		problems.put(id, problem);
 
 		final Solver solver = new Solver();
-		solver.options().setSolver(SATFactory.MiniSat);
+		solver.options().setSolver(SOLVER);
 		solver.options().setSymmetryBreaking(0);
 		final Integer bitwidth = problem.getBitwidth();
 		if (bitwidth != null) {
diff --git a/src/de/stups/probkodkod/SolverChecker.java b/src/de/stups/probkodkod/SolverChecker.java
new file mode 100644
index 0000000000000000000000000000000000000000..c5c06e8d3fde9b92bf9f90d438d336e3aab78682
--- /dev/null
+++ b/src/de/stups/probkodkod/SolverChecker.java
@@ -0,0 +1,65 @@
+/**
+ * 
+ */
+package de.stups.probkodkod;
+
+import java.util.HashMap;
+import java.util.Map;
+import java.util.logging.Level;
+import java.util.logging.Logger;
+
+import kodkod.ast.Formula;
+import kodkod.ast.IntConstant;
+import kodkod.ast.Relation;
+import kodkod.engine.Solver;
+import kodkod.engine.satlab.SATFactory;
+import kodkod.instance.Bounds;
+import kodkod.instance.Universe;
+
+/**
+ * Here we determine if we use Minisat or SAT4J as back-end. We do this by
+ * trying to load minisat.
+ * 
+ * @author plagge
+ */
+public class SolverChecker {
+	private static final Logger LOGGER = Logger
+			.getLogger("de.stups.probkodkod");
+	private static final SATFactory[] FACTORIES = { SATFactory.MiniSat,
+			SATFactory.DefaultSAT4J };
+
+	public static SATFactory determineSatFactory() {
+		Map<String, Throwable> throwables = new HashMap<String, Throwable>();
+		for (final SATFactory factory : FACTORIES) {
+			try {
+				check(factory);
+				// the factory seems to work, we use it
+				LOGGER.info("Using SAT solver back-end: " + factory);
+				return factory;
+			} catch (Throwable t) {
+				// the factory does not work, we store the stack-trace for the
+				// case that no solvers are found
+				throwables.put(factory.toString(), t);
+			}
+		}
+		LOGGER.severe("No SAT solver back-end found.");
+		for (final Map.Entry<String, Throwable> entry : throwables.entrySet()) {
+			final String msg = "Error when trying to use solver: "
+					+ entry.getKey();
+			LOGGER.log(Level.SEVERE, msg, entry.getValue());
+		}
+		throw new Error("No SAT solver back-end for Kodkod found.");
+	}
+
+	private static void check(SATFactory factory) {
+		final Solver solver = new Solver();
+		solver.options().setSolver(factory);
+		final Universe universe = new Universe("a", "b");
+		final Relation relation = Relation.unary("relation");
+		final Formula formula = relation.count().eq(IntConstant.constant(2));
+		final Bounds bounds = new Bounds(universe);
+		bounds.bound(relation, universe.factory().allOf(1));
+		solver.solve(formula, bounds);
+	}
+
+}
diff --git a/test/de/stups/probkodkod/NegativeIntTest.java b/test/de/stups/probkodkod/NegativeIntTest.java
index ce8e04a60e07c144d66a9d282c62c1c0390bab0c..164137f1e26509c0d426b52688bd968b7b9d9267 100644
--- a/test/de/stups/probkodkod/NegativeIntTest.java
+++ b/test/de/stups/probkodkod/NegativeIntTest.java
@@ -10,7 +10,6 @@ import kodkod.ast.IntConstant;
 import kodkod.ast.Relation;
 import kodkod.engine.Solution;
 import kodkod.engine.Solver;
-import kodkod.engine.satlab.SATFactory;
 import kodkod.instance.Bounds;
 import kodkod.instance.Instance;
 import kodkod.instance.Tuple;
@@ -46,7 +45,7 @@ public class NegativeIntTest {
 		bounds.bound(x, factory.allOf(1));
 		final Formula formula = x.sum().eq(IntConstant.constant(value));
 		final Solver solver = new Solver();
-		solver.options().setSolver(SATFactory.MiniSat);
+		solver.options().setSolver(SolverChecker.determineSatFactory());
 		solver.options().setBitwidth(5);
 		final Iterator<Solution> iterator = solver.solveAll(formula, bounds);
 		Assert.assertTrue("solution expected", iterator.hasNext());