Add basic tutorial

Signed-off-by: Arjo Chakravarty <[email protected]>

docs/tutorial.md

@@ -0,0 +1,64 @@
+# Using the SAT solver for Simple constraint scheduling tasks
+
+We provide two formulations for the SAT solver based approach. First, we have an approach which uses fixed timestamps. Suppose you have a scenario where 5 robots want to access 2 chargers. The robots must use the chargers within the next 5 hours. It takes 2 hours to charge on each charger. We can write each robot's request as:
+```rust
+let chargers = ["Charger 1".to_string(), "Charger 2".to_string()];
+let start_time = Utc:now();
+// Since we said it needs to be done in a time window of 5 hours and it takes 2 hours to charge therefore the latest start time is in 3 hours
+let latest_start_time = start_time + Duration::hours(3); 
+
+
+/// First robot alternative
+let robot1_alternatives = vec![
+    ReservationRequestAlternative {
+        parameters: ReservationParameters {
+            resource_name: chargers[0].clone(),
+            duration: Some(Duration::minutes(120)),
+            start_time: StartTimeRange {
+                earliest_start: Some(start_time),
+                latest_start: Some(latest_start_time),
+            },
+        },
+        cost_function: Arc::new(StaticCost::new(1.0)),
+    },
+    ReservationRequestAlternative {
+        parameters: ReservationParameters {
+            resource_name: chargers[1].clone(),
+            duration: Some(Duration::minutes(120)),
+            start_time: StartTimeRange {
+                earliest_start: Some(start_time),
+                latest_start: Some(latest_start_time),
+            },
+        },
+        cost_function: Arc::new(StaticCost::new(1.0)),
+    },
+];
+
+/// We can add more robots
+let robot2_alternatives = robot1_alternatives.clone();
+let robot3_alternatives = robot1_alternatives.clone();
+let robot4_alternatives = robot1_alternatives.clone();
+let robot5_alternatives = robot1_alternatives.clone();
+```
+Lets set up the SAT based solver problem:
+```rust
+let problem = Problem {
+        requests: vec![req1],
+    };
+```
+
+We are going to use the constrained SAT solver to see if we can get a feasible schedule
+```rust
+let model = SATFlexibleTimeModel {
+                clock_source: FakeClock::default(),
+            };
+```
+A clock source is needed because in the event no starting time is provided, we need to know the current time.
+We can then check if it is even feasible to schedule 5 robots like this on two chargers.
+```rust
+// The stop signal exists so other threads can tell the solver to cleanly exit. For the single
+// threaded case we can ignore it.
+let stop = Arc::new(AtomicBool::new(false));
+let result = model.feasibility_analysis(&problem, stop);
+```
+Note: It is much faster to check feasibility then optimize later on.

examples/discrete_vs_nodiscrete.rs

@@ -118,7 +118,7 @@ fn main() {
                 clock_source: FakeClock::default(),
             };
 
-            model.feasbility_analysis(&sat_flexible_time_problem, stop);
+            model.feasibility_analysis(&sat_flexible_time_problem, stop);
 
             let greedy_dur = timer.elapsed();
 

src/algorithms/sat_flexible_time_model.rs

@@ -124,7 +124,7 @@ impl<CS: ClockSource + Clone + std::marker::Send + std::marker::Sync> SolverAlgo
         stop: std::sync::Arc<AtomicBool>,
         problem: Problem,
     ) {
-        let Ok(problem) = self.feasbility_analysis(&problem, stop) else {
+        let Ok(problem) = self.feasibility_analysis(&problem, stop) else {
             result_channel.send(AlgorithmState::UnSolveable);
             return;
         };
@@ -573,7 +573,7 @@ impl<CS: ClockSource + Clone + std::marker::Send + std::marker::Sync> SATFlexibl
     /// - `stop` - Takes in an atomic boolean that allows you to stop the computation from another thread.
     /// Returns a result containing an example feasible schedule if OK. Otherwise, returns an error.
     /// The feasible schedule is a HashMap where the key of the hashmap is the resource and thevalue of the hashmap is the assigned alternative.
-    pub fn feasbility_analysis(
+    pub fn feasibility_analysis(
         &self,
         problem: &Problem,
         stop: std::sync::Arc<AtomicBool>,
@@ -965,7 +965,7 @@ fn test_flexible_one_item_sat_solver() {
     let model = SATFlexibleTimeModel {
         clock_source: DefaultUtcClock::default(),
     }
-    .feasbility_analysis(&problem, stop);
+    .feasibility_analysis(&problem, stop);
     let result = model.unwrap();
 
     assert_eq!(result.len(), 1usize);
@@ -1028,7 +1028,7 @@ fn test_flexible_two_items_sat_solver() {
     let model = SATFlexibleTimeModel {
         clock_source: DefaultUtcClock::default(),
     }
-    .feasbility_analysis(&problem, stop);
+    .feasibility_analysis(&problem, stop);
     let result = model.unwrap();
 
     assert_eq!(result.len(), 1usize);
@@ -1073,7 +1073,7 @@ fn test_flexible_n_items_sat_solver() {
     let model = SATFlexibleTimeModel {
         clock_source: DefaultUtcClock::default(),
     }
-    .feasbility_analysis(&problem, stop);
+    .feasibility_analysis(&problem, stop);
     let result = model.unwrap();
 
     assert_eq!(result.len(), 1usize);
@@ -1118,7 +1118,7 @@ fn test_flexible_no_soln_sat_solver() {
     let model = SATFlexibleTimeModel {
         clock_source: DefaultUtcClock::default(),
     }
-    .feasbility_analysis(&problem, stop);
+    .feasibility_analysis(&problem, stop);
     let result = model.unwrap();
 
     assert_eq!(result.len(), 1usize);