schedule.smt

(set-info :source | A cohort scheduling example. |)
(set-info :smt-lib-version 2.0)
(set-option :produce-models true)

;;; The budget indicates how large any one group can be
(declare-fun budget () Int)
(assert (= budget 20))

;;; The total number of groups
(declare-fun groups () Int)
(assert (= groups 3))

(declare-fun group (Int) Int)
(declare-fun group_day (Int) Int)
(declare-fun group_hour (Int) Int)

;;; Each group must not exceed the budget
(assert (< (group 0) budget))
(assert (< (group 1) budget))
(assert (< (group 2) budget))

;;; These variables track people assigned to groups
(declare-fun john_wiegley_group () Int)
(declare-fun aaron_crossley_group () Int)

;;; Each participant must be assigned to one of the available groups
(assert (and (>= john_wiegley_group 0)
             (< john_wiegley_group groups)))
(assert (and (>= aaron_crossley_group 0)
             (< aaron_crossley_group groups)))

;;; The number in each group is determined by the assignments
(assert (= (group 0)
           (+ (if (= john_wiegley_group 0) 1 0)
              (if (= aaron_crossley_group 0) 1 0))))
(assert (= (group 1)
           (+ (if (= john_wiegley_group 1) 1 0)
              (if (= aaron_crossley_group 1) 1 0))))
(assert (= (group 2)
           (+ (if (= john_wiegley_group 2) 1 0)
              (if (= aaron_crossley_group 2) 1 0))))

;;;;;; GROUP SETUP ;;;;;;;;;;

;; Sunday    = 0
;; Monday    = 1
;; Tuesday   = 2
;; Wednesday = 3
;; Thursday  = 4
;; Friday    = 5
;; Saturday  = 6

;; Group 1
(assert (= (group_day 1) 1))            ; Mondays
(assert (= (group_hour 1) 19))          ; 7pm

;; Group 2
(assert (= (group_day 2) 4))            ; Thursdays
(assert (= (group_hour 2) 16))          ; 4pm

;;;;;; ATTENDEE CONSTRAINTS ;;;;;;;;;;

;;; John can meet in the beginning of the week
(assert (or (= (group_day john_wiegley_group) 1)
            (= (group_day john_wiegley_group) 2)
            (= (group_day john_wiegley_group) 3)))

;;; Aaaron can meet toward the end of the week
(assert (or (= (group_day aaron_crossley_group) 4)
            (= (group_day aaron_crossley_group) 5)
            (= (group_day aaron_crossley_group) 6)))

(check-sat)
(get-model)