diff --git a/docs/tutorial.md b/docs/tutorial.md index e69de29..3a7268f 100644 --- a/docs/tutorial.md +++ b/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. \ No newline at end of file diff --git a/examples/discrete_vs_nodiscrete.rs b/examples/discrete_vs_nodiscrete.rs index 2d1f4e5..a55b61c 100644 --- a/examples/discrete_vs_nodiscrete.rs +++ b/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(); diff --git a/src/algorithms/sat_flexible_time_model.rs b/src/algorithms/sat_flexible_time_model.rs index 384ad42..5064cd8 100644 --- a/src/algorithms/sat_flexible_time_model.rs +++ b/src/algorithms/sat_flexible_time_model.rs @@ -124,7 +124,7 @@ impl SolverAlgo stop: std::sync::Arc, 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 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, @@ -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);