Merge branch 'development'

README.md

@@ -1,4 +1,4 @@
-[![wercker status](https://app.wercker.com/status/24c4765f3a0d79520ad80a1e4c20cfa2/s/master "wercker status")](https://app.wercker.com/project/bykey/24c4765f3a0d79520ad80a1e4c20cfa2) [![Coverage Status](https://coveralls.io/repos/logic-ng/LogicNG/badge.svg?branch=master&service=github)](https://coveralls.io/github/logic-ng/LogicNG?branch=master) ![License](https://img.shields.io/badge/license-Apache%202-blue.svg) ![Version](https://img.shields.io/badge/version-1.5.2-ff69b4.svg)
+[![wercker status](https://app.wercker.com/status/24c4765f3a0d79520ad80a1e4c20cfa2/s/master "wercker status")](https://app.wercker.com/project/bykey/24c4765f3a0d79520ad80a1e4c20cfa2) [![Coverage Status](https://coveralls.io/repos/logic-ng/LogicNG/badge.svg?branch=master&service=github)](https://coveralls.io/github/logic-ng/LogicNG?branch=master) ![License](https://img.shields.io/badge/license-Apache%202-blue.svg) ![Version](https://img.shields.io/badge/version-1.6.0-ff69b4.svg)
 
 <img src="https://github.com/logic-ng/LogicNG/blob/master/doc/logo/logo_big.png" alt="logo" width="300">
 
@@ -19,7 +19,7 @@ LogicNG is released in the Maven Central Repository.  To include it just add
 <dependency>
   <groupId>org.logicng</groupId>
   <artifactId>logicng</artifactId>
-  <version>1.5.2</version>
+  <version>1.6.0</version>
 </dependency>
 ```
 to your Maven POM.
@@ -63,6 +63,15 @@ The library is released under the Apache License and therefore is free to use in
 
 ## Changelog
 
+### Version 1.6.0 (Release September 2019)
+* A new method for generating CNFs directly on the solver instead of using the formula factory.
+  This often leads to a faster generation and reduced Heap consumption but with the loss of 
+  caching
+* The standard MiniSat-based solvers can now directly efficiently compute a backone.  No extra solver 
+  is required anymore
+* The current formula on a MiniSat-based solver can be extracted
+* BDD factory can now be extended externally
+
 ### Version 1.5.2 (Release July 2019)
 * Fixed caching behaviour when using a `sat()` call without assumptions after a call with assumptions
 * Clarified behaviour of the `Backbone` object

pom.xml

@@ -26,7 +26,7 @@
   <modelVersion>4.0.0</modelVersion>
   <groupId>org.logicng</groupId>
   <artifactId>logicng</artifactId>
-  <version>1.5.2</version>
+  <version>1.6.0</version>
   <packaging>jar</packaging>
 
   <name>LogicNG</name>

src/main/java/org/logicng/backbones/BackboneGeneration.java

@@ -29,7 +29,9 @@
 package org.logicng.backbones;
 
 import org.logicng.formulas.Formula;
+import org.logicng.formulas.FormulaFactory;
 import org.logicng.formulas.Variable;
+import org.logicng.solvers.MiniSat;
 import org.logicng.util.FormulaHelper;
 
 import java.util.Collection;
@@ -39,31 +41,18 @@
  * Main entry point for backbone computations.
  * <p>
  * This class provides convenient methods for backbone computation for many use cases.
- * For more control over the backbone solver you can create an instance of
- * {@link MiniSatBackbone} directly.  E.g., with an instance of {@link MiniSatBackbone}
- * the already loaded formulas can be re-used for multiple backbone computations.
- * @version 1.5.1
+ * @version 1.6.0
  * @since 1.5.0
  */
 public class BackboneGeneration {
 
-    private static final MiniSatBackbone solver = new MiniSatBackbone();
-
     /**
      * Private constructor.
      */
     private BackboneGeneration() {
         // Intentionally left empty.
     }
 
-    /**
-     * Sets a new backbone configuration.
-     * @param config the new backbone configuration
-     */
-    public static void setConfig(final BackboneConfig config) {
-        solver.setConfig(config);
-    }
-
     /**
      * Computes the backbone for a given collection of formulas w.r.t. a collection of variables and a backbone type.
      * @param formulas  the given collection of formulas
@@ -72,9 +61,13 @@ public static void setConfig(final BackboneConfig config) {
      * @return the backbone or {@code null} if the formula is UNSAT
      */
     public static Backbone compute(final Collection<Formula> formulas, final Collection<Variable> variables, final BackboneType type) {
-        solver.reset();
-        solver.add(formulas);
-        return solver.compute(variables, type);
+        if (formulas == null || formulas.isEmpty()) {
+            throw new IllegalArgumentException("Provide at least one formula for backbone computation");
+        }
+        final FormulaFactory f = formulas.iterator().next().factory();
+        final MiniSat miniSat = MiniSat.miniSat(f);
+        miniSat.add(formulas);
+        return miniSat.backbone(variables, type);
     }
 
     /**