<p>SAT, CP, SMT, (much of) ASP all deal with the same set of combinatorial optimisation problems.
However, they come at these problems from different angles and with different toolboxes.
These differences are largely in how each approach structures information about the exploration of the search space.
My working analogy is that SAT is machine code, while the others are higher level languages.</p>

<p>Based on my <a href="http://ora.ox.ac.uk/objects/uuid:5d641fff-4d95-43b2-9ff8-73395d782ad8" rel="noreferrer">thesis work on the structural theory of CSPs</a>, I have come to believe that the notion of "clause structure" is essential in unifying all these paradigms and in understanding how they differ.
Each clause of a SAT instance represents a forbidden partial assignment; a clause like $x_1 \lor \overline{x_2} \lor x_3$ forbids the partial assignment $\{(x_1,0),(x_2,1),(x_3,0)\}$ that simultaneously sets $x_1$ and $x_3$ to false and $x_2$ to true.
The clause structure of a combinatorial optimisation problem is its representation as a SAT instance, using some suitable encoding.
However, the clause structure includes <em>all</em> the forbidden partial assignments, not just the ones given at the start.
The clause structure is therefore usually too large to manipulate directly: typically it has at least exponential size in the number of variables, and may be infinite.
Hence, the clause structure has to be approximated with a limited amount of space.
SAT/CP/SMT/ASP maintain and update a more-or-less implicit representation of an underlying clause structure.
This is possible because if one partial assignment is known to be in the clause structure, then this implies that many other clauses are also present.
For instance, the SAT clause above also forbids any partial assignment that contains it as a subset, so clauses like $x_1 \lor \overline{x_2} \lor x_3 \lor x_4$ and $x_1 \lor \overline{x_2} \lor x_3 \lor \overline{x_4} \lor x_5$ are all in the clause structure of that instance.</p>

<p>An approximation of the clause structure is kept to narrow down the set of solutions, and to help determine whether this set is empty.
During search some partial assignments may turn out not to be contained in any solution (even if they individually satisfy each of the constraints in the instance).
These are known as <em>nogoods</em>, a term introduced by  <a href="http://dx.doi.org/10.1016/0004-3702(77)90029-7" rel="noreferrer">("Mr GNU") Stallman and Sussman</a>.
A nogood clause is therefore in the clause structure and can be included in an approximation of the clause structure, as a compact representation of many clauses that can be pruned from the search for solutions.
Adding nogoods to the approximate clause structure retains all the solutions, but better approximates those solutions.
So the approximate clause structure usually changes as search progresses.
Further, the way the problem is modelled in one of the combinatorial optimisation approaches affects the clause structure, often quite significantly.
For instance, propositional variables can represent intervals such as $x \le 5$ or points such as $x = 5$.
Hence there isn't a single general clause structure but one associated with each choice of representation, depending on what the singletons (literals) of the clause structure represent.</p>

<p><a href="https://en.wikipedia.org/wiki/Constraint_programming" rel="noreferrer">Constraint programming</a> (CP) was traditionally an AI discipline, with a focus on scheduling, timetabling, and combinatorial problems, and therefore has a central role for variables that can take more than just two values (but usually only finitely many).
CP has emphasised efficient search and, motivated by the traditional applications, has given a central role to the <a href="http://www.emn.fr/z-info/sdemasse/gccat/Calldifferent.html" rel="noreferrer"><code>all-different</code></a> (injectivity) constraint, but has also developed efficient propagators for many other kinds of constraints.
The formal definitions of CP have been around since at least Montanari's 1974 paper <a href="http://dx.doi.org/10.1016/0020-0255(74)90008-5" rel="noreferrer"><em>Networks of constraints</em></a>, with precursors going back even earlier.
This weight of history may have contributed to CP lagging behind other approaches in raw performance over the last decade.
CP classically maintains an approximation of the complement of the clause structure, via a set of active domains for the variables.
The aim is to eliminate values from the active domains, exploring the clause structure by trying to assign candidate values to variables and backtracking when necessary.</p>

