Some doc

doc/src/SUMMARY.md

@@ -4,10 +4,9 @@
 [Installation](install.md)
 
 - [Schlandals Modelization](modelization/README.md)
-    - [The Language](modelization/language.md)
-    - [Encoding Bayesian Networks](modelization/bn.md)
-    - [Encoding Probabilistic Graphs](modelization/pg.md)
-    - [Encoding ProbLog Programs](modelization/problog.md)
+    - [Bayesian Networks](modelization/bn.md)
+    - [Probabilistic Graphs](modelization/pg.md)
+    - [ProbLog Programs](modelization/problog.md)
 - [Probabilistic Inference](inference/README.md)
     - [Search solver](inference/search.md)
     - [Compiler](inference/compilation.md)

doc/src/install.md

@@ -1,17 +1,29 @@
 # Installation
 
-Before installing Schlandals, be sure to have [the rust toolchain installed](https://www.rust-lang.org/tools/install)
+Before installing Schlandals, be sure to have [the rust toolchain installed](https://www.rust-lang.org/tools/install).
+
+## From source (recommended)
+
+We assume that the commands are ran from `CURRENT_DIR`
+```bash
+git clone [email protected]:aia-uclouvain/schlandals.git && cd schlandals && cargo build --release
+ln -s $CURRENT_DIR/schlandals/target/release/schlandals $HOME/.local/bin
+```
+This compiles the code in `release` mode (with optimizations included) and add a symbolic links to the local binaries directory.
 
 ## Using Cargo
 
+Note that the code is still actively developed and it should not be expected that the version of the code on crates.io is the most up-to-date.
+The main branch of Schlandals should be stable enough for most use cases.
+
 ```bash
 cargo install schlandals
 ```
 This will put the `schlandals` executable in `~/.cargo/bin/`
 
-## From source
+## Building Schlandals with Torch support
 
-```bash
-git clone git@github.com:aia-uclouvain/schlandals.git && cd schlandals && cargo build --release
-```
-This will put the `schlandals` executable in `schlandals/target/release/`
+Schlandals supports [learning parameters](./learning/README.md) using Torch tensors.
+We use the [tch-rs crate](https://github.com/LaurentMazare/tch-rs) for the bindings with libtorch tensors and this feature can be installed by
+adding `--features tensor` as a flag to the install (`cargo install schlandals --features tensor`) or build (`cargo build --release --features tensor`) commands.
+Note that this requires to have libtorch install on your system and some environment variables set. For more information, see [tch install page](https://github.com/LaurentMazare/tch-rs?tab=readme-ov-file#getting-started).

doc/src/modelization/README.md

@@ -0,0 +1,59 @@
+# Modelization
+
+In this section, we describe how to encode problems in Schlandals.
+We first give the theoretical foundations to understand these encodings, and then each sub-section shows how to encode a specific problem.
+We currently have encodings (or translations) for
+
+- [Bayesian Networks](./bn.md)
+- [Reachability in Probabilistic Graphs](./pg.md)
+- [ProbLog Programs](./problog.md)
+
+## A Restricted Propositional Logic Language
+
+Schlandals works on propositional formulas in Conjunctive Normal Form (CNF) containing only Horn clauses.
+In Horn clauses, at most one literal has a positive polarity.
+For example, \\( \lnot x \lor \lnot y \lor z \\) is a valid Horn clause as only \\( z \\) has a positive polarity.
+Using the logical equivalence \\( (A \implies B) \Leftrightarrow (\lnot A \lor B) \\), Horn clauses are implications with potentially empty consequences.
+
+Let \\( F \\) be a Horn formula over variables \\( \mathcal{X} \\). In Schlandals, the variables are partitioned into two sets \\( \mathcal{P} \\) and \\( \mathcal{Y} \\).
+The set \\( \mathcal{Y} \\) of variables contains classical boolean variables (deterministic variables), while the set \\( \mathcal{P} \\) includes the variables associated with the distributions (probabilistic variables).
+Let us assume that \\( n \\) distributions are defined for the problem.
+Then, \\( \mathcal{P} = \cup_{i = 1}^n D_i \\) with \\( D_i \cap D_j = \emptyset \\) for all \\( i \neq j \\).
+Moreove, every variable \\( v \in D \\) has a weight \\( P(v) \\) and \\( \sum_{v \in D_i} P(v) = 1 \\).
+
+Let \\( I = \mathbf{x} \\) be an assignment to the variables \\( \mathcal{X} \\). We say that \\( I \\) is an interpretation of \\( F \\), and it is a model if \\( F[I] = \top \\) (i.e., evaluating \\( F \\) with the values in \\( I \\) reduce to true).
+In Schlandals, there is an additional constraint: a model \\( I \\) is valid only if it sets exactly one variable to \\( \top \\) per distribution.
+
+If we denote \\( v_i \\) the value set to \\( \top \\) in distribution \\( D_i \\), the weight of a model \\( I \\) can be computed as \\[ \omega(I) = \prod_{i = 1}^n P(v_i) \\]
+If \\( \mathcal{M} \\) denotes the set of models of \\( F \\), then the goal is to compute \\[ \sum_{I \in \mathcal{M}} \omega(I) \\].
+
+## A Modified DIMACS Format
+
+Schlandals reads its inputs from a modified [DIMACS format](https://mccompetition.org/assets/files/2021/competition2021.pdf).
+It follows the same rules as the DIMACS format, with an additional rule for the distributions (and it ignores the lines starting with `c p weight` used in other weighted model counters).
+Below is an example of a modified DIMACS file
+```
+p cnf 16 11
+c Lines starting with `c` alone are comments.
+c The first line must be the head in the form of "p cnf <number variable> <number clauses>
+c The distributions are defined by lines starting with "c p distribution"
+c Each value in a distribution is assigned to a variable, starting from 1. Hence, the first N variables
+c are used for the distributions.
+c p distribution 0.2 0.8
+c p distribution 0.3 0.7
+c p distribution 0.4 0.6
+c p distribution 0.1 0.9
+c p distribution 0.5 0.5
+c Finally, the clauses are encoded as in DIMACS.
+11 -1 0
+12 -2 0
+13 -11 -3 0
+13 -12 -5 0
+14 -11 -4 0
+14 -12 -6 0
+15 -13 -7 0
+15 -14 -9 0
+16 -13 -8 0
+16 -14 -10 0
+-12 0
+```

doc/src/modelization/bn.md

@@ -30,7 +30,7 @@ For each CPT entry of node \\( v \\), associated with value \\( v \\) and parent
 
 ## The Query
 
-Let \\( V \\) have domain \\( v_1, \ldots, v_m \\). Then, to encode the query \\( P(V = v_i \\), we add the clauses \\( \lnot v_i \\) for all \\( i \neq j \\).
+Let \\( V \\) have domain \\( v_1, \ldots, v_m \\). Then, to encode the query \\( P(V = v_i) \\), we add the clauses \\( \lnot v_i \\) for all \\( i \neq j \\).
 
 ## Example
 
@@ -87,4 +87,5 @@ c Query
 ## References
 
 [1] Mark Chavira and Adnan Darwiche. On probabilistic inference by weighted model counting. Artificial Intelligence, 172(6-7), 2008.
+
 [2] Anicet Bart, Frédéric Koriche, Jean-Marie Lagniez, and Pierre Marquis. An improved CNF encoding scheme for probabilistic inference. In Proceedings of the Twenty-second European Conference on Artificial Intelligence, 2016.