Merge pull request #43 from logic-ng/development

Development

Author: czengler

.gitignore

@@ -20,6 +20,9 @@ src/test/resources/partialweightedmaxsat/log.txt
 
 # test temporary files
 src/test/resources/writers/temp/*.dot
+src/test/resources/writers/temp/*.txt
+src/test/resources/writers/temp/*.cnf
+src/test/resources/writers/temp/*.map
 
 # LSP
 .settings

CHANGELOG.md

@@ -2,6 +2,25 @@
 
 LogicNG uses [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 
+## [2.4.0] - 2022-11-24
+
+### Added
+
+- Completely rewritten graphical outputs of formulas, BDDs, and graphs in the package `org.logicng.io.graphical`. It is now possible to configure the
+  generated graphs by dynamically styling nodes, edges, and computing node labels. Also, there are now two possible output formats: GraphViz DOT and Mermaid.js.
+- Convenience methods `isSatisfiable`, `isTautology`, `isContradiction`, `implies`, `isImpliedBy` and `isEquivalentTo` in the `Formula` class.
+- New OLL algorithm for OpenWBO for more efficient weighted MaxSAT solving.
+- Two overloaded factory methods `mk` in `MiniSat` to construct a solver by formula factory, solver style and optional configuration.
+- Methods to directly apply Boolean functions on BDDs
+- Added `toFormula` method on BDDs to generate a formula via Shannon expansion
+- Convenience methods `variables(Collection<String> names)` and `variables(String... names)` for creating a list of variables in the `FormulaFactory` class.
+
+### Changed
+
+- Methods `generateFromCnf(Formula formula)` and `generateFromCnf(Collection<Formula> formulas)` in `ConstraintGraphGenerator` are now deprecated, since the
+  constraint graph generation is not CNF specific. Both methods will be removed with LogicNG 3.0. Instead, use the general
+  method `generateFromFormulas(Collection<Formula> formulas)`.
+
 ## [2.3.2] - 2022-08-02
 
 ### Changed

README.md

@@ -34,7 +34,7 @@ LogicNG is released in the Maven Central Repository. To include it just add
 <dependency>
   <groupId>org.logicng</groupId>
   <artifactId>logicng</artifactId>
-  <version>2.3.2</version>
+  <version>2.4.0</version>
 </dependency>
 ```
 

pom.xml

@@ -26,7 +26,7 @@
   <modelVersion>4.0.0</modelVersion>
   <groupId>org.logicng</groupId>
   <artifactId>logicng</artifactId>
-  <version>2.3.2</version>
+  <version>2.4.0</version>
   <packaging>bundle</packaging>
 
   <name>LogicNG</name>
@@ -76,18 +76,18 @@
 
     <!-- Dependency Versions -->
     <version.antlr>4.9.3</version.antlr>
-    <version.junit>5.6.2</version.junit>
-    <version.assertj>3.16.1</version.assertj>
-    <version.mockito>3.11.2</version.mockito>
+    <version.junit>5.9.0</version.junit>
+    <version.assertj>3.23.1</version.assertj>
+    <version.mockito>4.7.0</version.mockito>
 
     <!-- Plugin Versions -->
     <version.antlr-plugin>4.9.3</version.antlr-plugin>
-    <version.jacoco>0.8.5</version.jacoco>
+    <version.jacoco>0.8.8</version.jacoco>
     <version.coveralls>4.3.0</version.coveralls>
-    <version.surefire>3.0.0-M5</version.surefire>
+    <version.surefire>3.0.0-M7</version.surefire>
     <version.nexus-staging>1.6.8</version.nexus-staging>
     <version.maven-gpg>1.6</version.maven-gpg>
-    <version.osgi-plugin>5.1.6</version.osgi-plugin>
+    <version.osgi-plugin>5.1.8</version.osgi-plugin>
     <version.maven-source>3.2.1</version.maven-source>
     <version.maven-javadoc>3.2.0</version.maven-javadoc>
     <version.maven-jar>3.2.0</version.maven-jar>
@@ -384,3 +384,4 @@
     </profile>
   </profiles>
 </project>
+

src/main/java/org/logicng/formulas/Formula.java

@@ -44,14 +44,17 @@
 import org.logicng.predicates.CNFPredicate;
 import org.logicng.predicates.DNFPredicate;
 import org.logicng.predicates.NNFPredicate;
+import org.logicng.predicates.satisfiability.ContradictionPredicate;
+import org.logicng.predicates.satisfiability.SATPredicate;
+import org.logicng.predicates.satisfiability.TautologyPredicate;
 import org.logicng.transformations.NNFTransformation;
 
 import java.util.SortedSet;
 import java.util.stream.Stream;
 
 /**
  * Super class for formulas.
- * @version 2.3.0
+ * @version 2.4.0
  * @since 1.0
  */
 public abstract class Formula implements Iterable<Formula> {
@@ -267,6 +270,78 @@ public Formula cnf() {
         return this.f.cnfEncoder().encode(this);
     }
 
+    /**
+     * Returns whether this formula is satisfiable.
+     * A new SAT solver is used to check the satisfiability. This is a convenience method for the
+     * predicate {@link org.logicng.predicates.satisfiability.SATPredicate}. If you want to
+     * have more influence on the solver (e.g. which solver type or configuration) you must create and
+     * use a {@link org.logicng.solvers.SATSolver} on your own.
+     * @return {@code true} when this formula is satisfiable, {@code false} otherwise
+     */
+    public boolean isSatisfiable() {
+        return this.holds(new SATPredicate(this.f));
+    }
+
+    /**
+     * Returns whether this formula is a tautology, hence always true.
+     * A new SAT solver is used to check the tautology. This is a convenience method for the
+     * predicate {@link org.logicng.predicates.satisfiability.TautologyPredicate}. If you want to
+     * have more influence on the solver (e.g. which solver type or configuration) you must create and
+     * use a {@link org.logicng.solvers.SATSolver} on your own.
+     * @return {@code true} when this formula is a tautology, {@code false} otherwise
+     */
+    public boolean isTautology() {
+        return this.holds(new TautologyPredicate(this.f));
+    }
+
+    /**
+     * Returns whether this formula is a contradiction, hence always false.
+     * A new SAT solver is used to check the contradiction. This is a convenience method for the
+     * predicate {@link org.logicng.predicates.satisfiability.ContradictionPredicate}. If you want to
+     * have more influence on the solver (e.g. which solver type or configuration) you must create and
+     * use a {@link org.logicng.solvers.SATSolver} on your own.
+     * @return {@code true} when this formula is a contradiction, {@code false} otherwise
+     */
+    public boolean isContradiction() {
+        return this.holds(new ContradictionPredicate(this.f));
+    }
+
+    /**
+     * Returns whether this formula implies the given other formula, i.e. `this =&gt; other` is a tautology.
+     * A new SAT solver is used to check this tautology. This is a convenience method. If you want to
+     * have more influence on the solver (e.g. which solver type or configuration) you must create and
+     * use a {@link org.logicng.solvers.SATSolver} on your own.
+     * @param other the formula which should be checked if it is implied by this formula
+     * @return {@code true} when this formula implies the given other formula, {@code false} otherwise
+     */
+    public boolean implies(final Formula other) {
+        return this.f.implication(this, other).holds(new TautologyPredicate(this.f));
+    }
+
+    /**
+     * Returns whether this formula is implied by the given other formula, i.e. `other =&gt; this` is a tautology.
+     * A new SAT solver is used to check this tautology. This is a convenience method. If you want to
+     * have more influence on the solver (e.g. which solver type or configuration) you must create and
+     * use a {@link org.logicng.solvers.SATSolver} on your own.
+     * @param other the formula which should be checked if it implies this formula
+     * @return {@code true} when this formula is implied by the given other formula, {@code false} otherwise
+     */
+    public boolean isImpliedBy(final Formula other) {
+        return this.f.implication(other, this).holds(new TautologyPredicate(this.f));
+    }
+
+    /**
+     * Returns whether this formula is equivalent to the given other formula, i.e. `other &lt;=&gt; this` is a tautology.
+     * A new SAT solver is used to check this tautology. This is a convenience method. If you want to
+     * have more influence on the solver (e.g. which solver type or configuration) you must create and
+     * use a {@link org.logicng.solvers.SATSolver} on your own.
+     * @param other the formula which should be checked if it is equivalent with this formula
+     * @return {@code true} when this formula is equivalent to the given other formula, {@code false} otherwise
+     */
+    public boolean isEquivalentTo(final Formula other) {
+        return this.f.equivalence(this, other).holds(new TautologyPredicate(this.f));
+    }
+
     /**
      * Generates a BDD from this formula with a given variable ordering.  This is done by generating a new BDD factory,
      * generating the variable order for this formula, and building a new BDD.  If more sophisticated operations should

src/main/java/org/logicng/formulas/FormulaFactory.java

@@ -59,6 +59,7 @@
 import org.logicng.util.FormulaRandomizerConfig;
 import org.logicng.util.Pair;
 
+import java.util.ArrayList;
 import java.util.Arrays;
 import java.util.Collection;
 import java.util.Collections;
@@ -79,7 +80,7 @@
  * <p>
  * A formula factory is NOT thread-safe.  If you generate formulas from more than one thread you either need to synchronize the formula factory
  * yourself or you use a formula factory for each single thread.
- * @version 2.3.2
+ * @version 2.4.0
  * @since 1.0
  */
 public class FormulaFactory {
@@ -909,6 +910,32 @@ public Variable variable(final String name) {
         return var;
     }
 
+    /**
+     * Creates a list of literals with the given names and positive phase.
+     * @param names the variable names
+     * @return a new list of literals with the given names and positive phase
+     */
+    public List<Variable> variables(final Collection<String> names) {
+        final List<Variable> variables = new ArrayList<>();
+        for (final String name : names) {
+            variables.add(variable(name));
+        }
+        return variables;
+    }
+
+    /**
+     * Creates a list of literals with the given names and positive phase.
+     * @param names the variable names
+     * @return a new list of literals with the given names and positive phase
+     */
+    public List<Variable> variables(final String... names) {
+        final List<Variable> variables = new ArrayList<>();
+        for (final String name : names) {
+            variables.add(variable(name));
+        }
+        return variables;
+    }
+
     /**
      * Creates a new pseudo-Boolean constraint.
      * @param comparator   the comparator of the constraint

src/main/java/org/logicng/graphs/generators/ConstraintGraphGenerator.java

@@ -37,7 +37,7 @@
 /**
  * A graph generator which generates a constraint graph for a
  * given list of formulas.
- * @version 2.0.0
+ * @version 2.4.0
  * @since 2.0.0
  */
 public final class ConstraintGraphGenerator {
@@ -53,7 +53,9 @@ private ConstraintGraphGenerator() {
      * Constructs the constraint graph.
      * @param formula the formula in extended CNF
      * @return the constraint graph for the given formula
+     * @deprecated the constraint graph generation is not CNF specific. Use general method {@link #generateFromFormulas(Collection)} instead.
      */
+    @Deprecated
     public static Graph<Variable> generateFromCnf(final Formula formula) {
         final Graph<Variable> constraintGraph = new Graph<>();
         addToGraph(formula, constraintGraph);
@@ -64,7 +66,9 @@ public static Graph<Variable> generateFromCnf(final Formula formula) {
      * Constructs the constraint graph.
      * @param formulas the formulas in extended CNF as set of CNFs
      * @return the constraint graph for the given formula
+     * @deprecated the constraint graph generation is not CNF specific. Use general method {@link #generateFromFormulas(Collection)} instead.
      */
+    @Deprecated
     public static Graph<Variable> generateFromCnf(final Collection<Formula> formulas) {
         final Graph<Variable> constraintGraph = new Graph<>();
         for (final Formula clause : formulas) {

src/main/java/org/logicng/graphs/io/GraphDimacsFileWriter.java

@@ -45,11 +45,14 @@
 
 /**
  * A dimacs file writer for graphs.  Writes the internal data structure of a graph to a dimacs file.
- * @version 1.2
+ * @version 2.4.0
  * @since 1.2
  */
 public final class GraphDimacsFileWriter {
 
+    private static final String COL_EXTENSION = ".col";
+    private static final String MAP_EXTENSION = ".map";
+
     /**
      * Private constructor.
      */
@@ -59,24 +62,24 @@ private GraphDimacsFileWriter() {
 
     /**
      * Writes a given graph's internal data structure as a dimacs file.
-     * @param fileName     the file name of the dimacs file to write
-     * @param g            the graph
+     * @param fileName     the file name of the dimacs file to write, will be extended by suffix {@code .col} if not already present
+     * @param graph        the graph
      * @param writeMapping indicates whether an additional file for translating the ids to variable names shall be written
      * @param <T>          the type of the graph content
      * @throws IOException if there was a problem writing the file
      */
-    public static <T> void write(final String fileName, final Graph<T> g, final boolean writeMapping) throws IOException {
-        final File file = new File(fileName.endsWith(".col") ? fileName : fileName + ".col");
+    public static <T> void write(final String fileName, final Graph<T> graph, final boolean writeMapping) throws IOException {
+        final File file = new File(fileName.endsWith(COL_EXTENSION) ? fileName : fileName + COL_EXTENSION);
         final Map<Node<T>, Long> node2id = new LinkedHashMap<>();
         long i = 1;
-        for (final Node<T> node : g.nodes()) {
+        for (final Node<T> node : graph.nodes()) {
             node2id.put(node, i++);
         }
 
         final StringBuilder sb = new StringBuilder("p edge ");
         final Set<Pair<Node<T>, Node<T>>> edges = new LinkedHashSet<>();
         final Set<Node<T>> doneNodes = new LinkedHashSet<>();
-        for (final Node<T> d : g.nodes()) {
+        for (final Node<T> d : graph.nodes()) {
             for (final Node<T> n : d.neighbours()) {
                 if (!doneNodes.contains(n)) {
                     edges.add(new Pair<>(d, n));
@@ -95,7 +98,7 @@ public static <T> void write(final String fileName, final Graph<T> g, final bool
             writer.flush();
         }
         if (writeMapping) {
-            final String mappingFileName = (fileName.endsWith(".col") ? fileName.substring(0, fileName.length() - 4) : fileName) + ".map";
+            final String mappingFileName = (fileName.endsWith(COL_EXTENSION) ? fileName.substring(0, fileName.length() - 4) : fileName) + MAP_EXTENSION;
             writeMapping(new File(mappingFileName), node2id);
         }
     }

src/main/java/org/logicng/graphs/io/GraphDotFileWriter.java

@@ -29,24 +29,24 @@
 package org.logicng.graphs.io;
 
 import org.logicng.graphs.datastructures.Graph;
-import org.logicng.graphs.datastructures.Node;
+import org.logicng.io.graphical.GraphicalDotWriter;
+import org.logicng.io.graphical.generators.GraphGraphicalGenerator;
 
-import java.io.BufferedWriter;
 import java.io.File;
 import java.io.IOException;
-import java.io.OutputStreamWriter;
-import java.nio.charset.StandardCharsets;
-import java.nio.file.Files;
-import java.util.LinkedHashSet;
-import java.util.Set;
 
 /**
- * A dot file writer for a graph.  Writes the internal data structure of the formula to a dot file.
- * @version 2.0.0
+ * A dot file writer for a graph.  Writes the internal data structure of the graph to a dot file.
+ * @version 2.4.0
  * @since 1.2
+ * @deprecated This legacy writer will be removed in LogicNG 3.0.0.  For a more configurable and flexible
+ * to use graph writer use {@link GraphGraphicalGenerator} within the new graphical writer framework.
  */
+@Deprecated
 public final class GraphDotFileWriter {
 
+    private static final String DOT_EXTENSION = ".dot";
+
     /**
      * Private constructor.
      */
@@ -55,14 +55,14 @@ private GraphDotFileWriter() {
     }
 
     /**
-     * Writes a given formula's internal data structure as a dimacs file.
-     * @param fileName the file name of the dimacs file to write
+     * Writes a given graph's internal data structure as a dot file.
+     * @param fileName the file name of the dot file to write, will be extended by suffix {@code .dot} if not already present
      * @param graph    the graph
      * @param <T>      the type of the graph content
      * @throws IOException if there was a problem writing the file
      */
     public static <T> void write(final String fileName, final Graph<T> graph) throws IOException {
-        write(new File(fileName.endsWith(".dot") ? fileName : fileName + ".dot"), graph);
+        write(new File(fileName.endsWith(DOT_EXTENSION) ? fileName : fileName + DOT_EXTENSION), graph);
     }
 
     /**
@@ -73,27 +73,6 @@ public static <T> void write(final String fileName, final Graph<T> graph) throws
      * @throws IOException if there was a problem writing the file
      */
     public static <T> void write(final File file, final Graph<T> graph) throws IOException {
-        final StringBuilder sb = new StringBuilder(String.format("strict graph {%n"));
-
-        final Set<Node<T>> doneNodes = new LinkedHashSet<>();
-        for (final Node<T> d : graph.nodes()) {
-            for (final Node<T> n : d.neighbours()) {
-                if (!doneNodes.contains(n)) {
-                    sb.append("  ").append(d.content()).append(" -- ").append(n.content()).append(System.lineSeparator());
-                }
-            }
-            doneNodes.add(d);
-        }
-        for (final Node<T> d : graph.nodes()) {
-            if (d.neighbours().isEmpty()) {
-                sb.append("  ").append(d.content()).append(System.lineSeparator());
-            }
-        }
-        sb.append("}");
-
-        try (final BufferedWriter writer = new BufferedWriter(new OutputStreamWriter(Files.newOutputStream(file.toPath()), StandardCharsets.UTF_8))) {
-            writer.append(sb);
-            writer.flush();
-        }
+        GraphGraphicalGenerator.<T>builder().build().translate(graph).write(file, GraphicalDotWriter.get());
     }
 }