Update doc

content/en/docs/Advanced usages/Explanations.md

@@ -0,0 +1,94 @@
+---
+title: "Explanations"
+date: 2020-01-07T16:06:55+01:00
+weight: 55
+math: "true"
+description: >
+  Using explanations.
+---
+
+Choco-solver natively support explanations. 
+However, no explanation engine is plugged-in by default.
+
+### Principle
+
+Nogoods and explanations have long been used in various paradigms for improving search.
+An explanation records some sufficient information to justify an inference made by the solver (domain reduction, contradiction, etc.).
+It is made of a subset of the original propagators of the problem and a subset of decisions applied during search.
+Explanations represent the logical chain of inferences made by the solver during propagation in an efficient and usable manner.
+In a way, they provide some kind of a trace of the behavior of the solver as any operation needs to be explained.
+
+The implemented explanation framework is an adapation of the well-konw SAT [CDCL algorithm](https://en.wikipedia.org/wiki/Conflict-driven_clause_learning) to discrete constraint solver.
+By exploiting the implication graph (that records events, i.e. variables’ modifications), this algorithm is able to derive a new constraint from the events that led to a contradiction.
+Once added to the constraint network, this constraint makes possible to “backjump” (non-chronological backtrack) to the appropriate decision in the decision path.
+
+In CP, learned constraints are denoted “signed-clauses” which is a disjunction of signed-literals, i.e. membership unary constraints : $\bigvee_{i=0}^{n}X_i \in D_i$
+where $X_i$ are variables and $D_i$ a set of values.
+A signed-clause is satisfied when at least one signed-literal is satisfied.
+
+The current explanation engine is coded to be *Asynchronous, Reverse, Low-intrusive and Lazy*:
+
+Asynchronous:
+
+    Explanations are not computed during the propagation.
+
+Reverse:
+
+    Explanations are computed in a bottom-up way, from the conflict to the first event generated, *keeping* only relevant events to compute the explanation of the conflict.
+
+Low-intrusive:
+
+    Basically, propagators need to implement only one method to furnish a convenient explanation schema.
+
+Lazy:
+
+    Explanations are computed on request.
+
+To do so, all events are stored during the descent to a conflict/solution, and are then evaluated and kept if relevant, to get the explanation.
+
+{{%alert title="Info"%}}
+In CP, CDCL algorithm requires that each constraint of a problem can be explained. Even though a default explanation function for any constraint, dedicated functions offers better performances.
+In Choco-solver a few set of constraints is equipped with dedicated explanation function (unary constraints, binary and ternary, sum and scalar).
+{{%/alert%}}
+
+
+### Computing explanations
+
+When a contradiction occurs during propagation, it can only be thrown by:
+
+
+* a propagator which detects unsatisfiability, based on the current domain of its variables;
+
+
+* or a variable whom domain became empty.
+
+Consequently, in addition to causes, variables can also explain the current state of their domain.
+Computing the explanation of a failure consists in going up in the stack of all events generated in the current branch of the search tree and filtering the one relative to the conflict.
+The entry point is either the not satisfiable propagator or the empty variable.
+
+Each propagator embeds its own explanation algorithm which relies on the relation it defines over variables.
+
+### Explanations for the system
+
+Explanations for the system, which try to reduce the search space, differ from the ones giving feedback to a user about the unsatisfiability of its model.
+Both rely on the capacity of the explanation engine to motivate a failure, during the search form system explanations and once the search is complete for user ones.
+
+#### Learning signed-clauses
+
+When learning is plugged-in, the search is hacked in the following way.
+On a failure, the implication graph is analyzed in order to build a signed-clause and to define the decision to jump back to it.
+Decisions from the current one to the return decision (excluded) are erased.
+Then, the signed-clause is added to the constraint network and automatically dominates decision refutation; then the search goes on.
+If the explanation jumps back to the root node, the problem is proven to have no solution and search stops.
+
+**API**:
+
+```java
+solver.setLearningSignedClauses();
+```
+
+
+* *solver*: the solver to explain.
+
+See Settings to configure learning algorithm.
+

content/en/docs/Advanced usages/Ibex.md

@@ -0,0 +1,29 @@
+---
+title: "Ibex"
+date: 2020-01-07T16:06:55+01:00
+weight: 56
+math: "true"
+description: >
+  Using Ibex.
+---
+
+To manage continuous constraints with Choco, an interface with [Ibex](http://www.ibex-lib.org/) has been done.
+It needs this library to be installed on your system.
+
+> “IBEX is a C++ library for constraint processing over real numbers.
+> It provides reliable algorithms for handling non-linear constraints.
+> In particular, round off errors are also taken into account.
+> It is based on interval arithmetic and affine arithmetic.”
+> – [http://www.ibex-lib.org/](http://www.ibex-lib.org/)
+
+### Installing Ibex
+
+See the [installation instructions](http://www.ibex-lib.org/doc/install.html) of Ibex to complied Ibex on your system.
+More specially, take a look at [Installation as a dynamic library](http://www.ibex-lib.org/doc/install.html#installation-as-a-dynamic-library)
+Do not forget to add the `--with-java-package=org.chocosolver.solver.constraints.real` configuration option.
+
+### Using Ibex
+
+Once the installation is completed, the JVM needs to know where Ibex is installed to fully benefit from the Choco-Ibex bridge and declare real variables and constraints.
+This can be done either with an environment variable of by adding `-Djava.library.path=path/to/ibex/lib` to the JVM arguments.
+The path /path/to/ibex/lib points to the lib directory of the Ibex installation directory.

content/en/docs/Advanced usages/to-remove.md → content/en/docs/Advanced usages/Miscellaneous.md

@@ -1,4 +1,90 @@
-# Miscellaneous
+---
+title: "Miscellaneous"
+date: 2020-01-07T16:06:55+01:00
+weight: 57
+math: "true"
+---
+
+### Search monitors
+
+#### Principle
+
+A search monitor is an observer of the resolver.
+It gives user access before and after executing each main step of the solving process:
+
+
+* initialize: when the solving process starts and the initial propagation is run,
+
+
+* open node: when a decision is computed,
+
+
+* down branch: on going down in the tree search applying or refuting a decision,
+
+
+* up branch: on going up in the tree search to reconsider a decision,
+
+
+* solution: when a solution is got,
+
+
+* restart search: when the search is restarted to a previous node, commonly the root node,
+
+
+* close: when the solving process ends,
+
+
+* contradiction: on a failure,
+
+With the accurate search monitor, one can easily observe with the resolver, from pretty printing of a solution to learning nogoods from restart, or many other actions.
+
+The interfaces to implement are:
+
+
+* `IMonitorInitialize`,
+
+
+* `IMonitorOpenNode`,
+
+
+* `IMonitorDownBranch`,
+
+
+* `IMonitorUpBranch`,
+
+
+* `IMonitorSolution`,
+
+
+* `IMonitorRestart`,
+
+
+* `IMonitorContradiction`,
+
+
+* `IMonitorClose`.
+
+Most of them gives the opportunity to do something before and after a step. The other ones are called after a step.
+
+Simple example to print every solution:
+
+```
+Solver s = model.getSolver();
+s.plugMonitor(new IMonitorSolution() {
+    @Override
+    public void onSolution() {
+        System.out.println("x = "+x.getValue());
+    }
+});
+```
+
+In Java 8 style:
+
+```
+Solver s = model.getSolver();
+s.plugMonitor((IMonitorSolution) () -> {System.out.println("x = "+x.getValue());});
+```
+
 
 ## Settings
 
@@ -38,26 +124,3 @@ choco-gui is an extension of Choco 4.
 It provides a Graphical User Interface with various views which can be simply plugged on any Choco Model object.
 You will find it at [https://github.com/chocoteam/choco-gui](https://github.com/chocoteam/choco-gui)
 
-## Ibex Solver
-
-To manage continuous constraints with Choco, an interface with Ibex has been done.
-It needs Ibex to be installed on your system.
-
-> “IBEX is a C++ library for constraint processing over real numbers.
-
-> It provides reliable algorithms for handling non-linear constraints.
-> In particular, round off errors are also taken into account.
-> It is based on interval arithmetic and affine arithmetic.”
-> – [http://www.ibex-lib.org/](http://www.ibex-lib.org/)
-
-### Installing Ibex
-
-See the [installation instructions](http://www.ibex-lib.org/doc/install.html) of Ibex to complied Ibex on your system.
-More specially, take a look at [Installation as a dynamic library](http://www.ibex-lib.org/doc/install.html#installation-as-a-dynamic-library)
-Do not forget to add the `--with-java-package=org.chocosolver.solver.constraints.real` configuration option.
-
-### Using Ibex
-
-Once the installation is completed, the JVM needs to know where Ibex is installed to fully benefit from the Choco-Ibex bridge and declare real variables and constraints.
-This can be done either with an environment variable of by adding `-Djava.library.path=path/to/ibex/lib` to the JVM arguments.
-The path /path/to/ibex/lib points to the lib directory of the Ibex installation directory.

content/en/docs/Advanced usages/Propagator.md

@@ -12,26 +12,32 @@ description: >
 
 You can create your own constraint by creating a generic `Constraint` object with the appropriate propagator:
 
-```
+```java
 Constraint c = new Constraint("MyConstraint", new MyPropagator(vars));
 ```
 
 The only tricky part relies in the propagator implementation.
 Your propagator must extend the `Propagator` class but, at the begining, not all methods have to be overwritted.
 We will see two ways to implement a propagator ensuring that `X >= Y`.
 
+A guided implementation of a scalar constraint is presented in the tutorial: [Designing a constraint]({{< ref "/tutos/Constraints.md" >}}).
+
 #### Basic propagator
 
 You must at least call the super constructor to specifies the scope (set of variables) of the propagator.
 Then you must implement the two following methods:
 
-`void propagate(int evtmask)`
+```java 
+void propagate(int evtmask)
+```
 
 > This method applies the global filtering algorithm of the propagator, that is, from *scratch*.
 > It is called once during initial propagation (to propagate initial domains) and then during the solving process if
 > the propagator is not incremental. It is the most important method of the propagator.
 
-`isEntailed()`
+```java 
+ESat isEntailed()
+```
 
 > This method checks the current state of the propagator. It is used for constraint reification.
 > It checks whether the propagator will be always satisfied (`ESat.TRUE`), never satisfied (`ESat.FALSE`)
@@ -45,7 +51,7 @@ but should at least cover the case where all variables are instantiated, in orde
 
 Here is an example of how to implement a propagator for `X >= Y`:
 
-```
+```java
 // Propagator to apply X >= Y
 public class MySimplePropagator extends Propagator<IntVar> {
 
@@ -96,7 +102,7 @@ The method `why(...)` explains the filtering, to allow learning.
 
 Here is an example of how to implement a propagator for `X >= Y`:
 
-```
+```java
 // Propagator to apply X >= Y
 public final class MyIncrementalPropagator extends Propagator<IntVar> {
 
@@ -150,19 +156,6 @@ public final class MyIncrementalPropagator extends Propagator<IntVar> {
             return ESat.UNDEFINED;
     }
 
-    @Override
-    public boolean why(RuleStore ruleStore, IntVar var, IEventType evt, int value) {
-        boolean newrules = ruleStore.addPropagatorActivationRule(this);
-        if (var.equals(x)) {
-            newrules |=ruleStore.addLowerBoundRule(y);
-        } else if (var.equals(y)) {
-            newrules |=ruleStore.addUpperBoundRule(x);
-        } else {
-            newrules |=super.why(ruleStore, var, evt, value);
-        }
-        return newrules;
-    }
-
     @Override
     public String toString() {
         return "prop(" + vars[0].getName() + ".GEQ." + vars[1].getName() + ")";
@@ -202,7 +195,7 @@ The *coarse* option:
 > The propagator does not react to fine events.
 > The coarse filtering algorithm should be surrounded like this:
 
-> ```
+> ```java
 > // In the case of ``SetVar``, replace ``getDomSize()`` by ``getEnvSize()-getKerSize()``.
 > long size;
 > do{