Four lines designated A to D. A and B or A and C or C and D are not allowed to be consecutive but permutation is allowed. Various SMT and LP examples.

bool.txt

(set-option :produce-models true)
(set-logic QF_BV)

(declare-const A1 Bool)
(declare-const A2 Bool)
(declare-const A3 Bool)
(declare-const A4 Bool)

(declare-const B1 Bool)
(declare-const B2 Bool)
(declare-const B3 Bool)
(declare-const B4 Bool)

(declare-const C1 Bool)
(declare-const C2 Bool)
(declare-const C3 Bool)
(declare-const C4 Bool)

(declare-const D1 Bool)
(declare-const D2 Bool)
(declare-const D3 Bool)
(declare-const D4 Bool)

(assert (and
	(or A1 A2 A3 A4)
	(=> A1 (not (or A2 A3 A4 B1 C1 D1)))
	(=> A2 (not (or A1 A3 A4 B2 C2 D2)))
	(=> A3 (not (or A1 A2 A4 B3 C3 D3)))
	(=> A4 (not (or A1 A2 A3 B4 C4 D4)))
	(or B1 B2 B3 B4)
	(=> B1 (not (or B2 B3 B4 A1 C1 D1)))
	(=> B2 (not (or B1 B3 B4 A2 C2 D2)))
	(=> B3 (not (or B1 B2 B4 A3 C3 D3)))
	(=> B4 (not (or B1 B2 B3 A4 C4 D4)))
	(or C1 C2 C3 C4)
	(=> C1 (not (or C2 C3 C4 A1 B1 D1)))
	(=> C2 (not (or C1 C3 C4 A2 B2 D2)))
	(=> C3 (not (or C1 C2 C4 A3 B3 D3)))
	(=> C4 (not (or C1 C2 C3 A4 B4 D4)))
	(or D1 D2 D3 D4)
	(=> D1 (not (or D2 D3 D4 A1 B1 C1)))
	(=> D2 (not (or D1 D3 D4 A2 B2 C2)))
	(=> D3 (not (or D1 D2 D4 A3 B3 C3)))
	(=> D4 (not (or D1 D2 D3 A4 B4 C4)))
	(=> A1 (not B2)) (=> B1 (not A2))
	(=> A2 (not B3)) (=> B2 (not A3))
	(=> A3 (not B4)) (=> B3 (not A4))
	(=> A1 (not C2)) (=> C1 (not A2))
	(=> A2 (not C3)) (=> C2 (not A3))
	(=> A3 (not C4)) (=> C3 (not A4))
	(=> C1 (not D2)) (=> D1 (not C2))
	(=> C2 (not D3)) (=> D2 (not C3))
	(=> C3 (not D4)) (=> D3 (not C4))
))

(check-sat)
;(get-model)
(get-value (
	A1 A2 A3 A4
	B1 B2 B3 B4
	C1 C2 C3 C4
	D1 D2 D3 D4
))

bv.txt

(set-option :produce-models true)
(set-logic QF_BV)

(declare-const A (_ BitVec 2))
(declare-const B (_ BitVec 2))
(declare-const C (_ BitVec 2))
(declare-const D (_ BitVec 2))

(define-fun notouch ((a (_ BitVec 2)) (b (_ BitVec 2))) Bool
	(ite (bvult a b)
	(bvuge (bvsub b a) #b10)
	(bvuge (bvsub a b) #b10)
))

(assert (and
	(distinct A B C D)
	(notouch A B)
	(notouch A C)
	(notouch C D)
))

(check-sat)
;(get-model)
(get-value (A B C D))

idl.txt

(set-option :produce-models true)
(set-logic QF_IDL)

(declare-const A Int)
(declare-const B Int)
(declare-const C Int)
(declare-const D Int)

(define-fun inrange ((x Int)) Bool
	(and (>= x 1) (<= x 4)))

(define-fun notouch ((x Int) (y Int)) Bool
	(ite (< x y) (>= (- y x) 2) (>= (- x y) 2)))

(assert (and
	(distinct A B C D)
	(inrange A)
	(inrange B)
	(inrange C)
	(inrange D)
	(notouch A B)
	(notouch A C)
	(notouch C D)
))

(check-sat)
;(get-model)
(get-value (A B C D))

lp.txt

Maximize

A1 + A2 + A3 + A4 + B1 + B2 + B3 + B4 + C1 + C2 + C3 + C4 + D1 + D2 + D3 + D4

Subject to

A1 + A2 + A3 + A4 <= 1
B1 + B2 + B3 + B4 <= 1
C1 + C2 + C3 + C4 <= 1
D1 + D2 + D3 + D4 <= 1

A1 + B1 + C1 + D1 <= 1
A2 + B2 + C2 + D2 <= 1
A3 + B3 + C3 + D3 <= 1
A4 + B4 + C4 + D4 <= 1

A1 + B2 <= 1
B1 + A2 <= 1
A2 + B3 <= 1
B2 + A3 <= 1
A3 + B4 <= 1
B3 + A4 <= 1

A1 + C2 <= 1
C1 + A2 <= 1
A2 + C3 <= 1
C2 + A3 <= 1
A3 + C4 <= 1
C3 + A4 <= 1

C1 + D2 <= 1
D1 + C2 <= 1
C2 + D3 <= 1
D2 + C3 <= 1
C3 + D4 <= 1
D3 + C4 <= 1

Binary

A1 A2 A3 A4 B1 B2 B3 B4 C1 C2 C3 C4 D1 D2 D3 D4

End