The Complexity of Satisfiability Problems over Finite Lattices


Bernhard Schwarz
Institut für Informatik
Julius-Maximilians-Universität Würzburg
schwarzb@informatik.uni-wuerzburg.de


Abstract:
We study the computational complexity of problems defined by formulas over fixed finite lattices. We consider evaluation, satisfiability, tautology, counting, and quantified formulas. It turns out that evaluation and tautology always can be decided in alternating logarithmic time. For satisfiability we obtain the following dichotomy result: If the lattice is distributive, satisfiability is in alternating logarithmic time. Otherwise, it is NP-complete. Counting is #P-complete for every lattice with at least two elements. For quantified formulas over non-distributive lattices we obtain PSPACE-completeness, while the problem is in alternating logarithmic time, if the lattice is distributive.