<p>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 <a href="https://dtai.cs.kuleuven.be/software/idp" rel="nofollow noreferrer">IDP system</a>.</p>
<p>For instance, I took a small variation of your example and <a href="http://dtai.cs.kuleuven.be/krr/idp-ide/?src=dc0e9cb57c8f39bdd30cb3d6eb0f75f0" rel="nofollow noreferrer">coded it up</a> in the online IDP editor:</p>
<pre><code>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))
}
</code></pre>
<p>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.</p>
<p>Now, if you uncomment the <code>//stdoptions.symmetrybreaking=&quot;static&quot;</code> 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. <a href="https://limo.libis.be/primo-explore/fulldisplay?docid=LIRIAS512089&amp;context=L&amp;vid=Lirias&amp;search_scope=Lirias&amp;tab=default_tab&amp;lang=en_US&amp;fromSitemap=1" rel="nofollow noreferrer">Here</a> is a reference to how this is done under the hood.</p>
<p>Now, can modern SAT solvers exploit this symmetry, without knowing the high level FO specification?</p>
<p>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 <a href="https://limo.libis.be/primo-explore/fulldisplay?docid=LIRIAS1118218&amp;context=L&amp;vid=Lirias&amp;search_scope=Lirias&amp;tab=default_tab&amp;lang=en_US&amp;fromSitemap=1" rel="nofollow noreferrer">here</a> and is available for <a href="https://bitbucket.org/krr/breakid" rel="nofollow noreferrer">download</a>.</p>

