2019 evaluation version

fbacchus · Mar 9, 2020 · 415a6e2 · 415a6e2
1 parent 19d29bc
commit 415a6e2
Show file tree

Hide file tree

Showing 67 changed files with 7,303 additions and 591 deletions.
diff --git a/LICENSE b/LICENSE
@@ -1,4 +1,4 @@
-MaxHS -- Copyright (c) 2012-2017 Jessica Davies, Fahiem Bacchus
+1) MaxHS -- Copyright (c) 2012-2017 Jessica Davies, Fahiem Bacchus
 
 Permission is hereby granted, free of charge, to any person obtaining a
 copy of this software and associated documentation files (the
@@ -19,7 +19,7 @@ LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
 OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
 WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
 
-
+2) Minisat:
 MaxHs makes extensive use of MiniSat, for this part of the software
 the minisat license agreement applies and is appened below:
 ==================================================================
@@ -45,3 +45,34 @@ NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE
 LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION
 OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION
 WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+
+3) Glucose:
+MaxHs can optionally be built to use glucose 3.0 instead of MiniSat.
+If glucose is used in the build then this part of the code is subject to
+the glucose license agreement applies appened below:
+==================================================================
+ Glucose -- Copyright (c) 2009-2017, Gilles Audemard, Laurent Simon
+                                CRIL - Univ. Artois, France
+                                LRI  - Univ. Paris Sud, France (2009-2013)
+                                Labri - Univ. Bordeaux, France
+
+ Syrup (Glucose Parallel) -- Copyright (c) 2013-2014, Gilles Audemard, Laurent Simon
+                                CRIL - Univ. Artois, France
+                                Labri - Univ. Bordeaux, France
+
+Glucose sources are based on MiniSat (see aboveMiniSat copyrights). Permissions and copyrights of
+Glucose (sources until 2013, Glucose 3.0, single core) are exactly the same as Minisat on which it 
+is based on. (see below).
+
+Glucose-Syrup sources are based on another copyright. Permissions and copyrights for the parallel
+version of Glucose-Syrup (the "Software") are granted, free of charge, to deal with the Software
+without restriction, including the rights to use, copy, modify, merge, publish, distribute,
+sublicence, and/or sell copies of the Software, and to permit persons to whom the Software is 
+furnished to do so, subject to the following conditions:
+
+- The above and below copyrights notices and this permission notice shall be included in all
+copies or substantial portions of the Software;
+- The parallel version of Glucose (all files modified since Glucose 3.0 releases, 2013) cannot
+be used in any competitive event (sat competitions/evaluations) without the express permission of 
+the authors (Gilles Audemard / Laurent Simon). This is also the case for any competitive event
+using Glucose Parallel as an embedded SAT engine (single core or not).
diff --git a/Makefile b/Makefile
@@ -1,27 +1,21 @@
 ###################################################################################################
-#  make			 "for a satically linked release version"
+#  make			 "for release version"
 #  make d		 "debug version"
 #  make p		 "profiling version"
-#  make config  	 "Set up local locations, see README"
-#  make install 	 "install maxhs executable"
 #  make clean   	 "remove object files and executable"
-#  make distclean 	 "clean and undo config"
 ###################################################################################################
-.PHONY:	r d p lr ld lp  config all install install-bin clean distclean
-all: r lr 
-
-## Load Previous Configuration ####################################################################
-
--include config.mk
+.PHONY:	r d p lr ld lp all install install-bin clean distclean
+all: r
 
 ## Configurable options ###########################################################################
 
