English   español  
Please use this identifier to cite or link to this item: http://hdl.handle.net/10261/155762
logo share SHARE logo core CORE   Add this article to your Mendeley library MendeleyBASE

Visualizar otros formatos: MARC | Dublin Core | RDF | ORE | MODS | METS | DIDL | DATACITE
Exportar a otros formatos:


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

AuthorsSoler, Joan Ramon ; Manyà, Felip
KeywordsMany-Valued logic
Lukasiewicz logic
Issue Date19-May-2016
PublisherInstitute of Electrical and Electronics Engineers. Computer Group
Citation2016 IEEE 46th International Symposium on Multiple-Valued Logic (ISMVL), pp. 270-275
AbstractWe 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.
Identifiersdoi: 10.1109/ISMVL.2016.47
issn: 0195623X
Appears in Collections:(IIIA) Comunicaciones congresos
Files in This Item:
File Description SizeFormat 
accesoRestringido.pdf15,38 kBAdobe PDFThumbnail
Show full item record
Review this work

WARNING: Items in Digital.CSIC are protected by copyright, with all rights reserved, unless otherwise indicated.