Mỗi yêu cầu có thể được hiểu là các biểu thức logic:

• ~(v_1 \neq i_1) \rightarrow (v_{2}=i_{2}) AND (v_{3}=i_{3})~

• ~(v_2 \neq i_2) \rightarrow (v_{1}=i_{1}) AND (v_{3}=i_{3})~

• ~(v_3 \neq i_3) \rightarrow (v_{2}=i_{2}) AND (v_{1}=i_{1})~

Khi đó, ta có thể đưa bài toán về giải phương trình đồng dư tuyến tính ~n~ ẩn dạng chuẩn tắc hội, trong đó mỗi tuyển sơ cấp chỉ gồm 2 mệnh đề sơ cấp.

~\Rightarrow~ Twosat:

- Twosat có dạng là ~AND~ của nhiều biểu thức dạng ~(a_1 \lor b_1) \land (a_2 \lor b_2) \land \cdots \land (a_n \lor b_n)~.

- Vậy để biến đổi ~1~ yêu cầu dạng ~3~ điều kiện ~a, b, c~ sao cho có ít nhất ~2~ trong ~3~ thoả về để sử dụng twosat là: ~(a \lor b) \land (a \lor c) \land (b \lor c)~.

Code mẫu