-## Cplex library location (configure these variables with "make config")
-LINUX_CPLEXLIBDIR   ?= /w/63/fbacchus/CPLEX_Studio127/cplex/lib/x86-64_linux/static_pic
-LINUX_CPLEXINCDIR   ?= /w/63/fbacchus/CPLEX_Studio127/cplex/include
-##
-DARWIN_CPLEXLIBDIR   ?= /Users/fbacchus/Applications/IBM/ILOG/CPLEX_Studio127/cplex/lib/x86-64_osx/static_pic/
-DARWIN_CPLEXINCDIR   ?= /Users/fbacchus/Applications/IBM/ILOG/CPLEX_Studio127/cplex/include
+## Cplex library location (configure these variables)
+LINUX_CPLEXLIBDIR   ?= /w/63/fbacchus/CPLEX_Studio1210/cplex/lib/x86-64_linux/static_pic
+LINUX_CPLEXINCDIR   ?= /w/63/fbacchus/CPLEX_Studio1210/cplex/include
+#
+#If you want to build on macos
+DARWIN_CPLEXLIBDIR   ?= /Users/fbacchus/Applications/IBM/ILOG/CPLEX_Studio128/cplex/lib/x86-64_osx/static_pic/
+DARWIN_CPLEXINCDIR   ?= /Users/fbacchus/Applications/IBM/ILOG/CPLEX_Studio128/cplex/include
 
 ifeq "$(shell uname)" "Linux"
 CPLEXLIBDIR   =$(LINUX_CPLEXLIBDIR)
@@ -38,39 +32,19 @@ BUILD_DIR      ?= build
 # Include debug-symbols in release builds?
 MAXHS_RELSYM ?= -g
 
-# Sets of compile flags for different build types
-MAXHS_REL    ?= -O3 -D NDEBUG
+# Sat solver you can use minisat of glucose. minisat is faster.for maxhs
+SATSOLVER = minisat
+#SATSOLVER = glucose
+
+MAXHS_REL    ?= -O3 -flto -D NDEBUG
 MAXHS_DEB    ?= -O0 -D DEBUG -D_GLIBCXX_DEBUG -ggdb
 MAXHS_PRF    ?= -O3 -D NDEBUG
 
-# GNU Standard Install Prefix
-prefix         ?= /usr/local
-
-## Write Configuration  ###########################################################################
-
-config:
-	@( echo 'BUILD_DIR?=$(BUILD_DIR)'       ; \
-	   echo 'MAXHS_RELSYM?=$(MAXHS_RELSYM)' ; \
-	   echo 'MAXHS_REL?=$(MAXHS_REL)'       ; \
-	   echo 'MAXHS_DEB?=$(MAXHS_DEB)'       ; \
-	   echo 'MAXHS_PRF?=$(MAXHS_PRF)'       ; \
-	   echo LINUX_CPLEXLIBDIR?=$(LINUX_CPLEXLIBDIR) ; \
-	   echo LINUX_CPLEXINCDIR?=$(LINUX_CPLEXINCDIR) ; \
-	   echo DARWIN_CPLEXLIBDIR?=$(DARWIN_CPLEXLIBDIR) ; \
-	   echo DARWIN_CPLEXINCDIR?=$(DARWIN_CPLEXINCDIR) ; \
-	   echo 'prefix?=$(prefix)'                 ) > config.mk
-
-## Configurable options end #######################################################################
-
-INSTALL ?= install
-
-# GNU Standard Install Variables
-exec_prefix ?= $(prefix)
-includedir  ?= $(prefix)/include
-bindir      ?= $(exec_prefix)/bin
-libdir      ?= $(exec_prefix)/lib
-datarootdir ?= $(prefix)/share
-mandir      ?= $(datarootdir)/man
+ifeq "$(SATSOLVER)" "glucose"
+MAXHS_REL    += -D GLUCOSE
+MAXHS_DEB    += -D GLUCOSE
+MAXHS_PRF    += -D GLUCOSE
+endif
 
 # Target file names
 MAXHS      = maxhs#       Name of Maxhs main executable.