<p><a href="https://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories" rel="noreferrer">Satisfiability modulo theories</a> (SMT) came out of the verification community.
Each theory in an SMT solver forms an implicit representation of potentially infinitely many SAT clauses.
The theories used with SMT and the constraints used in CP reflect their different historical applications.
Most of the theories SMT considers have to do with integer-indexed arrays, real closed fields, linear orders, and suchlike; these arise from static analysis of programs (in computer aided verification) or when formalising mathematical proofs (in automated reasoning).
In contrast, in timetabling and scheduling the injectivity constraint is central, and although the standard <a href="http://smt-lib.org/" rel="noreferrer">SMTLIB</a> language has had an injectivity constraint since its inception in 2003 (via the <code>distinct</code> symbol), until 2010 SMT solvers only implemented <code>distinct</code> via a naive algorithm.
At that stage the matching technique from the standard CP propagator for <code>all-different</code> was ported across, to great effect when applied to large lists of variables; see <a href="http://argo.matf.bg.ac.rs/publications/2010/alldiff-smt2010.pdf" rel="noreferrer"><em>An Alldifferent constraint solver in SMT</em></a> by Banković and Marić, SMT 2010.
Moreover, most CP propagators are designed for problems with finite domains, whereas standard SMT theories deal with infinite domains (integers, and more recently reals) out of the box.
SMT uses a SAT instance as the approximation of the clause structure, extracting nogood clauses from the theories as appropriate.
A nice overview is <a href="http://www.cis.upenn.edu/~alur/CIS673/smt11.pdf" rel="noreferrer"><em>Satisfiability Modulo Theories: Introduction and Applications</em></a>
by De Moura and Bjørner,
doi:<a href="http://dx.doi.org/10.1145/1995376.1995394" rel="noreferrer">10.1145/1995376.1995394</a>.</p>

<p><a href="https://en.wikipedia.org/wiki/Answer_set_programming" rel="noreferrer">Answer set programming</a> (ASP) came out of logic programming.
Due to its focus on solving the more general problem of finding a stable model, and also because it allows universal as well as existential quantification, ASP was for many years not competitive with CP or SMT.</p>

<p>Formally, SAT is CSP on Boolean domains, but the focus in SAT on clause learning, good heuristics for conflict detection, and fast ways to backtrack are quite different to the traditional CSP focus on propagators, establishing consistency, and heuristics for variable ordering.
SAT is usually extremely efficient, but for many problems huge effort is required to first express the problem as a SAT instance.
Using a higher level paradigm like CP can allow a more natural expression of the problem, and then either the CP instance can be translated into SAT by hand, or a tool can take care of the translation.
A nice overview of the nuts and bolts of SAT is <a href="http://reasoning.cs.ucla.edu/fetch.php?id=108&amp;type=pdf" rel="noreferrer"><em>On Modern Clause-Learning Satisfiability Solvers</em></a> by Pipatsrisawat and Darwiche, doi:<a href="http://dx.doi.org/10.1007/s10817-009-9156-3" rel="noreferrer">10.1007/s10817-009-9156-3</a>.</p>

<p>Now let's move on from generalities to present day specifics.</p>

<p>Over the last decade some people in CP have started to focus on lazy clause generation (LCG).
This is essentially a way to bolt CP propagators together using more flexible SMT-like techniques rather than the rather rigid active domains abstraction.
This is useful because there is a long history of published CP propagators to efficiently represent and solve many kinds of problems.
(Of course, a similar effect would be achieved by concerted effort to implement new theories for SMT solvers.)
LCG has performance that is often competitive with SMT, and for some problems it may be superior.
A quick overview is Stuckey's CPAIOR 2010 paper <a href="http://people.eng.unimelb.edu.au/pstuckey/papers/lazy.pdf" rel="noreferrer"><em>Lazy Clause Generation: Combining the power of SAT and CP (and MIP?) solving</em></a>, doi:<a href="http://dx.doi.org/10.1007/978-3-642-13520-0_3" rel="noreferrer">10.1007/978-3-642-13520-0_3</a>.
It is also worth reading the position paper of Garcia de la Banda, Stuckey, Van Hentenryck and Wallace, which paints a CP-centric vision of <a href="http://people.eng.unimelb.edu.au/pstuckey/papers/position.pdf" rel="noreferrer"><em>The Future of Optimization Technology</em></a>, doi:<a href="http://dx.doi.org/10.1007/s10601-013-9149-z" rel="noreferrer">10.1007/s10601-013-9149-z</a>.</p>

