From 10ab16ee1a67329434023906641b9457394bacc4 Mon Sep 17 00:00:00 2001 From: Christoph Zengler Date: Sat, 4 May 2024 12:01:12 +0200 Subject: [PATCH 1/6] Next development version --- pom.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pom.xml b/pom.xml index 6066e06f..c68fd28d 100644 --- a/pom.xml +++ b/pom.xml @@ -26,7 +26,7 @@ 4.0.0 org.logicng logicng - 2.5.0 + 2.5.1-SNAPSHOT bundle LogicNG From b6e69752a8ae694f3ff0d93c9cf8699b9f79fa53 Mon Sep 17 00:00:00 2001 From: Christoph Zengler Date: Sat, 4 May 2024 14:07:20 +0200 Subject: [PATCH 2/6] Preparations for formula and solver serializiation --- .../logicng/collections/LNGBooleanVector.java | 7 ++- .../org/logicng/collections/LNGIntVector.java | 7 ++- .../logicng/collections/LNGLongVector.java | 7 ++- .../datastructures/LNGBoundedIntQueue.java | 16 ++--- .../datastructures/LNGBoundedLongQueue.java | 16 ++--- .../solvers/datastructures/LNGHeap.java | 14 +++-- .../solvers/datastructures/MSClause.java | 8 +-- .../solvers/datastructures/MSVariable.java | 4 +- .../logicng/solvers/sat/GlucoseConfig.java | 52 ++++++++++++++++ .../logicng/solvers/sat/MiniSatConfig.java | 60 +++++++++++++++++++ 10 files changed, 162 insertions(+), 29 deletions(-) diff --git a/src/main/java/org/logicng/collections/LNGBooleanVector.java b/src/main/java/org/logicng/collections/LNGBooleanVector.java index cca8786b..0cf8c14c 100644 --- a/src/main/java/org/logicng/collections/LNGBooleanVector.java +++ b/src/main/java/org/logicng/collections/LNGBooleanVector.java @@ -88,7 +88,12 @@ public LNGBooleanVector(final boolean... elems) { this.size = elems.length; } - LNGBooleanVector(final boolean[] elements, final int size) { + /** + * Creates a vector with the given elements and capacity. + * @param elements the elements + * @param size the capacity of the vector + */ + public LNGBooleanVector(final boolean[] elements, final int size) { this.elements = elements; this.size = size; } diff --git a/src/main/java/org/logicng/collections/LNGIntVector.java b/src/main/java/org/logicng/collections/LNGIntVector.java index c732168b..5f28b027 100644 --- a/src/main/java/org/logicng/collections/LNGIntVector.java +++ b/src/main/java/org/logicng/collections/LNGIntVector.java @@ -88,7 +88,12 @@ public LNGIntVector(final int... elems) { this.size = elems.length; } - LNGIntVector(final int[] elements, final int size) { + /** + * Creates a vector with the given elements and capacity. + * @param elements the elements + * @param size the capacity of the vector + */ + public LNGIntVector(final int[] elements, final int size) { this.elements = elements; this.size = size; } diff --git a/src/main/java/org/logicng/collections/LNGLongVector.java b/src/main/java/org/logicng/collections/LNGLongVector.java index 738bf030..6e05e22d 100644 --- a/src/main/java/org/logicng/collections/LNGLongVector.java +++ b/src/main/java/org/logicng/collections/LNGLongVector.java @@ -88,7 +88,12 @@ public LNGLongVector(final long... elems) { this.size = elems.length; } - LNGLongVector(final long[] elements, final int size) { + /** + * Creates a vector with the given elements and capacity. + * @param elements the elements + * @param size the capacity of the vector + */ + public LNGLongVector(final long[] elements, final int size) { this.elements = elements; this.size = size; } diff --git a/src/main/java/org/logicng/solvers/datastructures/LNGBoundedIntQueue.java b/src/main/java/org/logicng/solvers/datastructures/LNGBoundedIntQueue.java index e9988e6b..83c2b343 100644 --- a/src/main/java/org/logicng/solvers/datastructures/LNGBoundedIntQueue.java +++ b/src/main/java/org/logicng/solvers/datastructures/LNGBoundedIntQueue.java @@ -104,8 +104,8 @@ public LNGBoundedIntQueue() { this.queueSize = 0; } - LNGBoundedIntQueue(final LNGIntVector elems, final int first, final int last, final long sumOfQueue, - final int maxSize, final int queueSize) { + public LNGBoundedIntQueue(final LNGIntVector elems, final int first, final int last, final long sumOfQueue, + final int maxSize, final int queueSize) { this.elems = elems; this.first = first; this.last = last; @@ -164,27 +164,27 @@ private void growTo(final int size) { this.last = 0; } - LNGIntVector getElems() { + public LNGIntVector getElems() { return this.elems; } - int getFirst() { + public int getFirst() { return this.first; } - int getLast() { + public int getLast() { return this.last; } - long getSumOfQueue() { + public long getSumOfQueue() { return this.sumOfQueue; } - int getMaxSize() { + public int getMaxSize() { return this.maxSize; } - int getQueueSize() { + public int getQueueSize() { return this.queueSize; } diff --git a/src/main/java/org/logicng/solvers/datastructures/LNGBoundedLongQueue.java b/src/main/java/org/logicng/solvers/datastructures/LNGBoundedLongQueue.java index 753ccd30..63a1199e 100644 --- a/src/main/java/org/logicng/solvers/datastructures/LNGBoundedLongQueue.java +++ b/src/main/java/org/logicng/solvers/datastructures/LNGBoundedLongQueue.java @@ -104,8 +104,8 @@ public LNGBoundedLongQueue() { this.queueSize = 0; } - LNGBoundedLongQueue(final LNGLongVector elems, final int first, final int last, final long sumOfQueue, - final int maxSize, final int queueSize) { + public LNGBoundedLongQueue(final LNGLongVector elems, final int first, final int last, final long sumOfQueue, + final int maxSize, final int queueSize) { this.elems = elems; this.first = first; this.last = last; @@ -182,27 +182,27 @@ public void fastClear() { this.sumOfQueue = 0; } - LNGLongVector getElems() { + public LNGLongVector getElems() { return this.elems; } - int getFirst() { + public int getFirst() { return this.first; } - int getLast() { + public int getLast() { return this.last; } - long getSumOfQueue() { + public long getSumOfQueue() { return this.sumOfQueue; } - int getMaxSize() { + public int getMaxSize() { return this.maxSize; } - int getQueueSize() { + public int getQueueSize() { return this.queueSize; } diff --git a/src/main/java/org/logicng/solvers/datastructures/LNGHeap.java b/src/main/java/org/logicng/solvers/datastructures/LNGHeap.java index 5b1db19f..cfbb2a8a 100644 --- a/src/main/java/org/logicng/solvers/datastructures/LNGHeap.java +++ b/src/main/java/org/logicng/solvers/datastructures/LNGHeap.java @@ -69,8 +69,14 @@ public LNGHeap(final MiniSatStyleSolver solver) { this.indices = new LNGIntVector(1000); } - LNGHeap(final MiniSatStyleSolver s, final LNGIntVector heap, final LNGIntVector indices) { - this.s = s; + /** + * Constructs a new heap for a given solver and content. + * @param solver the solver + * @param heap the heap content + * @param indices the indices content + */ + public LNGHeap(final MiniSatStyleSolver solver, final LNGIntVector heap, final LNGIntVector indices) { + this.s = solver; this.heap = heap; this.indices = indices; } @@ -258,11 +264,11 @@ private void percolateDown(final int pos) { this.indices.set(y, p); } - LNGIntVector getHeap() { + public LNGIntVector getHeap() { return this.heap; } - LNGIntVector getIndices() { + public LNGIntVector getIndices() { return this.indices; } diff --git a/src/main/java/org/logicng/solvers/datastructures/MSClause.java b/src/main/java/org/logicng/solvers/datastructures/MSClause.java index 1feb20bc..acc4c633 100644 --- a/src/main/java/org/logicng/solvers/datastructures/MSClause.java +++ b/src/main/java/org/logicng/solvers/datastructures/MSClause.java @@ -123,9 +123,9 @@ public MSClause(final LNGIntVector ps, final boolean learnt, final boolean isAtM this.atMostWatchers = -1; } - MSClause(final LNGIntVector data, final boolean learnt, final boolean isAtMost, final double activity, - final int szWithoutSelectors, final boolean seen, final long lbd, final boolean canBeDel, - final boolean oneWatched, final int atMostWatchers) { + public MSClause(final LNGIntVector data, final boolean learnt, final boolean isAtMost, final double activity, + final int szWithoutSelectors, final boolean seen, final long lbd, final boolean canBeDel, + final boolean oneWatched, final int atMostWatchers) { this.data = data; this.learnt = learnt; this.isAtMost = isAtMost; @@ -316,7 +316,7 @@ public int cardinality() { return this.data.size() - this.atMostWatchers + 1; } - LNGIntVector getData() { + public LNGIntVector getData() { return this.data; } diff --git a/src/main/java/org/logicng/solvers/datastructures/MSVariable.java b/src/main/java/org/logicng/solvers/datastructures/MSVariable.java index f7545b0b..249290b9 100644 --- a/src/main/java/org/logicng/solvers/datastructures/MSVariable.java +++ b/src/main/java/org/logicng/solvers/datastructures/MSVariable.java @@ -74,8 +74,8 @@ public MSVariable(final boolean polarity) { this.decision = false; } - MSVariable(final Tristate assignment, final int level, final MSClause reason, final double activity, - final boolean polarity, final boolean decision) { + public MSVariable(final Tristate assignment, final int level, final MSClause reason, final double activity, + final boolean polarity, final boolean decision) { this.assignment = assignment; this.level = level; this.reason = reason; diff --git a/src/main/java/org/logicng/solvers/sat/GlucoseConfig.java b/src/main/java/org/logicng/solvers/sat/GlucoseConfig.java index 626f96a5..26b41ab1 100644 --- a/src/main/java/org/logicng/solvers/sat/GlucoseConfig.java +++ b/src/main/java/org/logicng/solvers/sat/GlucoseConfig.java @@ -81,6 +81,58 @@ public static Builder builder() { return new Builder(); } + public int getLbLBDMinimizingClause() { + return this.lbLBDMinimizingClause; + } + + public int getLbLBDFrozenClause() { + return this.lbLBDFrozenClause; + } + + public int getLbSizeMinimizingClause() { + return this.lbSizeMinimizingClause; + } + + public int getFirstReduceDB() { + return this.firstReduceDB; + } + + public int getSpecialIncReduceDB() { + return this.specialIncReduceDB; + } + + public int getIncReduceDB() { + return this.incReduceDB; + } + + public double getFactorK() { + return this.factorK; + } + + public double getFactorR() { + return this.factorR; + } + + public int getSizeLBDQueue() { + return this.sizeLBDQueue; + } + + public int getSizeTrailQueue() { + return this.sizeTrailQueue; + } + + public boolean isReduceOnSize() { + return this.reduceOnSize; + } + + public int getReduceOnSizeSize() { + return this.reduceOnSizeSize; + } + + public double getMaxVarDecay() { + return this.maxVarDecay; + } + @Override public String toString() { final StringBuilder sb = new StringBuilder("GlucoseConfig{").append(System.lineSeparator()); diff --git a/src/main/java/org/logicng/solvers/sat/MiniSatConfig.java b/src/main/java/org/logicng/solvers/sat/MiniSatConfig.java index 691fc9a1..c3afef8d 100644 --- a/src/main/java/org/logicng/solvers/sat/MiniSatConfig.java +++ b/src/main/java/org/logicng/solvers/sat/MiniSatConfig.java @@ -167,6 +167,66 @@ public boolean isAuxiliaryVariablesInModels() { return this.auxiliaryVariablesInModels; } + public double getVarDecay() { + return this.varDecay; + } + + public double getVarInc() { + return this.varInc; + } + + public ClauseMinimization getClauseMin() { + return this.clauseMin; + } + + public int getRestartFirst() { + return this.restartFirst; + } + + public double getRestartInc() { + return this.restartInc; + } + + public double getClauseDecay() { + return this.clauseDecay; + } + + public boolean isRemoveSatisfied() { + return this.removeSatisfied; + } + + public double getLearntsizeFactor() { + return this.learntsizeFactor; + } + + public double getLearntsizeInc() { + return this.learntsizeInc; + } + + public boolean isIncremental() { + return this.incremental; + } + + public boolean isInitialPhase() { + return this.initialPhase; + } + + public boolean isProofGeneration() { + return this.proofGeneration; + } + + public boolean isBbInitialUBCheckForRotatableLiterals() { + return this.bbInitialUBCheckForRotatableLiterals; + } + + public boolean isBbCheckForComplementModelLiterals() { + return this.bbCheckForComplementModelLiterals; + } + + public boolean isBbCheckForRotatableLiterals() { + return this.bbCheckForRotatableLiterals; + } + @Override public String toString() { final StringBuilder sb = new StringBuilder("MiniSatConfig{").append(System.lineSeparator()); From d77cea2109e1b442edeb24856374e148cae9130e Mon Sep 17 00:00:00 2001 From: Christoph Zengler Date: Fri, 12 Jul 2024 09:43:19 +0200 Subject: [PATCH 3/6] Prepare 2.6.0 release --- pom.xml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pom.xml b/pom.xml index c68fd28d..36e797ed 100644 --- a/pom.xml +++ b/pom.xml @@ -26,7 +26,7 @@ 4.0.0 org.logicng logicng - 2.5.1-SNAPSHOT + 2.6.0-SNAPSHOT bundle LogicNG From 5ba79db0f2149ca4335affbf3c5278817d081998 Mon Sep 17 00:00:00 2001 From: Rouven Walter Date: Mon, 22 Jul 2024 12:55:24 +0200 Subject: [PATCH 4/6] fixed MiniSatConfig doc for default CNF method --- src/main/java/org/logicng/solvers/sat/MiniSatConfig.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/main/java/org/logicng/solvers/sat/MiniSatConfig.java b/src/main/java/org/logicng/solvers/sat/MiniSatConfig.java index c3afef8d..f60a9211 100644 --- a/src/main/java/org/logicng/solvers/sat/MiniSatConfig.java +++ b/src/main/java/org/logicng/solvers/sat/MiniSatConfig.java @@ -406,7 +406,7 @@ public Builder proofGeneration(final boolean proofGeneration) { /** * Sets the CNF method for converting formula which are not in CNF for the solver. The default value - * is {@code FACTORY_CNF}. + * is {@code PG_ON_SOLVER}. * @param cnfMethod the CNF method * @return the builder */ From 9aa1d299d6338e630fa24c0661c50d5e667b02d0 Mon Sep 17 00:00:00 2001 From: Christoph Zengler Date: Wed, 31 Jul 2024 11:06:36 +0200 Subject: [PATCH 5/6] Prepare 2.5.1 release --- CHANGELOG.md | 8 ++++++++ README.md | 2 +- pom.xml | 2 +- 3 files changed, 10 insertions(+), 2 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 9fb1c7d6..40ca17f6 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -2,6 +2,14 @@ LogicNG uses [Semantic Versioning](https://semver.org/spec/v2.0.0.html). +## [2.5.1] - 2024-07-31 + +### Changed + +- Changed visibility from some methods from package-private to public for formula and solver serializiation via the + new https://github.com/logic-ng/serialization library + + ## [2.5.0] - 2024-05-02 ### Removed (Potentially Breaking Change!) diff --git a/README.md b/README.md index 376679a6..9bc07c4b 100644 --- a/README.md +++ b/README.md @@ -34,7 +34,7 @@ LogicNG is released in the Maven Central Repository. To include it just add org.logicng logicng - 2.5.0 + 2.5.1 ``` diff --git a/pom.xml b/pom.xml index 36e797ed..c68fd28d 100644 --- a/pom.xml +++ b/pom.xml @@ -26,7 +26,7 @@ 4.0.0 org.logicng logicng - 2.6.0-SNAPSHOT + 2.5.1-SNAPSHOT bundle LogicNG From 79bb7b0986ff7f2fe73571a6a03216df9fe0fca7 Mon Sep 17 00:00:00 2001 From: Christoph Zengler Date: Wed, 31 Jul 2024 16:33:25 +0200 Subject: [PATCH 6/6] Final 2.5.1 --- pom.xml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/pom.xml b/pom.xml index c68fd28d..70ebfd72 100644 --- a/pom.xml +++ b/pom.xml @@ -26,17 +26,17 @@ 4.0.0 org.logicng logicng - 2.5.1-SNAPSHOT + 2.5.1 bundle LogicNG The Next Generation Logic Library - http://www.logicng.org + https://www.logicng.org The Apache License, Version 2.0 - http://www.apache.org/licenses/LICENSE-2.0.txt + https://www.apache.org/licenses/LICENSE-2.0.txt