How to obtain an ipasir backend implementation.
There are several SAT solver libraries that implement the IPASIR interface; in particular, the entrants in the 2016 and 2017 SAT Competitions are available, respectively, here and here. However, the build scripts for these libraries are configured to produce a static library, and we need a shared library so that we can link it into a running Lisp session. We'll walk through the steps necessary to adapt the makefile to build a Linux shared library for glucose, whose sources are available here.
First, ensure that you have gcc and g++ version 6 or greater.
Unzip the archive and edit the file "sat/glucose4/makefile" as follows:
Or apply the following patch instead:
32,33c32,33 < CXXFLAGS= -g -std=c++11 -Wall -DNDEBUG -O3 < --- > CXXFLAGS= -g -std=c++11 -Wall -DNDEBUG -O3 -fPIC > export CXXFLAGS 70c70 < $(CXX) -g -std=c++11 $(CXXLAGS) \ --- > $(CXX) -g -std=c++11 $(CXXFLAGS) \
After fixing the makefile, run "make". This should produce files "ipasirglucoseglue.o" and "libipasirglucose4.a".
Link those two files into a shared library. For Linux, this can be done as follows:
g++ -shared -Wl,-soname,libipasirglucose4.so -o libipasirglucose4.so \ ipasirglucoseglue.o libipasirglucose4.a
(Note: Counterintuitively, it is important that the .o file is listed before the .a file.)
Finally, move the resulting shared library "libipasirglucose4.so" to a permanent location and either: