SAT and SMT Technology for Many-Valued Logics
Carlos Ansotegui, Miquel Bofill, Felip Manya and Mateu Villaret
We propose to use the SAT and SMT technology to deal with many-valued logics. Our approach is twofold. Firstly, we focus on finitely-valued logics, and extend the language of signed CNF formulas with linear integer arithmetic constraints. This way, we get a simple modeling language in which a wide range of practical combinatorial problems admit compact and natural encodings. We then define efficient translations from our language into the SAT and SMT formalisms, and propose to use SAT and SMT solvers for finding solutions.
Secondly, we show how we can use the SMT technology to build efficient automated theorem provers for infinitely-valued logics, taking Łukasiewicz infinitely-valued logic as a case study.
Keywords: Many-valued logics, Łukasiewicz infinitely-valued logic, SAT, SMT, linear integer arithmetic, linear real arithmetic, bit vectors, regular encodings