Does negation of Axiom of Choice imply symmetry? It seems that every construction of a model in which the Axiom of Choice fails involves some kind of symmetry. Is there an example of a construction of a model where AC fails but no argument involving symmetry appears? Is there any result that connects the negation of choice (any kind of choice) to some kind of symmetry?
 A: We have a vague idea. First let me cover the historical background for symmetries.
First one should observe that we don't actually know how to generate models of set theory. Sure, under assumptions that those models exist we can generate more, but we can't really come up with them out of nowhere. This means that most ways to generate a model of ZF would require us to already have a model and then alter it using one way or another. If we want to have "nice" models (i.e. countable transitive models) then we have two major ways of obtaining them from already existing nice models -- inner models, and adding new sets (usually generic sets). Using symmetric extensions is to do both, first we add sets then we move to an inner model of the extension.
The idea of using symmetries goes back to Fraenkel, and was then incorporated into forcing by Cohen. This idea began with ZF+Atoms, and of course we cannot separate between the atoms without the axiom of choice (they all satisfy the same formulas), so by taking only things which are definable from a small set of atoms and are impervious to most of the permutations of the atoms (namely, a large set of permutations of the atoms will not change our object) we are removing anything which can separate between the atoms. In particular we ensure that they cannot be well-ordered.
Similar approach was taken by Cohen, and is the guiding idea behind symmetric extensions by forcing. We add generic sets that from the ground model have the same properties and cannot be discerned. While atoms satisfy virtually no formula; generic sets satisfy virtually every formula. But inseparability is still there so we can do a similar trick.
Lastly relative definability is also an option, but it was proved to be essentially equivalent to symmetric extensions (under reasonable conditions) by Griegoreff. I am saying essentially because we can generate relative definability models which are not symmetric extensions, but the idea is close enough that we can think of it as the same thing.

About two years ago several prominent set theorists met in Bristol and in a few days concocted a model which is not a symmetric extension and the axiom of choice fails there. Sadly, however, no one wrote the details. I hope to reconstruct their work sometime in the next couple of years. But until then I can't give more details because I don't really have them. 
There is also a proof that if there are uncountably many measurable cardinals then Chang's model does not satisfy the axiom of choice. Chang's model is the model which is constructed when taking an $L$-like closure using an infinitary logic instead first-order logic.
While I don't know much (yet) about this process, I have been told that if we use an undefinable logic then its closure is unlikely to satisfy the axiom of choice. But I don't have too much to give about that yet, either. I should mention that this is one of the proposed topics for my Ph.D. dissertation, and I have yet to overrule it completely.
Of course sometime one can just assume that they live within a model without the axiom of choice. It is possible that this model is not a symmetric extension of any ground model, but this too is still quite an open end as far as I know. One could verify whether or not it is a symmetric extension of a set forcing (symmetries satisfy Blass' SVC) but not all class forcing symmetries do, so we can't really ensure that in the general case (if we wish to include class forcing based symmetries, that is).
All in all, I have a hard time to point out exact references and who would know to give better answers, but I have the feeling that there isn't too much that we can conclude with certainty.
A: I have an example which is not symmetric, or at least not obviously so. It is a bit advanced, so I advice searching the literature for it.
In the effective topos, which is based on recursive realizability, there are surjective functions that do not have sections. In this topos, all morphisms $\mathbb N \to \mathbb N$ are recursive functions. Therefore, there is a set of algorithms for total functions $\mathbb T$ and a surjection $s:\mathbb T \to \mathbb N^{\mathbb N}$. This surjection cannot have a section for the following reason. We can recursively decide whether two algorithms are equal. An inverse of $s$ would allow us to decide the equality of functions, which is impossible.
