1
$\begingroup$

I'm re-posting this question from cstheory.SE hoping to have more luck.

I'm a computer scientist learning a bit about algebraic logic and I was wondering how knowing the algebraic semantics of a given logic might help the study of the logic itself from a computational point of view.

In particular, is there any example of a complexity (or decidability) result for the satisfiability problem for some logics that can be obtained by reasoning about its algebraic semantics?

For example, the semantics of propositional logic can be given in terms of boolean algebras. Is there any connection between them and the fact that SAT is decidable and $NP$-complete?

$\endgroup$
4
  • $\begingroup$ I know just enough about this to be dangerous, meaning that I may say things that sound like they make sense but actually don't. With that disclaimer, the closest I can get to your question is a recent study of constraint satisfaction problems arising from various universal algebras. There is a tie between the computational complexity of CSP and some algebraic properties. I recommend looking at the universal algebra literature for more. Gerhard "Have I Embarrassed Myself Yet?" Paseman, 2018.02.04. $\endgroup$ Commented Feb 5, 2018 at 5:51
  • $\begingroup$ Thanks Gerhard. Don’t you have some reference about that work about CSP that you mentioned? $\endgroup$ Commented Feb 5, 2018 at 6:00
  • $\begingroup$ I am unfamiliar with the literature. As a starting point, try papers of Ross Willard. You may want to go on an abstract hunt and check out fifty or more abstracts before you start choosing papers to read. Gerhard "Gather Search Terms While Looking" Paseman, 2018.02.04. $\endgroup$ Commented Feb 5, 2018 at 6:10
  • 1
    $\begingroup$ All CSPs are either NP-complete or in P, as shown by Bulatov arxiv.org/pdf/1703.03021.pdf and Zhuk arxiv.org/abs/1704.01914 last year $\endgroup$ Commented Feb 5, 2018 at 7:19

1 Answer 1

4
$\begingroup$

The example you gave extends as follows:

  • SAT for arbitrary lattices (meaning, is a given formula satisfiable in some lattice) is polynomial-time decidable
  • SAT for modular lattices is Turing undecidable: Freese, Ralph, Free modular lattices, Trans. Am. Math. Soc. 261, 81-91 (1980). ZBL0437.06006.
  • SAT for Boolean algebras is NP-complete

So while modular lattices are in between Boolean algebras and arbitrary lattices, they are the most complicated.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .