merge dev_lcg into master

Author: cprudhom

.github/workflows/maven-test.yml

@@ -19,7 +19,7 @@ jobs:
           java-version: '11'
           distribution: 'temurin'
           cache: 'maven'
-        
+
       # Install Ibex
       - name: Install ibex
         run: |
@@ -28,14 +28,14 @@ jobs:
       # Regression tests
       - name: Test Ibex
         run: mvn --file pom.xml test -Pcoverage -DtestFailureIgnore=true -Dgroups=ibex
-  
+
   test-solver:
     runs-on: ubuntu-latest
     # Tests matrix
     strategy:
       #fail-fast: false
       matrix:
-        group: [ "1s", "10s", "checker" ]
+        group: [ "1s", "10s", "checker", "lcg" ]
 
     # The different steps
     steps:
@@ -52,7 +52,7 @@ jobs:
       # Regression tests
       - name: Test ${{ matrix.group }}
         run: mvn --file pom.xml test -Pcoverage -DtestFailureIgnore=true -Dgroups=${{ matrix.group }}
-        
+
   test-parser:
     needs: [ test-solver ]
     runs-on: ubuntu-latest

CHANGES.md

@@ -4,6 +4,39 @@ Choco Solver ChangeLog
 This file is dedicated to sum up the new features added and bugs fixed in Choco-solver since the version, 4.0.0.
 **Note**: double-space is replaced by "\t" character on release process. Make sure the format is ok.
 
+5.0.0-beta.1 - 17 Feb 2025
+--------------------------
+
+### Major features:
+
+This version introduces CP-SAT in Choco-solver which 
+replaces the previous explanation framework.
+The Lazy Clause Generation (LCG) is a technique that allows the solver to generate clauses during search.
+The current implementation is inspired by Chuffed 
+and "Lazy Clause Generation Reengineered" - Feydy, T., Stuckey, P.J. (2009).
+This new version has necessitated a rather intrusive revision of the way propagators filter.                                         
+
+By default, LCG is not enabled. The following code shows how to enable it:
+```java
+Model model = new Model(Settings.init().setLCG(true));
+```
+
+At this stage, this is a [beta version](https://github.com/orgs/chocoteam/projects/1).
+First, only integer and boolean variables are supported. 
+Second, some constraints are explained with dedicated functions and 
+others are decomposed into explained ones.
+More importantly, others are neither explained nor decomposed (for the moment). 
+In the latter case, an exception is raised to inform the user of the situation. 
+
+
+### Other closed issues and pull requests:
+See [milestone 5.0.0](https://github.com/chocoteam/choco-solver/milestone/40)
+
+#### Contributors to this release:
+- [Charles Prud'homme](https://github.com/cprudhom) (@cprudhom)
+
+**Full Changelog**: https://github.com/chocoteam/choco-solver/compare/v4.10.18...v5.0.0-beta.1
+
 4.10.18 - 27 Jan 2025
 ---------------------
 
@@ -16,23 +49,6 @@ This file is dedicated to sum up the new features added and bugs fixed in Choco-
 
 **Full Changelog**: https://github.com/chocoteam/choco-solver/compare/v4.10.17...v4.10.18
 
-4.10.17 - 23 Sep 2024
- -------------------
- 
- ### Hotfix
- - Fix bug in `PropHybridTable` (#1102)
- 
- **Full Changelog**: https://github.com/chocoteam/choco-solver/compare/v4.10.16...v4.10.17
-
-4.10.16 - 12 Sep 2024
--------------------
-
-### Hotfix
-- Fix bug in `IntAffineView` (#1101)
-
-**Full Changelog**: https://github.com/chocoteam/choco-solver/compare/v4.10.15...v4.10.16
-
-
 4.10.17 - 23 Sep 2024
 -------------------
 

Makefile

@@ -2,7 +2,8 @@
 # like running test suites
 
 ROOT_DIR := $(shell dirname $(realpath $(lastword $(MAKEFILE_LIST))))
-DATE := $(shell date +'%y%m%d_%H:%M')
+PRETTY_DATE := $(shell date +'%m/%d/%Y %H:%M')
+DATE := $(shell date +'%y%m%d_%H%M')
 CURRENT_VERSION := $(shell mvn help:evaluate -Dexpression=project.version | grep -v "\[INFO\]" | grep -v "\[WARNING\]")
 
 .PHONY: all clean compile tests 1s 10s ibex checker mzn xcsp mps dimacs expl update_date compet msc delmsc help
@@ -25,6 +26,7 @@ help:
 	@echo "  mps        			to run all tests with mps"
 	@echo "  dimacs     			to run all tests with dimacs"
 	@echo "  expl       			to run all tests with expl"
+	@echo "  lcg       				to run all tests with lcg"
 	@echo "  update_date 			to update the date in the parsers"
 	@echo "  compet     			to update the date, clean and package the project"
 	@echo "  msc        			for MiniZincIDE, to install the msc file in ~/.minizinc/solvers"
@@ -45,23 +47,23 @@ clean:
 compile:
 	mvn -q compile -DskipTests
 
-tests : 1s 10s ibex checker mzn xcsp mps dimacs expl
+tests : 1s 10s ibex checker mzn xcsp mps dimacs expl lcg
 
-1s 10s ibex checker mzn xcsp mps dimacs : compile
+1s 10s ibex checker mzn xcsp mps dimacs lcg: compile
 	mvn -q test -DtestFailureIgnore=true -Dgroups="$@"
 
 update_date:
-	@sed -i '' 's|            System.out.println("c Choco .*|            System.out.println("c Choco $(DATE)");|' parsers/src/main/java/org/chocosolver/parser/xcsp/XCSP.java
-	@sed -i '' 's|            System.out.println("%% Choco .*|            System.out.println("%% Choco $(DATE)");|' parsers/src/main/java/org/chocosolver/parser/flatzinc/Flatzinc.java
+	@sed -i '' 's|\s*System.out.printf("c Choco.*|System.out.printf("c Choco%s ($(PRETTY_DATE))\\n", lcg? " with LCG" : "");|' parsers/src/main/java/org/chocosolver/parser/xcsp/XCSP.java
+	@sed -i '' 's|\s*System.out.printf("%% Choco%s (.*|System.out.printf("%% Choco%s ($(PRETTY_DATE))\\n", lcg? " with LCG" : "");|' parsers/src/main/java/org/chocosolver/parser/flatzinc/Flatzinc.java
 
 compet: update_date clean package
 
 msc: compet
-	@sed -i '' 's|  "version": .*|  "version" : "$(CURRENT_VERSION)",|' parsers/src/main/minizinc/choco.msc
+	@sed -i '' 's|  "version" : .*|  "version" : "$(CURRENT_VERSION)",|' parsers/src/main/minizinc/choco.msc
 	@sed -i '' 's|SNAPSHOT|$(DATE)|g' parsers/src/main/minizinc/choco.msc
-	@sed -i '' 's|  "mznlib": .*|  "mznlib" : "$(ROOT_DIR)/parsers/src/main/minizinc/mzn_lib/",|' parsers/src/main/minizinc/choco.msc
-	@sed -i '' 's|  "executable": .*|  "executable" : "$(ROOT_DIR)/parsers/src/main/minizinc/fzn-choco",|' parsers/src/main/minizinc/choco.msc
-	@sed -i '' 's|^[^ ]*CHOCO_JAR=.*|CHOCO_JAR=$(ROOT_DIR)/parsers/target/choco-parsers-$(CURRENT_VERSION)-light.jar|' parsers/src/main/minizinc/fzn-choco
+	@sed -i '' 's|  "mznlib" : .*|  "mznlib" : "$(ROOT_DIR)/parsers/src/main/minizinc/mzn_lib/",|' parsers/src/main/minizinc/choco.msc
+	@sed -i '' 's|  "executable" : .*|  "executable" : "$(ROOT_DIR)/parsers/src/main/minizinc/fzn-choco",|' parsers/src/main/minizinc/choco.msc
+	@sed -i '' 's|^[^ ]*JAR_FILE=.*|JAR_FILE="$(ROOT_DIR)/parsers/target/choco-parsers-$(CURRENT_VERSION)-light.jar"|' parsers/src/main/minizinc/fzn-choco.py
 	@cp $(ROOT_DIR)/parsers/src/main/minizinc/choco.msc ~/.minizinc/solvers/choco-$(CURRENT_VERSION)-$(DATE).msc
 
 delmsc:

README.md

@@ -17,7 +17,7 @@
 
 Choco-solver is an open-source Java library for Constraint Programming.
 
-Current stable version is 4.10.18 (27 Jan 2025).
+Current stable version is 5.0.0-beta.1 (17 Feb 2025).
 
 Choco-solver comes with:
 - various type of variables (integer, boolean, set, graph and real),
@@ -124,7 +124,7 @@ So you only have to edit your `pom.xml` to declare the following library depende
 <dependency>
    <groupId>org.choco-solver</groupId>
    <artifactId>choco-solver</artifactId>
-   <version>4.10.18</version>
+   <version>5.0.0-beta.1</version>
 </dependency>
 ```
 

examples/pom.xml

@@ -17,7 +17,7 @@
   <parent>
     <groupId>org.choco-solver</groupId>
     <artifactId>choco</artifactId>
-    <version>4.10.18</version>
+    <version>5.0.0-beta.1</version>
   </parent>
   <artifactId>examples</artifactId>
   <packaging>jar</packaging>

examples/src/test/java/org/chocosolver/examples/integer/KnapsackTest.java

@@ -120,7 +120,7 @@ public void testALL10() throws IOException, SetUpException {
             ks.solveIt(s, true);
             Assert.assertEquals(s.getSolver().getBestSolutionValue().intValue(), 1078, "obj val");
             Assert.assertEquals(s.getSolver().getSolutionCount(), 1, "nb sol");
-            Assert.assertEquals(s.getSolver().getNodeCount(), 18, "nb nod");
+            Assert.assertEquals(s.getSolver().getNodeCount(), 3, "nb nod");
         }
     }
 
@@ -130,8 +130,8 @@ public void testOPT13() throws IOException, SetUpException {
         Model s = ks.modelIt("k20", 13);
         ks.solveIt(s, true);
         Assert.assertEquals(s.getSolver().getBestSolutionValue().intValue(), 2657, "obj val");
-        Assert.assertEquals(s.getSolver().getSolutionCount(), 1, "nb sol");
-        Assert.assertEquals(s.getSolver().getNodeCount(), 18, "nb nod");
+        Assert.assertEquals(s.getSolver().getSolutionCount(), 3, "nb sol");
+        Assert.assertEquals(s.getSolver().getNodeCount(), 60, "nb nod");
     }
 
     @Test(groups = "1s", timeOut = 60000)
@@ -141,7 +141,7 @@ public void testOPT14() throws IOException, SetUpException {
         ks.solveIt(s, true);
         Assert.assertEquals(s.getSolver().getBestSolutionValue().intValue(), 2657, "obj val");
         Assert.assertEquals(s.getSolver().getSolutionCount(), 1, "nb sol");
-        Assert.assertEquals(s.getSolver().getNodeCount(), 26, "nb nod");
+        Assert.assertEquals(s.getSolver().getNodeCount(), 30, "nb nod");
     }
 
     @Test(groups = "1s", timeOut = 60000)
@@ -151,7 +151,7 @@ public void testOPT15() throws IOException, SetUpException {
         ks.solveIt(s, true);
         Assert.assertEquals(s.getSolver().getBestSolutionValue().intValue(), 2657, "obj val");
         Assert.assertEquals(s.getSolver().getSolutionCount(), 1, "nb sol");
-        Assert.assertEquals(s.getSolver().getNodeCount(), 29, "nb nod");
+        Assert.assertEquals(s.getSolver().getNodeCount(), 47, "nb nod");
     }
 
 }

parsers/pom.xml

@@ -17,7 +17,7 @@
     <parent>
         <groupId>org.choco-solver</groupId>
         <artifactId>choco</artifactId>
-        <version>4.10.18</version>
+        <version>5.0.0-beta.1</version>
     </parent>
     <artifactId>choco-parsers</artifactId>
     <packaging>jar</packaging>

parsers/src/main/java/org/chocosolver/parser/RegParser.java

@@ -18,7 +18,6 @@
 import org.chocosolver.solver.ParallelPortfolio;
 import org.chocosolver.solver.Settings;
 import org.chocosolver.solver.Solver;
-import org.chocosolver.solver.learn.XParameters;
 import org.chocosolver.solver.search.strategy.BlackBoxConfigurator;
 import org.chocosolver.solver.search.strategy.Search;
 import org.chocosolver.solver.search.strategy.SearchParams;
@@ -169,15 +168,15 @@ public abstract class RegParser implements IParser {
     @Option(name = "-seed", usage = "Set the seed for random number generator. ")
     protected long seed = 0L;
 
-    @Option(name = "-exp", usage = "Plug explanation in (default: false).")
-    public boolean exp = false;
-
-    @Option(name = "-dfx", usage = "Force default explanation algorithm.")
-    public boolean dftexp = false;
-
     @Option(name = "--cp-profiler", usage = "Connect to CP-Profiler. Two comma-separated values are expected: the execution id and the port.")
     public String cpProfiler = null;
 
+    @Option(name = "-lcg", usage = "Set Lazy Clause Generation (LCG) on. ")
+    protected boolean lcg = false;
+
+    @Option(name = "--disable-shutdown-hook", usage = "Disable the shutdown hook.")
+    protected boolean disableShutdownHook = false;
+
     /**
      * Default settings to apply
      */
@@ -214,7 +213,7 @@ protected RegParser(String parser_cmd) {
     }
 
     public void createSettings() {
-        defaultSettings = Settings.prod();
+        defaultSettings = Settings.prod().setLCG(lcg);
     }
 
     public final Settings getSettings() {
@@ -265,7 +264,9 @@ public final boolean setUp(String... args) throws SetUpException {
             valsel = new SearchParams.ValSelConf(valH, best, bestRate, last);
         }
         createSettings();
-        Runtime.getRuntime().addShutdownHook(statOnKill);
+        if (!disableShutdownHook) {
+            Runtime.getRuntime().addShutdownHook(statOnKill);
+        }
         return true;
     }
 
@@ -301,22 +302,6 @@ public void configureSearch() {
             solver.verboseSolving(1000);
         }
         if (nb_cores == 1) {
-            if (exp) {
-                if (level.isLoggable(Level.INFO)) {
-                    solver.log().white().println("exp is on");
-                }
-                solver.setLearningSignedClauses();
-                // THEN PARAMETERS
-                XParameters.DEFAULT_X = dftexp;
-                XParameters.PROOF = XParameters.FINE_PROOF = false;
-                XParameters.PRINT_CLAUSE = false;
-                XParameters.ASSERT_UNIT_PROP = true; // todo : attention aux clauses globales
-                XParameters.ASSERT_NO_LEFT_BRANCH = false;
-                XParameters.INTERVAL_TREE = true;
-                if (solver.hasObjective()) {
-                    solver.setRestartOnSolutions();
-                }
-            }
             if (free) {
                 freesearch(solver);
             }

parsers/src/main/java/org/chocosolver/parser/flatzinc/Flatzinc.java

@@ -101,10 +101,12 @@ public Flatzinc(boolean all, boolean free, int nb_cores) {
     public void createSettings() {
         defaultSettings = Settings.prod()
                 .setMinCardinalityForSumDecomposition(256)
-                .setLearntClausesDominancePerimeter(0)
-                .setNbMaxLearntClauses(Integer.MAX_VALUE)
-                .setRatioForClauseStoreReduction(.66f)
-                .set("adhocReification", true);
+                .setLCG(lcg)
+                .setNbMaxLearntClauses(100_000)
+                //.setIntVarLazyLitWithWeakBounds(false)
+                .set("adhocReification", true)
+                .setWarnUser(false)
+        ;
     }
 
     @Override
@@ -126,7 +128,7 @@ public Thread actionOnKill() {
     @Override
     public void createSolver() {
         if (level.isLoggable(Level.COMPET)) {
-            System.out.println("%% Choco 250127_16:13");
+            System.out.printf("%% Choco-solver%s (5.0.0-beta.1, 250217_17:45)\n", lcg? " with LCG" : "");
         }
         super.createSolver();
         datas = new Datas[nb_cores];