<p>As far as I can tell, much of the focus of recent SMT research seems to have shifted to applications in formal methods and formalised mathematics.  An example is reconstructing proofs found by SMT solvers inside proof systems such as <a href="http://isabelle.in.tum.de/" rel="noreferrer">Isabelle</a>/HOL, by building Isabelle/HOL tactics to reflect inference rules in SMT proof traces; see <a href="http://www4.in.tum.de/~boehmes/fast_proof_rec.html" rel="noreferrer"><em>Fast LCF-Style Proof Reconstruction for Z3</em></a> by Böhmer and Weber at ITP 2010.</p>

<p>The top ASP solvers have over the last few years been developed to become competitive with CP, SMT and SAT-only solvers.
I'm only vaguely familiar with the implementation details that have allowed solvers such as <a href="http://www.cs.uni-potsdam.de/clasp/" rel="noreferrer"><code>clasp</code></a> to be competitive so cannot really compare these with SMT and CP, but clasp explicitly advertises its focus on learning nogoods.</p>

<p>Cutting across the traditional boundaries between these formalisms is translation from more abstract problem representations into lower level efficiently implementable formalisms.
Several of the top ASP and CP solvers now explicitly translate their input into a SAT instance, which is then solved using an off-the-shelf SAT solver.
In CP, the <a href="http://savilerow.cs.st-andrews.ac.uk/" rel="noreferrer">Savile Row constraint modelling assistant</a> uses compiler design techniques to translate problems expressed in the medium level language Essence' into a lower level formalism, suitable for input to CP solvers such as <a href="http://minion.sourceforge.net/" rel="noreferrer">Minion</a> or <a href="http://www.minizinc.org/2.0/index.html" rel="noreferrer">MiniZinc</a>.
Savile Row originally worked with a CP representation as the low-level formalism but introduced SAT as a target in version 1.6.2.
Moreover, the even higher-level language <a href="http://dx.doi.org/10.1007/s10601-008-9047-y" rel="noreferrer">Essence</a> can now be automatically translated into Essence' by the <a href="https://github.com/conjure-cp/conjure" rel="noreferrer">Conjure</a> tool.
At the same time, low level SAT-only solvers like <a href="http://fmv.jku.at/lingeling/" rel="noreferrer">Lingeling</a> continue to be refined each year, most recently by alternating clause learning and in-processing phases; see the brief overview <a href="http://www.cs.utexas.edu/~marijn/publications/WhatsHot.pdf" rel="noreferrer"><em>What's Hot in the SAT and ASP Competitions</em></a> by Heule and Schaub in AAAI 2015.</p>

<p>The analogy with the history of programming languages therefore seems appropriate.
SAT is becoming a kind of "machine code", targeting a low-level model of exploration of the clauses in the clause structure.
The abstract paradigms are becoming more like higher level computer languages, with their own distinct methodologies and applications they are good at addressing.
Finally, the increasingly dense collection of links between these different layers is starting to resemble the compiler optimisation ecosystem.</p>

