2-SAT Problems in Some Multi-Valued Logics Based on Finite Lattices
Witold Charatonik, Michał Wrona · Proceedings/Proceedings - International Symposium on Multiple-Valued Logic · 2007
We prove that regular 2-SAT with signs of the form | i and J, i, where the underlying truth value set forms a lattice, is solvable in quadratic time in the size of the input, and in the case where the lattice is fixed, in linear time in the size of the formula. Moreover, we show that the satisfiability problem for 2-CNF formulas in multi-valued logics based on arbitrary De Morgan algebras may be done in time linear in the size of a formula and quadratic in the size of the underlying algebra. All algorithms we develop find satisfying valuations if they exist.