@@ -81,9 +55,9 @@ MAXHS_SLIB = lib$(MAXHS).a#  Name of Maxhs static library.
 MAXHS_CXXFLAGS = -DIL_STD -I. -I$(CPLEXINCDIR)
 MAXHS_CXXFLAGS += -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS 
 MAXHS_CXXFLAGS += -Wall -Wno-parentheses -Wextra -Wno-deprecated
-MAXHS_CXXFLAGS += -std=c++11
+MAXHS_CXXFLAGS += -std=c++14
 
-MAXHS_LDFLAGS  = -Wall -lz -L$(CPLEXLIBDIR) -lcplex -lpthread
+MAXHS_LDFLAGS  = -Wall -lz -L$(CPLEXLIBDIR) -lcplex -lpthread -ldl
 
 ECHO=@echo
 
@@ -93,11 +67,17 @@ else
 VERB=
 endif
 
-SRCS = $(wildcard minisat/core/*.cc) $(wildcard minisat/simp/*.cc) $(wildcard minisat/utils/*.cc) \
+SRCS = $(wildcard $(SATSOLVER)/core/*.cc) $(wildcard $(SATSOLVER)/simp/*.cc) $(wildcard $(SATSOLVER)/utils/*.cc) \
        $(wildcard maxhs/core/*.cc) $(wildcard maxhs/ifaces/*.cc) \
-       $(wildcard maxhs/utils/*.cc) 
-MINISAT_HDRS = $(wildcard minisat/mtl/*.h) $(wildcard minisat/core/*.h) \
-       $(wildcard minisat/utils/*.h) $(wildcard minisat/simp/*.h) 
+       $(wildcard maxhs/utils/*.cc)
+
+ALLSRCS = $(wildcard minisat/core/*.cc) $(wildcard minisat/simp/*.cc) $(wildcard minisat/utils/*.cc) \
+$(wildcard glucose/core/*.cc) $(wildcard glucose/simp/*.cc) $(wildcard glucose/utils/*.cc) \
+$(wildcard maxhs/core/*.cc) $(wildcard maxhs/ifaces/*.cc) \
+$(wildcard maxhs/utils/*.cc)
+
+SATSOLVER_HDRS = $(wildcard $(SATSOLVER)/mtl/*.h) $(wildcard $(SATSOLVER)/core/*.h) \
+       $(wildcard $(SATSOLVER)/utils/*.h) $(wildcard $(SATSOLVER)/simp/*.h)
 MAXHS_HDRS = $(wildcard maxhs/core/*.h) $(wildcard maxhs/ifaces/*.h) \
        $(wildcard maxhs/ds/*.h) $(wildcard maxhs/utils/*.h) 
 
@@ -120,12 +100,12 @@ $(BUILD_DIR)/profile/%.o:			MAXHS_CXXFLAGS +=$(MAXHS_PRF) -pg
 ## Build-type Link-flags:
 $(BUILD_DIR)/profile/bin/$(MAXHS):		MAXHS_LDFLAGS += -pg
 ifeq "$(shell uname)" "Linux"
-$(BUILD_DIR)/release/bin/$(MAXHS):		MAXHS_LDFLAGS += --static -z muldefs
+$(BUILD_DIR)/release/bin/$(MAXHS):		MAXHS_LDFLAGS += -z muldefs
 endif
 $(BUILD_DIR)/release/bin/$(MAXHS):		MAXHS_LDFLAGS += $(MAXHS_RELSYM)
 
 ## Executable dependencies
-$(BUILD_DIR)/release/bin/$(MAXHS):	 	$(BUILD_DIR)/release/maxhs/core/Main.o $(BUILD_DIR)/release/lib/$(MAXHS_SLIB)
+$(BUILD_DIR)/release/bin/$(MAXHS):	 	$(BUILD_DIR)/release/maxhs/core/Main.o $(foreach o,$(OBJS),$(BUILD_DIR)/release/$(o))
 $(BUILD_DIR)/debug/bin/$(MAXHS):	 	$(BUILD_DIR)/debug/maxhs/core/Main.o $(BUILD_DIR)/debug/lib/$(MAXHS_SLIB)
 $(BUILD_DIR)/profile/bin/$(MAXHS):	 	$(BUILD_DIR)/profile/maxhs/core/Main.o $(BUILD_DIR)/profile/lib/$(MAXHS_SLIB)
 
@@ -161,52 +141,12 @@ $(BUILD_DIR)/release/bin/$(MAXHS) $(BUILD_DIR)/debug/bin/$(MAXHS) $(BUILD_DIR)/p
 	$(ECHO) Linking Static Library: $@
 	$(VERB) mkdir -p $(dir $@)
 	$(VERB) $(AR) -rcs $@ $^
-
-install:	install-headers install-lib install-bin
-
-install-debug:	install-headers install-lib-debug
-
-install-headers:
-#       Create directories
-	$(INSTALL) -d $(DESTDIR)$(includedir)/maxhs
-	$(INSTALL) -d $(DESTDIR)$(includedir)/minisat
-#
-	for dir in maxhs/core maxhs/ifaces maxhs/ds maxhs/utils; do \
-	  $(INSTALL) -d $(DESTDIR)$(includedir)/$$dir ; \
-        done
-	for dir in minisat/mtl minisat/utils minisat/core minisat/simp; do \
-	  $(INSTALL) -d $(DESTDIR)$(includedir)/$$dir ; \
-	done
-# Install headers
-	for h in $(MINISAT_HDRS) ; do \
-	  $(INSTALL) -m 644 $$h $(DESTDIR)$(includedir)/$$h ; \
-	done
-	for h in $(MAXHS_HDRS) ; do \
-	  $(INSTALL) -m 644 $$h $(DESTDIR)$(includedir)/$$h ; \
-	done
-
-
-install-lib-debug: $(BUILD_DIR)/debug/lib/$(MAXHS_SLIB)
-	$(INSTALL) -d $(DESTDIR)$(libdir)
-	$(INSTALL) -m 644 $(BUILD_DIR)/debug/lib/$(MAXHS_SLIB) $(DESTDIR)$(libdir)
-
-install-lib: $(BUILD_DIR)/release/lib/$(MAXHS_SLIB) 
-	$(INSTALL) -d $(DESTDIR)$(libdir)
-	$(INSTALL) -m 644 $(BUILD_DIR)/release/lib/$(MAXHS_SLIB) $(DESTDIR)$(libdir)
-
-install-bin: $(BUILD_DIR)/release/bin/$(MAXHS)
-	$(INSTALL) -d $(DESTDIR)$(bindir)
-	$(INSTALL) -m 755 $(BUILD_DIR)/release/bin/$(MAXHS) $(DESTDIR)$(bindir)
-
 clean:
-	rm -f $(foreach t, release debug profile, $(foreach o, $(SRCS:.cc=.o), $(BUILD_DIR)/$t/$o)) \
-          $(foreach t, release debug profile, $(foreach d, $(SRCS:.cc=.d), $(BUILD_DIR)/$t/$d)) \
+	rm -f $(foreach t, release debug profile, $(foreach o, $(ALLSRCS:.cc=.o), $(BUILD_DIR)/$t/$o)) \
+          $(foreach t, release debug profile, $(foreach d, $(ALLSRCS:.cc=.d), $(BUILD_DIR)/$t/$d)) \
 	  $(foreach t, release debug profile, $(BUILD_DIR)/$t/bin/$(MAXHS)) \
 	  $(foreach t, release debug profile, $(BUILD_DIR)/$t/lib/$(MAXHS_SLIB))
 
-distclean:	clean
-	rm -f config.mk
-
 ## Include generated dependencies
 -include $(foreach s, $(SRCS:.cc=.d), $(BUILD_DIR)/release/$s)
 -include $(foreach s, $(SRCS:.cc=.d), $(BUILD_DIR)/debug/$s)

diff --git a/README b/README
@@ -13,83 +13,67 @@ Building and installing:
    available from IBM under their academic Initiative program. It is
    free to faculty members and graduate students in academia. 
 
-   try 
-   http://www-03.ibm.com/ibm/university/academic/pub/page/ban_ilog_programming
+   try https://www.ibm.com/academic 
 
-   a google search should find the right site.
-   You apply for their academic initiative program and then then you
-   can download CPLEX and other IBM software. 
+   If that fails aa google search of 'IBM academic initiative' should
+   find the right site.  You apply for their academic initiative
+   program and then then you can download CPLEX and other IBM
+   software.
 
    Note. CPLEX is very useful for many tasks and well worth having
    access to irrespective of MaxHS. 
 
+1) clone maxhs from https://github.com/fbacchus/MaxHS
 
-1) Configure
-------------
-Use "make config VAR=defn" or edit config.mk directly. 
+2) Move into the MaxHS directory and edit the Makefile to
+   properly set the following Makefile variables
 
 REQUIRED VARIABLE SETTINGS:
 ===========================
 
 LINUX_CPLEXLIBDIR=<path to CPLEX library>
    #the directory on your linux system that contains libcplex.a
-   #and libilocplex.a (the makefile does a static build)
+   #and libilocplex.a
 LINUX_CPLEXINCDIR=<path to CPLEX headers>
 
+and if you want to build on macos
+
 DARWIN_CPLEXLIBDIR=<path to CPLEX library>
    #the directory on your MAC system that contains libcplex.a
-   #and libilocplex.a (the makefile does a static build)
+   #and libilocplex.a 
 DARWIN_CPLEXINCDIR=<path to CPLEX headers>
 
 NOTE: you do not have to set both the LINUX_ and DARWIN_ variables, just
 the ones for the operating system you are using. 
 
-RECOMMENDED VARIABLE SETTINGS:
-==============================
-
-prefix=<location for install; default = '/usr/local'>
-  #Root install directory for GNU standard install locations 
-  #finer control can be achieved by modifying the GNU install
-  #variables (e.g., includedir, bindir, etc). See the Makefile
-  #"make install" will put the executable in $(prefix)/bin
-
-  #Change this if you want to install MaxHS (you can also use the
-  #executable directly from the build/release/bin directory), and
-  #you do not want to install it it the system directories
-
-OPTIONAL VARIABLE SETTINGS:
-==========================
-
-Various compiler settings can be configured, see the Makefile
-
-Notes:
-
-- Multiple configuration steps can be joined into one call to "make
-  config" by appending multiple variable assignments on the same line.
+3) Build
+-----------
+In the MaxHS directory execute
 
-- The configuration is stored in the file "config.mk". Look here if
-  you want to know what the current configuration looks like.
+make
 
-- To reset from defaults simply remove the "config.mk" file or call
-  "make distclean".
+4) Run
+---------
+The executable is built in MaxHS/build/release/bin/ if you change to that
+directory you should be able to execute
 
-- Once configured, recompilation can be done as many times as wanted. 
+./maxhs -no-printSoln <maxsat instance file>
 
-2) Compile and Build 
------------
+use
+./maxhs --help
+or
+./maxhs --help-verb
 
-make install
+to obtain a listing of the available parameter settings
 
 ================================================================================
 Directory Overview:
 
 maxhs/                  MaxHs code
-minisat/mtl/            Minsat  Template Library
-minisat/utils/          Minisat helper code (I/O, Parsing, CPU-time, etc)
-minisat/core/           Minisat core solver (does not do simplification)
-doc/                    Documentation...right now try "maxhs --help" ;-<
+minisat/                Minisat SAT solver with changes to make assumptions more
+                        efficient
+glucose/                Glucose SAT solver 
 README
 LICENSE
-
 ================================================================================
 
diff --git a/config.mk b/config.mk