pizza_puzzle_blocked.smt2

; Rachel's Pizza Ordering Puzzle — blocking the first solution
;
; Same puzzle as pizza_puzzle.smt2, but we block the known solution
; to check if any other solution exists. If unsat, the solution is unique.

(set-logic QF_DT)

; --- Pizza types (from the coffee-stained list) ---
(declare-datatypes ((Pizza 0)) ((
  (Cheese) (Pepperoni) (Margherita) (Hawaiian) (BBQChicken) (PeppersOnions) (Sausage)
)))

; --- Each person's order ---
(declare-const rachel  Pizza)
(declare-const emily   Pizza)
(declare-const owen    Pizza)
(declare-const yasmine Pizza)
(declare-const nathan  Pizza)
(declare-const wendy   Pizza)
(declare-const kevin   Pizza)

; --- Pizza properties ---

(define-fun is-vegetarian ((p Pizza)) Bool
  (or (= p Cheese) (= p Margherita) (= p PeppersOnions)))

(define-fun has-meat ((p Pizza)) Bool
  (or (= p Pepperoni) (= p Hawaiian) (= p BBQChicken) (= p Sausage)))

(define-fun has-onions ((p Pizza)) Bool
  (= p PeppersOnions))

(define-fun has-pineapple ((p Pizza)) Bool
  (= p Hawaiian))

(define-fun is-classic ((p Pizza)) Bool
  (or (= p Cheese) (= p Pepperoni) (= p Margherita)))

; --- Constraints (same as before) ---

(assert (distinct rachel emily owen yasmine nathan wendy kevin))
(assert (is-vegetarian emily))
(assert (is-vegetarian owen))
(assert (not (= yasmine Cheese)))
(assert (is-classic nathan))
(assert (not (has-onions emily)))
(assert (not (has-pineapple wendy)))
(assert (= rachel Cheese))
(assert (has-meat kevin))
(assert (or (= nathan Sausage) (= owen Sausage) (= kevin Sausage)))

; --- Block the first solution ---
; Negate the conjunction of all assignments from the known solution.
; This forces the solver to find a *different* assignment if one exists.
(assert (not (and
  (= rachel  Cheese)
  (= emily   Margherita)
  (= owen    PeppersOnions)
  (= yasmine Hawaiian)
  (= nathan  Pepperoni)
  (= wendy   BBQChicken)
  (= kevin   Sausage)
)))

(check-sat)
; If sat  → there is another solution (get-model to see it)
; If unsat → the first solution is the only one