(set-logic QF_UF)
(set-option :produce-models true)
; 2x3 board as an example


; 4 horizontal dominos
; h_i_j covers (i,j) and (i, j+1) cells

(declare-const h_1_1 Bool)
(declare-const h_1_2 Bool)
(declare-const h_2_1 Bool)
(declare-const h_2_2 Bool)

; Three vertical dominos
; v_i_j covers (i,j) and (i+1, j) cells


(declare-const v_1_1 Bool)
(declare-const v_1_2 Bool)
(declare-const v_1_3 Bool)

; Exactly one domino covers each square.
(assert (or h_1_1 v_1_1)) ; square (1, 1): at least one
(assert (not (and h_1_1 v_1_1))) ; square (1, 1): not both
(assert (or h_1_1 h_1_2 v_1_2)) ; square (1, 2): at least one
(assert (not (and h_1_1 h_1_2))) ; square (1, 2): not both
(assert (not (and h_1_1 v_1_2))) ; square (1, 2): not both
(assert (not (and h_1_2 v_1_2))) ; square (1, 2): not both
(assert (or h_1_2 v_1_3)) ; square (1, 3): at least one
(assert (not (and h_1_2 v_1_3))) ; square (1, 3): not both
(assert (or h_2_1 v_1_1)) ; square (2, 1): at least one
(assert (not (and h_2_1 v_1_1))) ; square (2, 1): not both
(assert (or h_2_1 h_2_2 v_1_2)) ; square (2, 2): at least one
(assert (not (and h_2_1 h_2_2))) ; square (2, 2): not both
(assert (not (and h_2_1 v_1_2))) ; square (2, 2): not both
(assert (not (and h_2_2 v_1_2))) ; square (2, 2): not both
(assert (or h_2_2 v_1_3)) ; square (2, 3): at least one
(assert (not (and h_2_2 v_1_3))) ; square (2, 3): not both

(check-sat)
(get-value (h_1_1 h_1_2 h_2_1 h_2_2 v_1_1 v_1_2 v_1_3))

; Scenario: forbid both outer verticals
(push 1)
(assert (and (not v_1_1) (not v_1_3)))
(check-sat) ; expect unsat
(pop 1)

(exit)