It's a good question. I was asking something like this myself at lunch today.
Basically I think the issue is that SAT solvers accept stuff at a conjunctive normal form level, which is pretty far from what you'd want to use for most applications. It's more like an IR. So SAT solvers are more typically backends to higher level tools which compile to them.
If your tool offers a high level interface, one may be inclined to just call it an SMT solver. I too despite being interested in SAT, basically reach for an SMT solver even if my problem is pure boolean because of convenience.
- Z3 https://microsoft.github.io/z3guide/docs/logic/intro/ can put problems into CNF and pretty print dimacs. It contains a SAT solver, but one would probably expect a purely boolean problem to do better on the top of the line SAT-only solver like Kissat.
> If your tool offers a high level interface, one may be inclined to just call it an SMT solver. I too despite being interested in SAT, basically reach for an SMT solver even if my problem is pure boolean because of convenience.
Fortunately SMT solvers pass the problem into a SAT solver if they are simple enough, so you are probably not even trading away performance
Basically I think the issue is that SAT solvers accept stuff at a conjunctive normal form level, which is pretty far from what you'd want to use for most applications. It's more like an IR. So SAT solvers are more typically backends to higher level tools which compile to them.
If your tool offers a high level interface, one may be inclined to just call it an SMT solver. I too despite being interested in SAT, basically reach for an SMT solver even if my problem is pure boolean because of convenience.
- SAT/SMT by example is an excellent text https://smt.st/
- https://pysathq.github.io/ offers a nicer interface directly to SAT solvers
- Z3 https://microsoft.github.io/z3guide/docs/logic/intro/ can put problems into CNF and pretty print dimacs. It contains a SAT solver, but one would probably expect a purely boolean problem to do better on the top of the line SAT-only solver like Kissat.