Algebraic Attacks and CNF
Since the seminal papers [1] and [2] by Bard, Courtois and Jefferson it seems accepted wisdom that the right thing to do for constructing a CNF representation of a block cipher is to construct an algebraic system of equations first (cf. [3]). This system of equations is then converted to CNF using some ANF to CNF converted (e.g. [4]) which deals with the negative impact of the XORs just introduced via the ANF. On the other hand, it is straight forward to compute some CNF for a given S-Box directly by considering its truth table. Sage now contains code which does this for you:
sage: sr = mq.SR(1,1,1,4,gf2=True,polybori=True) sage: S = sr.sbox() sage: print S.cnf()[(1, 2, 3, 4, -5), (1, 2, 3, 4, 6), (1, 2, 3, 4, 7), (1, 2, 3, 4, -8), (1, 2, 3, -4, 5), (1, 2, 3, -4, -6), (1, 2, 3, -4, 7), (1, 2, 3, -4, 8), (1, 2, -3, 4, -5), (1, 2, -3, 4, 6), (1, 2, -3, 4, -7),(1, 2, -3, 4, 8), (1, 2, -3, -4, -5), (1, 2, -3, -4, 6), (1, 2, -3, -4, -7), (1, 2, -3, -4, -8), (1, -2, 3, 4, -5), (1, -2, 3, 4, -6), (1, -2, 3, 4, 7), (1, -2, 3, 4, -8), (1, -2, 3, -4, 5), (1, -2, 3, -4, 6), (1, -2, 3, -4, 7), (1, -2, 3, -4, -8), (1, -2, -3, 4, -5), (1, -2, -3, 4, 6), (1, -2, -3,4, 7), (1, -2, -3, 4, 8), (1, -2, -3, -4, 5), (1, -2, -3, -4, -6), (1, -2, -3, -4, 7), (1, -2, -3, -4, -8), (-1, 2, 3, 4, 5), (-1, 2, 3, 4, -6), (-1, 2, 3, 4, -7), (-1, 2, 3, 4, 8), (-1, 2, 3, -4, 5), (-1, 2, 3, -4, 6), (-1, 2, 3, -4, -7), (-1, 2, 3, -4, 8), (-1, 2, -3, 4, 5), (-1, 2, -3, 4, 6), (-1, 2, -3, 4, 7), (-1, 2, -3, 4, 8), (-1, 2, -3, -4, 5), (-1, 2, -3, -4, 6), (-1, 2, -3, -4, -7), (-1, 2, -3, -4, -8), (-1, -2, 3, 4, -5), (-1, -2, 3, 4, -6), (-1, -2, 3, 4, 7), (-1, -2, 3, 4, 8), (-1,-2, 3, -4, -5), (-1, -2, 3, -4, -6), (-1, -2, 3, -4, -7), (-1, -2, 3, -4, 8), (-1, -2, -3, 4, -5), (-1, -2, -3, 4, -6), (-1, -2, -3, 4, -7), (-1, -2, -3, 4, -8), (-1, -2, -3, -4, 5), (-1, -2, -3, -4,-6), (-1, -2, -3, -4, -7), (-1, -2, -3, -4, -8)]
I am not claiming that this naive approach produces an optimal representation, it seems more compact than what ANF to CNF converters produce, though.

