A Bit-Vector Approach to Satisfiability Testing in Finitely-Valued Logics

We define a new bit-vector approach for reducing the satisfiability problem of any finitely-valued logic to SAT. Our approach consists of encoding the finitely-valued logic and the formula under consideration as an SMT program under the logic of quantifier-free uninterpreted functions and bit vectors (QF\_UFBV), and then automatically derive a SAT instance using flattening techniques and efficient CNF conversion algorithms. Moreover, we report on an experimental investigation that demonstrates that the proposed approach is competitive.Research supported by Generalitat de Catalunya grant AGAUR 2014-SGR-118, CSIC Intramural Project 201450E045, and the Ministerio de Economía y Competitividad project RASO TIN2015-71799-C2-1-P.Peer Reviewe