CC BY-SA 4.0
2020-07-07T21:15:06.637Z
2020-07-07T21:15:06.637Z
HolKann
<p>I take that by &quot;symmetry&quot; we are talking about reasoning over the generalities in a first-order formula instead of grounding all the possible assignments. I may be misinterpreting the question, but I'll answer anyway.</p>
<p>First off, there is some definitional inconsistency with first-order logic depending on the field. Modern automated theorem provers do not explicitly provide a domain of discourse (see the first-order problems in the TPTP problem library <a href="http://www.tptp.org" rel="nofollow noreferrer">1</a> <a href="http://www.tptp.org/cgi-bin/SeeTPTP?Category=Problems" rel="nofollow noreferrer">2</a>). They implement algorithms based upon resolution and first-order unification. This method is closely related to SAT solving since DPLL/CDCL a very efficient top-down-style implementation of the iterated resolution method.</p>
<p>Additionally, the variables are seen to range over not only base-level atoms but over the syntactic combinations of functions AND atoms. Below, you can see that we are applying the substitutions <span class="math-container">$x := S(x)$</span>, <span class="math-container">$x := S(S(x))$</span> etc. This structure is known as the <a href="https://en.wikipedia.org/wiki/Herbrand_structure" rel="nofollow noreferrer">Herbrand Universe</a> and is related to propositional grounding in <a href="https://en.wikipedia.org/wiki/Herbrand%27s_theorem" rel="nofollow noreferrer">Herbrand's Theorem</a>. The extension of SAT to include universal quantifiers but over only atomic variables is <a href="https://en.wikipedia.org/wiki/True_quantified_Boolean_formula" rel="nofollow noreferrer">QBF solving</a> - that looks more like what you're getting at with the <span class="math-container">$2^{\#groundatoms}$</span> brute force algorithm.</p>
<p>Generally speaking, in this context, it isn't possible to enumerate all models of a first-order formula. Take the simple problem <span class="math-container">$f(z) \land \Big[\forall x, f(x) \implies f(S(x)) \Big]$</span>. With repeated applications of resolution, one derives the infinite model <span class="math-container">$f(z) \land f(S(z)) \land f(S(S(z))) \land \dots$</span>.</p>
<p>That said, I think the best answer to your question is to look into resolution with first-order unification. Unification works with the inherent generalities of first-order terms and instantiates them only as much as necessary in the current logical context. However, it does form an entirely new solver; it's not the kind of thing that you can encode as-is into SAT.</p>

CC BY-SA 4.0
2020-08-13T17:54:03.847Z
2020-08-13T18:08:09.893Z
2020-08-13T18:08:09.893Z
Monty Thibault
<p>Apologies if the question is trivial or is wrongly stated, I am a Physicist!</p>
<p>Assuming that we have a universally quantified first-order logic sentence, all variables are universally quantified, defined over a finite domain <span class="math-container">$\mathcal{D}$</span>. 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.</p>
<p>Trivial Example:</p>
<p>Let the domain <span class="math-container">$\mathcal{D} = \{a,b\}$</span>
<span class="math-container">$$\forall x F(x)$$</span>
Then the grounding of this sentence is,
<span class="math-container">$$F(a)\land F(b)$$</span>
So the brute force idea would be to just check all <span class="math-container">$2^{\#ground atoms}$</span> 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?</p>

CC BY-SA 4.0
2020-07-06T22:24:26.737Z
What do you mean by the "symmetries of FOL"?
Martin Berger
CC BY-SA 4.0
2020-07-07T06:20:48.747Z
@D.W. The OP wants to enumerate all *models* of a given sentence. These are invariant under permutations.
Emil Jeřábek
CC BY-SA 4.0
2020-07-07T09:06:32.360Z
@MartinBerger I don't have a clear idea of what this symmetry could be at the propositional level. But in the fragment, I mentioned (every variable is universally quantified), the FOL formula itself entails every permutated version of itself. Intuitively to me, this should have some impact on SAT-solving.
SagarM
CC BY-SA 4.0
2020-07-07T12:49:15.090Z
@SagarM This is an interesting question. Modern CDCL probably doesn't have an *explicit* heuristic for exploiting structure coming from the translation of FOL formulae.  One approach would be, to make the back-translation from SAT to FOL smarter: once you have a model for the propositional translation of the FOL formula, you can generate all variants using symmetry. I imagine that modern SMT-solvers do look into that. Aside: adapting SAT algorithms to different classes of SAT formulae is a big research subject in SAT research. Also: maybe clarify what notion of efficiency you have in mind.
Martin Berger
<sat><first-order-logic>
Can modern SAT-Solvers utilise the symmetry of First Order Logic?
SagarM
# Can modern SAT-Solvers utilise the symmetry of First Order Logic?

(Asked by: username_0 on 2020-07-06)

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 "symmetry" from the First Order sentence?

**Tags:** sat, first-order-logic

> **Comments:**
> **username_1**: What do you mean by the "symmetries of FOL"?  
> **username_2**: @D.W. The OP wants to enumerate all *models* of a given sentence. These are invariant under permutations.  
> **username_0**: @MartinBerger I don't have a clear idea of what this symmetry could be at the propositional level. But in the fragment, I mentioned (every variable is universally quantified), the FOL formula itself entails every permutated version of itself. Intuitively to me, this should have some impact on SAT-solving.  
> **username_1**: @username_0 This is an interesting question. Modern CDCL probably doesn't have an *explicit* heuristic for exploiting structure coming from the translation of FOL formulae.  One approach would be, to make the back-translation from SAT to FOL smarter: once you have a model for the propositional translation of the FOL formula, you can generate all variants using symmetry. I imagine that modern SMT-solvers do look into that. Aside: adapting SAT algorithms to different classes of SAT formulae is a big research subject in SAT research. Also: maybe clarify what notion of efficiency you have in mind.  

---

## 2 answers

### Answer by username_3 on 2020-07-07. Score: 4

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="static"
    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="static" 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.


---

### Answer by username_4 on 2020-08-13. Score: 1

I take that by "symmetry" we are talking about reasoning over the generalities in a first-order formula instead of grounding all the possible assignments. I may be misinterpreting the question, but I'll answer anyway.

First off, there is some definitional inconsistency with first-order logic depending on the field. Modern automated theorem provers do not explicitly provide a domain of discourse (see the first-order problems in the TPTP problem library [1](http://www.tptp.org) [2](http://www.tptp.org/cgi-bin/SeeTPTP?Category=Problems)). They implement algorithms based upon resolution and first-order unification. This method is closely related to SAT solving since DPLL/CDCL a very efficient top-down-style implementation of the iterated resolution method.

Additionally, the variables are seen to range over not only base-level atoms but over the syntactic combinations of functions AND atoms. Below, you can see that we are applying the substitutions $x := S(x)$, $x := S(S(x))$ etc. This structure is known as the [Herbrand Universe](https://en.wikipedia.org/wiki/Herbrand_structure) and is related to propositional grounding in [Herbrand's Theorem](https://en.wikipedia.org/wiki/Herbrand%27s_theorem). The extension of SAT to include universal quantifiers but over only atomic variables is [QBF solving](https://en.wikipedia.org/wiki/True_quantified_Boolean_formula) - that looks more like what you're getting at with the $2^{\#groundatoms}$ brute force algorithm.

Generally speaking, in this context, it isn't possible to enumerate all models of a first-order formula. Take the simple problem $f(z) \land \Big[\forall x, f(x) \implies f(S(x)) \Big]$. With repeated applications of resolution, one derives the infinite model $f(z) \land f(S(z)) \land f(S(S(z))) \land \dots$.

That said, I think the best answer to your question is to look into resolution with first-order unification. Unification works with the inherent generalities of first-order terms and instantiates them only as much as necessary in the current logical context. However, it does form an entirely new solver; it's not the kind of thing that you can encode as-is into SAT.


---

