Index: math/Makefile
===================================================================
--- math/Makefile
+++ math/Makefile
@@ -204,6 +204,7 @@
     SUBDIR += glgraph
     SUBDIR += glm
     SUBDIR += glpk
+    SUBDIR += glucose
     SUBDIR += gmm++
     SUBDIR += gmp
     SUBDIR += gmp-ecm
Index: math/glucose/Makefile
===================================================================
--- /dev/null
+++ math/glucose/Makefile
@@ -0,0 +1,27 @@
+# $FreeBSD$
+
+PORTNAME=	glucose
+DISTVERSION=	4.1
+CATEGORIES=	math
+MASTER_SITES=	http://www.labri.fr/perso/lsimon/downloads/softwares/
+DISTNAME=	glucose-syrup-${DISTVERSION}
+
+MAINTAINER=	yuri@FreeBSD.org
+COMMENT=	Parallel SAT solver based on Minisat, with glue clauses
+
+LICENSE=	MIT
+LICENSE_FILE=	${WRKSRC}/LICENCE
+
+USES=		gmake tar:tgz
+
+PLIST_FILES=	bin/glucose bin/glucose-syrup
+
+do-build:
+	@cd ${WRKSRC}/simp && ${MAKE_CMD}
+	@cd ${WRKSRC}/parallel && ${MAKE_CMD}
+
+do-install:
+	${INSTALL_PROGRAM} ${WRKSRC}/simp/glucose ${STAGEDIR}${PREFIX}/bin/
+	${INSTALL_PROGRAM} ${WRKSRC}/parallel/glucose-syrup ${STAGEDIR}${PREFIX}/bin/
+
+.include <bsd.port.mk>
Index: math/glucose/distinfo
===================================================================
--- /dev/null
+++ math/glucose/distinfo
@@ -0,0 +1,3 @@
+TIMESTAMP = 1517475160
+SHA256 (glucose-syrup-4.1.tgz) = 51aa1cf1bed2b14f1543b099e85a56dd1a92be37e6e3eb0c4a1fd883d5cc5029
+SIZE (glucose-syrup-4.1.tgz) = 82779
Index: math/glucose/files/patch-utils_System.cc
===================================================================
--- /dev/null
+++ math/glucose/files/patch-utils_System.cc
@@ -0,0 +1,11 @@
+--- utils/System.cc.orig	2018-02-01 09:11:32 UTC
++++ utils/System.cc
+@@ -78,7 +78,7 @@ double Glucose::memUsed(void) {
+     struct rusage ru;
+     getrusage(RUSAGE_SELF, &ru);
+     return (double)ru.ru_maxrss / 1024; }
+-double MiniSat::memUsedPeak(void) { return memUsed(); }
++//double MiniSat::memUsedPeak(void) { return memUsed(); }
+ 
+ 
+ #elif defined(__APPLE__)
Index: math/glucose/pkg-descr
===================================================================
--- /dev/null
+++ math/glucose/pkg-descr
@@ -0,0 +1,12 @@
+Glucose is based on the MiniSat solver, and extends it by preserving
+the so-called "glue clauses" and using new scoring scheme.
+
+Glucose is a SAT solver based on a particular scoring scheme for the clause
+learning mechanism, based on the paper Laurent Simon and Gilles Audemard
+presented at IJCAI'09. Solver's name is a contraction of the concept of
+"glue clauses", a particular kind of clauses that glucose detects and preserves
+during search.
+
+Glucode accepts SAT problems in the DIMACS format.
+
+WWW: http://www.labri.fr/perso/lsimon/glucose/