Sabato non booleano

Question

Mi chiedevo la complessità dei test SAT con variabili $ x_i = 0 lor 1 lor 2 dots lor n $, con le clausole che sono della forma $ x_i = a implica x_j neq b $. quando $ n = 2 $, abbiamo 2sat, che ha algoritmi di tempo lineari. Nel frattempo, se $ n> 2 $, quindi se possiamo quasi convertirlo in 2sat avendo variabili booleane $ x_ {i, a} $ corrispondente alla dichiarazione $ x_i = a $, Tuttavia, ciò consente $ x_ {i, 1} = x_ {i, 2} = dots = x_ {i, n} = 0 $, che sarebbe andato $ x_i $ non assegnato.