CC BY-SA 3.0
2015-07-21T13:12:22.220Z
Tks for this very useful answer.
Xavier Labouze
CC BY-SA 3.0
2015-07-21T16:08:01.213Z
Note: in the FOCS/STOC community a narrower definition of CSP is used.  These CSPs are of the form CSP(L), "all CSP instances that can be expressed using a fixed set L of constraint relations".  The all-different constraint doesn't fit into this framework, nor do problems that have tree-like structure.
András Salamon
CC BY-SA 4.0
2022-06-19T10:13:14.963Z
Apologies for missing the obvious, but when you say " However, the clause structure includes all the forbidden partial assignments, not just the ones given at the start.", what is meant by "the ones [partial assignments] given at the start"?
Hanno
CC BY-SA 3.0
2015-02-09T16:04:03.050Z
2017-08-08T06:44:18.257Z
2017-08-08T06:44:18.257Z
András Salamon
<p>Does someone dare to attempt to clarify what's the relation of these fields of study or perhaps even give a more concrete answer at the level of problems? Like which includes which assuming some widely accepted formulations. If I got this correctly, when you go from SAT to SMT you're basically entering the field of CSP; vice-versa, if you limit CSP to booleans you're basically talking of SAT and maybe a few related problems like #SAT. I think this much is clear (e.g. cf Kolaitis and Vardi's chapter "A Logical Approach to Constraint Satisfaction" in <em>Finite Model Theory and Its Applications</em> by Grädel et al.), but what's less clear to me is when are the constraints "modulo a theory" and when aren't they? Does SMT always imply the theory uses only equality and inequality constraints are always in the broader field of CSP? As far as I can tell, you can often introduce <a href="http://en.wikipedia.org/wiki/Slack_variable" rel="noreferrer">slack variables</a>, so the distinction [if it exists] is less than obvious.</p>

<p>The relatively recent <a href="https://books.google.com/books?id=YVSM3sxhBhcC" rel="noreferrer">"Satisfiability handbook" (IOP Press 2009)</a> gathers both SMT and CSP problems under its broad "satisfiability" umbrella, but given the way it is structured (chapters written by various authors) doesn't really help me with figuring out this. </p>

<p>I would hope the terminology gets less confusing when you talk of constraint <em>programming</em>, which (by analogy with the term ''mathematical programming'') I hope involves minimizing/maximizing some objective function. The Wikipedia article on constraint programming is alas so vague that I can't really say if this framing happens though. What I can gather from <em>Essentials of Constraint Programming</em> by
Frühwirth and Abdennadher (p. 56)  is that a "constraint solver" usually provides more than just a satisfiability checker, with simplification etc. being important in practice.</p>

<p>Although this is hardly an actual CS-theory research question, I don't expect good answers to this one on the undergraduate CS.SE site given what I saw at <a href="https://cs.stackexchange.com/questions/14946/distinguish-decision-procedure-vs-smt-solver-vs-theorem-prover-vs-constraint-sol">https://cs.stackexchange.com/questions/14946/distinguish-decision-procedure-vs-smt-solver-vs-theorem-prover-vs-constraint-sol</a> (which contains a lot of words but not what I would consider a real answer, alas).</p>

