XOR with three constants in First Order Logic

Question

I have a problem where S(X) is true for either (only one of) X=a, X=i, or X=k

I've expressed it like so:
$$ (S(a)\land ¬S(i)\land ¬S(k))\lor(¬S(a)\land S(i)\land ¬S(k))\lor (¬S(a)\land ¬S(i)\land S(k)) $$

If I reduce this to CNF I get a very long set of clauses after distributing ands over ors. Is there a 'nicer' way of writing this?

Thanks!

Answer 1

If you are okay with using XOR then your expression can be seen as XOR of all the cases, excluding the one with all true:

$$(S(a) \oplus S(i) \oplus S(k)) \land \lnot (S(a) \land S(i) \land S(k))$$

In general taking the XOR of some inputs will be true if an odd number of inputs are true, that is XOR acts like addition mod 2.

Note that I interpret your first sentence as "$S(X)$ is true for exactly one of $X=a, X=i, X=k$". The "either" case is trivial OR.