sat_rs/
notation.rs

1//! Collection of structs representing the notation used in the SAT solver
2//!
3//! * [`Literal`] - A struct representing a literal (atom)
4//! * [`Clause`] - A struct representing a clause
5//! * [`Formula`] - A struct representing a propositional formula
6use std::collections::HashMap;
7
8/// Struct representing a Literal. Also known as an atom.
9///
10/// Derives from [`Debug`] and [`Clone`].
11/// Contains a value and a boolean representing whether it is negated or not
12///
13/// # Examples
14/// ```rust
15/// use sat_rs::notation::Literal;
16///
17/// let literal = Literal::new();
18///
19/// let literal = Literal::from_value(1);
20///
21/// let literal = Literal{ value: 1, negated: false};
22/// ```
23#[derive(Debug, Clone)]
24pub struct Literal {
25    pub value: i32,
26    pub negated: bool,
27}
28
29impl Literal {
30
31    /// Creates a new [`Literal`] with value `0` and negated set to `false`
32    ///
33    /// # Examples
34    /// ```rust
35    /// use sat_rs::notation::Literal;
36    ///
37    /// let literal = Literal::new();
38    /// ```
39    #[allow(dead_code)]
40    pub fn new() -> Literal {
41        return Literal {
42            value: 0,
43            negated: false,
44        }
45    }
46
47    /// Creates a new [`Literal`] from a given value. Negated is set to `false`
48    ///
49    /// # Arguments
50    /// * `value` - An [`i32`] representing the value of the [`Literal`]
51    ///
52    /// # Examples
53    /// ```rust
54    /// use sat_rs::notation::Literal;
55    ///
56    /// let literal = Literal::from_value(1);
57    /// ```
58    #[allow(dead_code)]
59    pub fn from_value(value: i32) -> Literal {
60        return Literal {
61            value: value,
62            negated: false,
63        }
64    }
65}
66
67/// Struct representing a Clause
68///
69/// Derives from [`Debug`] and [`Clone`].
70///
71/// Contains a vector of [`Literal`]s
72///
73/// # Examples
74/// ```rust
75/// use sat_rs::notation::Literal;
76/// use sat_rs::notation::Clause;
77///
78/// let mut clause = Clause::new();
79///
80/// let p = Literal{ value: 1, negated: false};
81/// let q = Literal{ value: 2, negated: false};
82///
83/// clause.literals.push(p);
84/// clause.literals.push(q);
85/// ```
86#[derive(Debug, Clone)]
87pub struct Clause {
88    pub literals: Vec<Literal>,
89}
90
91impl Clause {
92
93    /// Creates a new [`Clause`] with an empty vector of [`Literal`]s
94    ///
95    /// # Examples
96    /// ```rust
97    /// use sat_rs::notation::Clause;
98    ///
99    /// let clause = Clause::new();
100    /// ```
101    pub fn new() -> Clause {
102        Clause {
103            literals: Vec::new(),
104        }
105    }
106}
107
108/// Struct representing a Propositional Formula
109///
110/// Derives from [`Debug`] and [`Clone`].
111///
112/// Contains a vector of [`Clause`]s, a vector of [`Literal`]s, the number of clauses and the number of variables
113#[derive(Debug, Clone)]
114pub struct Formula {
115    pub clauses: Vec<Clause>,
116    pub literals: Vec<i32>,
117    pub num_clauses: i32,
118    pub num_vars: i32,
119}
120
121
122impl Formula {
123
124    /// Creates a new [`Formula`] with an empty vector of [`Clause`]s and [`Literal`]s
125    ///
126    /// # Examples
127    /// ```rust
128    /// use sat_rs::notation::Formula;
129    ///
130    /// let formula = Formula::new();
131    /// ```
132    #[allow(dead_code)]
133    pub fn new() -> Formula {
134        Formula {
135            clauses: Vec::new(),
136            literals: Vec::new(),
137            num_clauses: 0,
138            num_vars: 0,
139        }
140    }
141
142    #[allow(dead_code)]
143    /// Evaluates a [`Formula`] given an interpretation
144    ///
145    /// # Arguments
146    /// * `interpretation` - A [`HashMap`] of [`i32`] and [`bool`] representing the interpretation
147    ///
148    /// # Examples
149    /// Assuming the CNF file is in `/bin/problem.cnf` and contains the following:
150    /// ```;
151    /// p cnf 3 1
152    /// 1 -3 0
153    /// 2 3 -1 0
154    /// ```
155    ///
156    /// ```rust
157    /// use sat_rs::cnfparser;
158    /// use std::collections::HashMap;
159    ///
160    /// let buffer = include_str!("bin/problem.cnf");
161    /// let mut formula = cnfparser::parse_cnf(&buffer);
162    ///
163    /// let mut interpretation: HashMap<i32, bool> = HashMap::new();
164    /// interpretation.insert(1, false);
165    /// interpretation.insert(2, false);
166    /// interpretation.insert(3, false);
167    ///
168    /// assert_eq!(formula.unwrap().evaluate(&interpretation), true);
169    /// ```
170    pub fn evaluate(&mut self, interpretation: &HashMap<i32, bool>) -> bool {
171        let mut value: bool = true;
172        for clause in &mut self.clauses {
173            let mut clause_value: bool = false;
174            for literal in &mut clause.literals {
175                let mut literal_value: bool = false;
176                if interpretation.contains_key(&literal.value) {
177                    literal_value = interpretation[&literal.value];
178                }
179                if literal.negated {
180                    literal_value = !literal_value;
181                }
182                if literal_value {
183                    clause_value = true;
184                    break;
185                }
186            }
187            value = value && clause_value;
188        }
189        value
190    }
191}
sat_rs/notation.rs

sat_rs/
notation.rs
