diff --git a/pkgs/applications/science/logic/glucose/default.nix b/pkgs/applications/science/logic/glucose/default.nix
new file mode 100644
index 000000000000..5b318be16649
--- /dev/null
+++ b/pkgs/applications/science/logic/glucose/default.nix
@@ -0,0 +1,25 @@
+{ stdenv, fetchurl, zlib }:
+stdenv.mkDerivation rec {
+  name = "glucose-${version}";
+  version = "4.0";
+
+  src = fetchurl {
+    url = "http://www.labri.fr/perso/lsimon/downloads/softwares/glucose-syrup.tgz";
+    sha256 = "0bq5l2jabhdfhng002qfk0mcj4pfi1v5853x3c7igwfrgx0jmfld";
+  };
+
+  buildInputs = [ zlib ];
+
+  sourceRoot = "glucose-syrup/simp";
+  makeFlags = [ "r" ];
+  installPhase = ''
+    install -Dm0755 glucose_release $out/bin/glucose
+  '';
+
+  meta = with stdenv.lib; {
+    description = "Modern, parallel SAT solver (sequential version)";
+    license = licenses.mit;
+    platforms = platforms.unix;
+    maintainers = with maintainers; [ gebner ];
+  };
+}
diff --git a/pkgs/applications/science/logic/glucose/syrup.nix b/pkgs/applications/science/logic/glucose/syrup.nix
new file mode 100644
index 000000000000..7604ebc1a3d9
--- /dev/null
+++ b/pkgs/applications/science/logic/glucose/syrup.nix
@@ -0,0 +1,25 @@
+{ stdenv, fetchurl, zlib }:
+stdenv.mkDerivation rec {
+  name = "glucose-syrup-${version}";
+  version = "4.0";
+
+  src = fetchurl {
+    url = "http://www.labri.fr/perso/lsimon/downloads/softwares/glucose-syrup.tgz";
+    sha256 = "0bq5l2jabhdfhng002qfk0mcj4pfi1v5853x3c7igwfrgx0jmfld";
+  };
+
+  buildInputs = [ zlib ];
+
+  sourceRoot = "glucose-syrup/parallel";
+  makeFlags = [ "r" ];
+  installPhase = ''
+    install -Dm0755 glucose-syrup_release $out/bin/glucose-syrup
+  '';
+
+  meta = with stdenv.lib; {
+    description = "Modern, parallel SAT solver (parallel version)";
+    license = licenses.unfreeRedistributable;
+    platforms = platforms.unix;
+    maintainers = with maintainers; [ gebner ];
+  };
+}
diff --git a/pkgs/top-level/all-packages.nix b/pkgs/top-level/all-packages.nix
index b007154bc2d5..00a64d76d608 100644
--- a/pkgs/top-level/all-packages.nix
+++ b/pkgs/top-level/all-packages.nix
@@ -16230,6 +16230,9 @@ in
 
   ginac = callPackage ../applications/science/math/ginac { };
 
+  glucose = callPackage ../applications/science/logic/glucose { };
+  glucose-syrup = callPackage ../applications/science/logic/glucose/syrup.nix { };
+
   hol = callPackage ../applications/science/logic/hol { };
 
   hol_light = callPackage ../applications/science/logic/hol_light {