README.md

glucose4j

Accessing the native Glucose SAT solver through IPASIR interface and its Java binding

This project packages native shared libraries of the Glucose SAT solver so that they can be used in Apache Maven projects.

Overview and usage

This project consists of two modules:

• glucose: This module contains precompiled native shared libraries that implement the Reentrant Incremental Sat solver API (reverse: IPASIR) used in SAT competitions. The native functions can be accessed, e.g., using the Java Native Access (JNA). To use this library from Apache Maven, add the following dependency to your project, where <classifier> should be replaced with JNA canonical prefix for your platform {OS}-{ARCH} (see https://github.com/java-native-access/jna/blob/master/www/GettingStarted.md).

    <dependency>
    	<groupId>com.github.liveontologies</groupId>
    	<artifactId>glucose</artifactId>
    	<version>...</version>
    	<classifier>linux-x86-64</classifier>
    </dependency>
  

• glucose4j: This module provides Java bindings for the native library using the IPASIR4J library -- a Java version of the IPASIR C library. To use this library add the following maven dependency:

   <dependency>
   	<groupId>com.github.liveontologies</groupId>
   	<artifactId>glucose4j</artifactId>
   	<version>...</version>
   </dependency>
  

See src/test/test for examples on how to use this library. The native library glucose for the current platform will be automatically added as a compile/runtime dependency. To include the library dependencies for all available platforms set a system property multi-platform, e.g., by adding a switch -Dmulti-platform to the maven command. This may be desirable, e.g., for creating platform-independent "stand-alone" jars.

To use snapshots versions of this library (if not compiled from sources), please add the sonatype snapshot repository either to your pom.xml or settings.xml:

<repositories>
  <repository>
    <id>ossrh</id>
    <url>https://oss.sonatype.org/content/repositories/snapshots</url>
    <snapshots>
      <enabled>true</enabled>
    </snapshots>			
  </repository>
</repositories>

Compiling from sources

To compile this software, one has to install Apache Maven version 3 or higher and standard development tools such as Make and GCC. To build all modules, issue the following command from this folder:

mvn clean install

License

All sources of this project are available under the terms of the Apache License 2.0 (see the file LICENSE.txt).

In addition, the sources of the module glucose are available under the terms of the MIT license, so that it is compatible to the license of the glucose solver (see the file glucose/LICENSE.txt).