Add comments on new files

README.md

@@ -9,10 +9,7 @@ Schlandals is a projected weighted model counter which targets inference in prob
 Current known probability queries that can be solved with the solver include
   - Computing the probability of some target variables (given some evidences) in a Bayesian network
   - Computing the probability that two nodes are connected in a probabilistic graph
-
-The solver currently supports two types of solving
-  - Search based solving with a DPLL-style backtracing search
-  - Compiling into (or read from a file) an arithmetic circuit with distributions as leaf
+  - A mapping from [ProbLog](https://github.com/ML-KULeuven/problog) programs to Schlandals
 
 # Problem specification
 
@@ -28,9 +25,9 @@ Schlandals takes as input a file using a modified version of the [DIMACS](https:
 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>
 p cnf 16 11
-c Following the header, must be the definition of the distributions. Note that the lines starts with "c p distribution" which is similar to how weights are encoded in DIMACS (c p weight).
-c /!\ The definition of the distribution MUST be before the clauses and induce an implicit numbering on the variable. Below, the first distribution will have
-c variable with index 1 and 2. The second has the variables with index 3 and 4, etc.
+c The distribution 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
@@ -84,3 +81,28 @@ The circuit can be stored in the file given by the `fdac` argument and a DOT vis
 ### Reading a compiled file
 
 A previously compiled file can be read using `schlandals read-compiled -i <fdac file> [--dotfile <dotfile]`.
+
+# Citing
+
+To cite Schlandals in your work, use the following
+
+```
+@InProceedings{dubray_et_al:LIPIcs.CP.2023.15,
+  author =	{Dubray, Alexandre and Schaus, Pierre and Nijssen, Siegfried},
+  title =	{{Probabilistic Inference by Projected Weighted Model Counting on Horn Clauses}},
+  booktitle =	{29th International Conference on Principles and Practice of Constraint Programming (CP 2023)},
+  pages =	{15:1--15:17},
+  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
+  ISBN =	{978-3-95977-300-3},
+  ISSN =	{1868-8969},
+  year =	{2023},
+  volume =	{280},
+  editor =	{Yap, Roland H. C.},
+  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
+  address =	{Dagstuhl, Germany},
+  URL =		{https://drops.dagstuhl.de/opus/volltexte/2023/19052},
+  URN =		{urn:nbn:de:0030-drops-190520},
+  doi =		{10.4230/LIPIcs.CP.2023.15},
+  annote =	{Keywords: Model Counting, Bayesian Networks, Probabilistic Networks}
+}
+```

src/core/clause.rs

@@ -14,6 +14,16 @@
 //You should have received a copy of the GNU Affero General Public License
 //along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+//! Representation of a clause in Schlandals. All clauses used in Schlandals are Horn clause, which
+//! means that they have at most one positive literal, the head of the clause.
+//! The literals of the clause (head included) are stored in a vector that implements the 2-watch literals
+//! method.
+//! However, the specific needs of Schlandals for the propagation impose that each clause is watched by two pairs
+//! of watched literals.
+//! One pair is composed of deterministic literals, and the other of probabilistic ones.
+//! In this way the propagator can, at any time, query a boud on the number of unfixed deterministic/probabilistic
+//! variables in the clause.
+
 use search_trail::StateManager;
 use super::graph::ClauseIndex;
 use super::sparse_set::SparseSet;
@@ -24,6 +34,7 @@ use super::graph::{DistributionIndex, VariableIndex, Graph};
 
 #[derive(Debug)]
 pub struct Clause {
+    /// id of the clause in the input problem
     id: usize,
     /// If the clause is not learned, this is the literal which is the head of the clause. Otherwise, None
     head: Option<Literal>,
@@ -35,6 +46,7 @@ pub struct Clause {
     pub parents: SparseSet<ClauseIndex>,
     /// Random bitstring used for hash computation
     hash: u64,
+    /// Has the clause been learned during the search
     is_learned: bool,
 }
 
@@ -52,76 +64,99 @@ impl Clause {
         }
     }
 
+    /// Adds a child to the current clause. The child clause has the head of the current clause
+    /// as a negative literals in it.
     pub fn add_child(&mut self, child: ClauseIndex, state: &mut StateManager) {
         self.children.add(child, state);
     }
 
+    /// Adds a parent to the current clause. The parent clause has its head as a negative literal
+    /// in the current clause.
     pub fn add_parent(&mut self, parent: ClauseIndex, state: &mut StateManager) {
         self.parents.add(parent, state);
     }
 
+    /// Remove a child from the children of this clause. Not that this operation is reverted when
+    /// the state manager restore the state
     pub fn remove_child(&mut self, child: ClauseIndex, state: &mut StateManager) {
         self.children.remove(child, state);
     }
 
+    /// Remove a parent from the parents of this clause. Not that this operation is reverted when
+    /// the state manager restore the state
     pub fn remove_parent(&mut self, parent: ClauseIndex, state: &mut StateManager) {
         self.parents.remove(parent, state);
     }
 
+    /// Returns a bound on the number ofdeterministic (first element) and probabilistic (second element) 
+    /// unfixed variable in the clause
     pub fn get_bounds_watcher(&self, state: &StateManager) -> (usize, usize) {
         self.literals.get_bounds(state)
     }
 
+    /// Returns true if the clause still has unfixed probabilistic variables in it
     pub fn has_probabilistic(&self, state: &StateManager) -> bool {
         self.literals.get_alive_end_watcher(state).is_some()
     }
 
+    /// Set the clause as unconstrained. This operation is reverted when the state manager restore its state.
     pub fn set_unconstrained(&self, state: &mut StateManager) {
         self.literals.set_unconstrained(state);
     }
 
+    /// Returns true iff the clause is constrained
     pub fn is_constrained(&self, state: &StateManager) -> bool {
         self.literals.is_constrained(state)
     }
 
+    /// Returns the hash of the clause
     pub fn hash(&self) -> u64 {
         self.hash
     }
 
+    /// If the clause still has unfixed probabilisitc variables, return the distribution of the first watcher.
+    /// Else, return None.
     pub fn get_constrained_distribution(&self, state: &StateManager, g: &Graph) -> Option<DistributionIndex> {
         match self.literals.get_alive_end_watcher(state) {
             None => None,
             Some(l) => g[l.to_variable()].distribution(),
         }
     }
 
+    /// Returns the number of parents of the clause in the initial problem
     pub fn number_parents(&self) -> usize {
         self.parents.capacity()
     }
 
+    /// Returns the number of children of the clause in the initial problem
     pub fn number_children(&self) -> usize {
         self.children.capacity()
     }
 
+    /// Returns the number of constrained parent of the clause
     pub fn number_constrained_parents(&self, state: &StateManager) -> usize {
         self.parents.len(state)
     }
 
+    /// Returns the number of constrained children of the clause
     pub fn number_constrained_children(&self, state: &StateManager) -> usize {
         self.children.len(state)
     }
 
+    /// Return the head of the clause
     pub fn head(&self) -> Option<Literal> {
         self.head
     }
 
+    /// Returns true iff the variable is the head of the clause
     pub fn is_head(&self, variable: VariableIndex) -> bool {
         match self.head {
             None => false,
             Some(h) => h.to_variable() == variable,
         }
     }
 
+    /// Notify the clause that the given variable has taken the given value. Updates the watchers accordingly.
     pub fn notify_variable_value(&mut self, variable: VariableIndex, value: bool, probabilistic: bool, state: &mut StateManager) -> VariableIndex {
         if !probabilistic {
             self.literals.update_watcher_start(variable, value, state)
@@ -130,6 +165,7 @@ impl Clause {
         }
     }
 
+    /// Returns true iff the clause is unit
     pub fn is_unit(&self, state: &StateManager) -> bool {
         if !self.is_constrained(state) {
             return false;
@@ -138,6 +174,7 @@ impl Clause {
         bounds.0 + bounds.1 == 1
     }
 
+    /// Returns the last unfixed literal in the unit clause
     pub fn get_unit_assigment(&self, state: &StateManager) -> Literal {
         debug_assert!(self.is_unit(state));
         let bounds = self.literals.get_bounds(state);
@@ -148,16 +185,7 @@ impl Clause {
         }
     }
 
-    pub fn has_probabilistic_in_body(&self, state: &StateManager) -> bool {
-        let bound_probabilistic = self.literals.get_bounds(state).1;
-        for i in 0..bound_probabilistic {
-            if !self.literals[self.literals.limit() + i].is_positive() {
-                return true;
-            }
-        }
-        return false;
-    }
-
+    /// Returns true iff the clause stil has unfixed deterministic variables in its body
     pub fn has_deterministic_in_body(&self, state: &StateManager) -> bool {
         let bound_deterministic = self.literals.get_bounds(state).0;
         for i in 0..bound_deterministic {
@@ -168,34 +196,41 @@ impl Clause {
         return false;
     }
 
+    /// Returns true iff the clause is learned
     pub fn is_learned(&self) -> bool {
         self.is_learned
     }
 
     // --- ITERATORRS --- //
 
+    /// Returns an iterator on the (constrained) parents of the clause
     pub fn iter_parents(&self, state: &StateManager) -> impl Iterator<Item = ClauseIndex> + '_ {
         self.parents.iter(state)
     }
 
+    /// Returns an iterator on the (constrained) children of the clause
     pub fn iter_children(&self, state: &StateManager) -> impl Iterator<Item = ClauseIndex> + '_ {
         self.children.iter(state)
     }
 
+    /// Returns an interator on the literals of the clause
     pub fn iter(&self) -> impl Iterator<Item = Literal> + '_ {
         self.literals.iter()
     }
 
+    /// Returns an iterator on the variables represented by the literals of the clause
     pub fn iter_variables(&self) -> impl Iterator<Item = VariableIndex> + '_ {
         self.literals.iter().map(|l| l.to_variable())
     }
 
+    /// Returns an iterator on the probabilistic varaibles in the clause
     pub fn iter_probabilistic_variables(&self) -> impl Iterator<Item = VariableIndex> + '_ {
         self.literals.iter_end().map(|l| l.to_variable())
     }
 
 }
 
+// Writes a clause as C{id}: l1 l2 ... ln
 impl std::fmt::Display for Clause {
 
     fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {

src/core/components.rs

@@ -150,6 +150,7 @@ impl ComponentExtractor {
         g[clause].is_constrained(state) && !(comp_start <= clause_pos && clause_pos < (comp_start + *comp_size))
     }
 
+    /// Returns true if the distribution has not yet been visited during the component exploration
     fn is_distribution_visitable(&self, distribution: DistributionIndex, distribution_start: usize, distribution_size: &usize) -> bool {
         let distribution_pos = self.distribution_positions[distribution.0];
         !(distribution_start <= distribution_pos && distribution_pos < (distribution_start + *distribution_size))
@@ -210,10 +211,10 @@ impl ComponentExtractor {
                             *comp_number_distribution += 1;
                             for v in g[distribution].iter_variables() {
                                 if !g[v].is_fixed(state) {
-                                    for c in g[v].iter_clause_negative_occurence() {      
+                                    for c in g[v].iter_clauses_negative_occurence() {      
                                         self.explore_component(g, c, comp_start, comp_size, comp_distribution_start, comp_number_distribution, hash, state);
                                     }
-                                    for c in g[v].iter_clause_positive_occurence() {
+                                    for c in g[v].iter_clauses_positive_occurence() {
                                         self.explore_component(g, c, comp_start, comp_size, comp_distribution_start, comp_number_distribution, hash, state);
                                     }
                                 }
@@ -325,6 +326,8 @@ impl ComponentExtractor {
         self.distributions[start..end].iter().copied()
     }
 
+    /// Adds a clause to a component. This function is called when the solver encounters an UNSAT and needs to learn a clause.
+    /// During this process we ensure that the learned clause is horn and can be safely added in the component for further detections.
     pub fn add_clause_to_component(&mut self, component: ComponentIndex, clause: ClauseIndex) {
         debug_assert!(clause.0 == self.clause_positions.len());
         let start = self.components[component.0].start;   

src/core/distribution.rs

@@ -14,27 +14,27 @@
 //You should have received a copy of the GNU Affero General Public License
 //along with this program.  If not, see <http://www.gnu.org/licenses/>.
 
+//! This module provide the implementation of a distribution in Schlandals.
+//! A distribution is a set of variable that respects the following constraints:
+//!     1. Every variable must have a weight
+//!     2. The sum of the variables' weight must sum to 1
+//!     3. In each model of the input formula, exactly one of the variables is set to true
+
 use super::graph::VariableIndex;
 use search_trail::{StateManager, ReversibleUsize, UsizeManager};
 
-/// Represents a set of variable in a same distribution. This assume that the variable of a distribution
-/// are inserted in the graph one after the other (i.e. that their `VariableIndex` are consecutive).
-/// Since no variable should be removed from the graph once constructed, this should not be a problem.
-/// Thus a distribution is identified by the first `VariableIndex` and the number of variable in it.
-/// 
-/// We also store the number of clauses in which the distribution appears. This is usefull to compute
-/// the unconstrained probability during the propagation.
-/// In the same manner, the number of variable assigned to false in the distribution is kept, allowing us
-/// to efficiently detect that only one variable remains in a distribution.
+/// A distribution of the input problem
 #[derive(Debug, Clone, Copy, PartialEq)]
 pub struct Distribution {
+    /// Id of the distribution in the problem
     id: usize,
     /// First variable in the distribution
     pub first: VariableIndex,
     /// Number of variable in the distribution
     pub size: usize,
     /// Number of constrained clauses in which the distribution appears
     pub number_clause_unconstrained: ReversibleUsize,
+    /// Number of clauses in which the distribution appears
     number_clause: usize,
     /// Number of variables assigned to F in the distribution
     pub number_false: ReversibleUsize,
@@ -53,32 +53,43 @@ impl Distribution {
         }
     }
 
+    /// Increments the number of clauses in which the distribution appears
     pub fn increment_clause(&mut self) {
         self.number_clause += 1;
     }
 
+    /// Decrements the number of constrained clause in which the distribution appears. This
+    /// operation is reversed when the trail restore its state.
+    /// Returns the remaining number of constrained clauses in which it appears.
     pub fn decrement_constrained(&self, state: &mut StateManager) -> usize {
         self.number_clause - state.increment_usize(self.number_clause_unconstrained)
     }
 
+    /// Icrements the number of variable assigned to false in the distribution. This operation
+    /// is reversed when the trail restore its state.
     pub fn increment_number_false(&self, state: &mut StateManager) -> usize {
         state.increment_usize(self.number_false)
     }
 
+    /// Returns the number of unfixed variables in the distribution. This assume that the distribution
+    /// has no variable set to true (otherwise there is no need to consider it).
     pub fn number_unfixed(&self, state: &StateManager) -> usize {
         self.size - state.get_usize(self.number_false)
     }
 
+    /// Returns the number of variable set to false in the distribution.
     pub fn number_false(&self, state: &StateManager) -> usize {
         state.get_usize(self.number_false)
     }
 
+    /// Returns the start of the distribution in the vector of variables in the graph.
     pub fn start(&self) -> VariableIndex {
         self.first
     }
 
     // --- ITERATOR --- //
 
+    /// Returns an iterator on the variables of the distribution
     pub fn iter_variables(&self) -> impl Iterator<Item = VariableIndex> {
         (self.first.0..(self.first.0 + self.size)).map(VariableIndex)
     }