Can modern SAT-Solvers utilise the symmetry of First Order Logic? Apologies if the question is trivial or is wrongly stated, I am a Physicist!
Assuming that we have a universally quantified first-order logic sentence, all variables are universally quantified, defined over a finite domain $\mathcal{D}$. Then what are the most efficient ALL-SAT (algorithms that enumerate all models of a formula) algorithms in literature? In my understanding, DPLL and CDCL  based algorithms have no way of discerning symmetries which would be inherent to a grounded FOL formula.
Trivial Example:
Let the domain $\mathcal{D} = \{a,b\}$
$$\forall x F(x)$$
Then the grounding of this sentence is,
$$F(a)\land F(b)$$
So the brute force idea would be to just check all $2^{\#ground atoms}$ assignments and in this case, only {F(a): True , F(b): True} is the model. But obviously this is a trivial example, if we ground the formula for more complex sentence then, do SAT-solvers solve this as just another propositional case or are there methods to use the &quot;symmetry&quot; from the First Order sentence?
There exist first order (FO) logic systems that allow you to actually write FO constraints, and to reason with them in very intricate ways. E.g., see the IDP system.
For instance, I took a small variation of your example and coded it up in the online IDP editor:
vocabulary V{
    type D
    P(D)
}


theory T: V{
    ?x: P(x).
}


structure S:V{
    D = {a;b}
}

procedure main(){
    //stdoptions.symmetrybreaking=&quot;static&quot;
    printmodels(allmodels(T,S))
}

If you press the run button, it will print all the models (==solutions) of the FO specification, which in this case amounts to three models. The system uses a SAT solver under the hood.
Now, if you uncomment the //stdoptions.symmetrybreaking=&quot;static&quot; line, its automatic symmetry detection and breaking kicks in. Run again, and only two models will be printed, as the third is removed by symmetry breaking. Here is a reference to how this is done under the hood.
Now, can modern SAT solvers exploit this symmetry, without knowing the high level FO specification?
Not completely. The problem is that it seems hard to extract the interchangeability of first-order domain elements in the propositional logic formula. While the SAT solver typically can find permutations of variables that represent symmetries, it can not detect the particular structure of the symmetry group imposed by interchangeable FO domains. However, a succesful preprocessor for SAT solvers that partially detects FO interchangeability symmetry is described here and is available for download.