CC BY-SA 3.0
2015-02-08T17:50:31.827Z
add to this ASP. SMT/ ASP relatively recent developments. the previously separate fields are blending. see eg [Hybrid Automated Reasoning Tools: from Black-box to Clear-box Integration](http://arxiv.org/pdf/1312.6105.pdf) / Balduccini, Lierler as rough recent survey.
vzn
<soft-question><sat><terminology>
Constraint satisfaction problem (CSP) vs. satisfiability modulo theory (SMT); with a coda on constraint programming
got trolled too much this week
# Constraint satisfaction problem (CSP) vs. satisfiability modulo theory (SMT); with a coda on constraint programming

(Asked by: username_0 on 2015-02-07)

Does someone dare to attempt to clarify what's the relation of these fields of study or perhaps even give a more concrete answer at the level of problems? Like which includes which assuming some widely accepted formulations. If I got this correctly, when you go from SAT to SMT you're basically entering the field of CSP; vice-versa, if you limit CSP to booleans you're basically talking of SAT and maybe a few related problems like #SAT. I think this much is clear (e.g. cf Kolaitis and Vardi's chapter "A Logical Approach to Constraint Satisfaction" in *Finite Model Theory and Its Applications* by Grädel et al.), but what's less clear to me is when are the constraints "modulo a theory" and when aren't they? Does SMT always imply the theory uses only equality and inequality constraints are always in the broader field of CSP? As far as I can tell, you can often introduce [slack variables](http://en.wikipedia.org/wiki/Slack_variable), so the distinction [if it exists] is less than obvious.

The relatively recent ["Satisfiability handbook" (IOP Press 2009)](https://books.google.com/books?id=YVSM3sxhBhcC) gathers both SMT and CSP problems under its broad "satisfiability" umbrella, but given the way it is structured (chapters written by various authors) doesn't really help me with figuring out this.

I would hope the terminology gets less confusing when you talk of constraint *programming*, which (by analogy with the term ''mathematical programming'') I hope involves minimizing/maximizing some objective function. The Wikipedia article on constraint programming is alas so vague that I can't really say if this framing happens though. What I can gather from *Essentials of Constraint Programming* by
Frühwirth and Abdennadher (p. 56) is that a "constraint solver" usually provides more than just a satisfiability checker, with simplification etc. being important in practice.

Although this is hardly an actual CS-theory research question, I don't expect good answers to this one on the undergraduate CS.SE site given what I saw at <https://cs.stackexchange.com/questions/14946/distinguish-decision-procedure-vs-smt-solver-vs-theorem-prover-vs-constraint-sol> (which contains a lot of words but not what I would consider a real answer, alas).

**Tags:** soft-question, sat, terminology

> **Comments:**
> **username_1**: add to this ASP. SMT/ ASP relatively recent developments. the previously separate fields are blending. see eg [Hybrid Automated Reasoning Tools: from Black-box to Clear-box Integration](http://arxiv.org/pdf/1312.6105.pdf) / Balduccini, Lierler as rough recent survey.  

---

## 1 answers

### Answer by username_2 on 2015-02-09. Score: 55

SAT, CP, SMT, (much of) ASP all deal with the same set of combinatorial optimisation problems.
However, they come at these problems from different angles and with different toolboxes.
These differences are largely in how each approach structures information about the exploration of the search space.
My working analogy is that SAT is machine code, while the others are higher level languages.

Based on my [thesis work on the structural theory of CSPs](http://ora.ox.ac.uk/objects/uuid:5d641fff-4d95-43b2-9ff8-73395d782ad8), I have come to believe that the notion of "clause structure" is essential in unifying all these paradigms and in understanding how they differ.
Each clause of a SAT instance represents a forbidden partial assignment; a clause like $x\_1 \lor \overline{x\_2} \lor x\_3$ forbids the partial assignment $\{(x\_1,0),(x\_2,1),(x\_3,0)\}$ that simultaneously sets $x\_1$ and $x\_3$ to false and $x\_2$ to true.
The clause structure of a combinatorial optimisation problem is its representation as a SAT instance, using some suitable encoding.
However, the clause structure includes *all* the forbidden partial assignments, not just the ones given at the start.
The clause structure is therefore usually too large to manipulate directly: typically it has at least exponential size in the number of variables, and may be infinite.
Hence, the clause structure has to be approximated with a limited amount of space.
SAT/CP/SMT/ASP maintain and update a more-or-less implicit representation of an underlying clause structure.
This is possible because if one partial assignment is known to be in the clause structure, then this implies that many other clauses are also present.
For instance, the SAT clause above also forbids any partial assignment that contains it as a subset, so clauses like $x\_1 \lor \overline{x\_2} \lor x\_3 \lor x\_4$ and $x\_1 \lor \overline{x\_2} \lor x\_3 \lor \overline{x\_4} \lor x\_5$ are all in the clause structure of that instance.

An approximation of the clause structure is kept to narrow down the set of solutions, and to help determine whether this set is empty.
During search some partial assignments may turn out not to be contained in any solution (even if they individually satisfy each of the constraints in the instance).
These are known as *nogoods*, a term introduced by [("Mr GNU") Stallman and Sussman](http://dx.doi.org/10.1016/0004-3702(77)90029-7).
A nogood clause is therefore in the clause structure and can be included in an approximation of the clause structure, as a compact representation of many clauses that can be pruned from the search for solutions.
Adding nogoods to the approximate clause structure retains all the solutions, but better approximates those solutions.
So the approximate clause structure usually changes as search progresses.
Further, the way the problem is modelled in one of the combinatorial optimisation approaches affects the clause structure, often quite significantly.
For instance, propositional variables can represent intervals such as $x \le 5$ or points such as $x = 5$.
Hence there isn't a single general clause structure but one associated with each choice of representation, depending on what the singletons (literals) of the clause structure represent.

[Constraint programming](https://en.wikipedia.org/wiki/Constraint_programming) (CP) was traditionally an AI discipline, with a focus on scheduling, timetabling, and combinatorial problems, and therefore has a central role for variables that can take more than just two values (but usually only finitely many).
CP has emphasised efficient search and, motivated by the traditional applications, has given a central role to the [`all-different`](http://www.emn.fr/z-info/sdemasse/gccat/Calldifferent.html) (injectivity) constraint, but has also developed efficient propagators for many other kinds of constraints.
The formal definitions of CP have been around since at least Montanari's 1974 paper [*Networks of constraints*](http://dx.doi.org/10.1016/0020-0255(74)90008-5), with precursors going back even earlier.
This weight of history may have contributed to CP lagging behind other approaches in raw performance over the last decade.
CP classically maintains an approximation of the complement of the clause structure, via a set of active domains for the variables.
The aim is to eliminate values from the active domains, exploring the clause structure by trying to assign candidate values to variables and backtracking when necessary.

[Satisfiability modulo theories](https://en.wikipedia.org/wiki/Satisfiability_Modulo_Theories) (SMT) came out of the verification community.
Each theory in an SMT solver forms an implicit representation of potentially infinitely many SAT clauses.
The theories used with SMT and the constraints used in CP reflect their different historical applications.
Most of the theories SMT considers have to do with integer-indexed arrays, real closed fields, linear orders, and suchlike; these arise from static analysis of programs (in computer aided verification) or when formalising mathematical proofs (in automated reasoning).
In contrast, in timetabling and scheduling the injectivity constraint is central, and although the standard [SMTLIB](http://smt-lib.org/) language has had an injectivity constraint since its inception in 2003 (via the `distinct` symbol), until 2010 SMT solvers only implemented `distinct` via a naive algorithm.
At that stage the matching technique from the standard CP propagator for `all-different` was ported across, to great effect when applied to large lists of variables; see [*An Alldifferent constraint solver in SMT*](http://argo.matf.bg.ac.rs/publications/2010/alldiff-smt2010.pdf) by Banković and Marić, SMT 2010.
Moreover, most CP propagators are designed for problems with finite domains, whereas standard SMT theories deal with infinite domains (integers, and more recently reals) out of the box.
SMT uses a SAT instance as the approximation of the clause structure, extracting nogood clauses from the theories as appropriate.
A nice overview is [*Satisfiability Modulo Theories: Introduction and Applications*](http://www.cis.upenn.edu/~alur/CIS673/smt11.pdf)
by De Moura and Bjørner,
doi:[10.1145/1995376.1995394](http://dx.doi.org/10.1145/1995376.1995394).

[Answer set programming](https://en.wikipedia.org/wiki/Answer_set_programming) (ASP) came out of logic programming.
Due to its focus on solving the more general problem of finding a stable model, and also because it allows universal as well as existential quantification, ASP was for many years not competitive with CP or SMT.

Formally, SAT is CSP on Boolean domains, but the focus in SAT on clause learning, good heuristics for conflict detection, and fast ways to backtrack are quite different to the traditional CSP focus on propagators, establishing consistency, and heuristics for variable ordering.
SAT is usually extremely efficient, but for many problems huge effort is required to first express the problem as a SAT instance.
Using a higher level paradigm like CP can allow a more natural expression of the problem, and then either the CP instance can be translated into SAT by hand, or a tool can take care of the translation.
A nice overview of the nuts and bolts of SAT is [*On Modern Clause-Learning Satisfiability Solvers*](http://reasoning.cs.ucla.edu/fetch.php?id=108&type=pdf) by Pipatsrisawat and Darwiche, doi:[10.1007/s10817-009-9156-3](http://dx.doi.org/10.1007/s10817-009-9156-3).

Now let's move on from generalities to present day specifics.

Over the last decade some people in CP have started to focus on lazy clause generation (LCG).
This is essentially a way to bolt CP propagators together using more flexible SMT-like techniques rather than the rather rigid active domains abstraction.
This is useful because there is a long history of published CP propagators to efficiently represent and solve many kinds of problems.
(Of course, a similar effect would be achieved by concerted effort to implement new theories for SMT solvers.)
LCG has performance that is often competitive with SMT, and for some problems it may be superior.
A quick overview is Stuckey's CPAIOR 2010 paper [*Lazy Clause Generation: Combining the power of SAT and CP (and MIP?) solving*](http://people.eng.unimelb.edu.au/pstuckey/papers/lazy.pdf), doi:[10.1007/978-3-642-13520-0\_3](http://dx.doi.org/10.1007/978-3-642-13520-0_3).
It is also worth reading the position paper of Garcia de la Banda, Stuckey, Van Hentenryck and Wallace, which paints a CP-centric vision of [*The Future of Optimization Technology*](http://people.eng.unimelb.edu.au/pstuckey/papers/position.pdf), doi:[10.1007/s10601-013-9149-z](http://dx.doi.org/10.1007/s10601-013-9149-z).

As far as I can tell, much of the focus of recent SMT research seems to have shifted to applications in formal methods and formalised mathematics. An example is reconstructing proofs found by SMT solvers inside proof systems such as [Isabelle](http://isabelle.in.tum.de/)/HOL, by building Isabelle/HOL tactics to reflect inference rules in SMT proof traces; see [*Fast LCF-Style Proof Reconstruction for Z3*](http://www4.in.tum.de/~boehmes/fast_proof_rec.html) by Böhmer and Weber at ITP 2010.

The top ASP solvers have over the last few years been developed to become competitive with CP, SMT and SAT-only solvers.
I'm only vaguely familiar with the implementation details that have allowed solvers such as [`clasp`](http://www.cs.uni-potsdam.de/clasp/) to be competitive so cannot really compare these with SMT and CP, but clasp explicitly advertises its focus on learning nogoods.

Cutting across the traditional boundaries between these formalisms is translation from more abstract problem representations into lower level efficiently implementable formalisms.
Several of the top ASP and CP solvers now explicitly translate their input into a SAT instance, which is then solved using an off-the-shelf SAT solver.
In CP, the [Savile Row constraint modelling assistant](http://savilerow.cs.st-andrews.ac.uk/) uses compiler design techniques to translate problems expressed in the medium level language Essence' into a lower level formalism, suitable for input to CP solvers such as [Minion](http://minion.sourceforge.net/) or [MiniZinc](http://www.minizinc.org/2.0/index.html).
Savile Row originally worked with a CP representation as the low-level formalism but introduced SAT as a target in version 1.6.2.
Moreover, the even higher-level language [Essence](http://dx.doi.org/10.1007/s10601-008-9047-y) can now be automatically translated into Essence' by the [Conjure](https://github.com/conjure-cp/conjure) tool.
At the same time, low level SAT-only solvers like [Lingeling](http://fmv.jku.at/lingeling/) continue to be refined each year, most recently by alternating clause learning and in-processing phases; see the brief overview [*What's Hot in the SAT and ASP Competitions*](http://www.cs.utexas.edu/~marijn/publications/WhatsHot.pdf) by Heule and Schaub in AAAI 2015.

The analogy with the history of programming languages therefore seems appropriate.
SAT is becoming a kind of "machine code", targeting a low-level model of exploration of the clauses in the clause structure.
The abstract paradigms are becoming more like higher level computer languages, with their own distinct methodologies and applications they are good at addressing.
Finally, the increasingly dense collection of links between these different layers is starting to resemble the compiler optimisation ecosystem.

> **Comments:**
> **username_3**: Tks for this very useful answer.  
> **username_2**: Note: in the FOCS/STOC community a narrower definition of CSP is used.  These CSPs are of the form CSP(L), "all CSP instances that can be expressed using a fixed set L of constraint relations".  The all-different constraint doesn't fit into this framework, nor do problems that have tree-like structure.  
> **username_4**: Apologies for missing the obvious, but when you say " However, the clause structure includes all the forbidden partial assignments, not just the ones given at the start.", what is meant by "the ones [partial assignments] given at the start"?  

---

