Item


A Write-Based Solver for SAT Modulo the Theory of Arrays

The extensional theory of arrays is one of the most important ones for applications of SAT Modulo Theories (SMT) to hardware and software verification. Here we present a new T-solver for arrays in the context of the DPLL(T) approach to SMT. The main characteristics of our solver are: (i) no translation of writes into reads is needed, (ii) there is no axiom instantiation, and (iii) the T-solver interacts with the Boolean engine by asking to split on equality literals between indices. As far as we know, this is the first accurate description of an array solver integrated in a state-of-the-art SMT solver and, unlike most state-of-the-art solvers, it is not based on a lazy instantiation of the array axioms. Moreover, it is very competitive in practice, specially on problems that require heavy reasoning on array literals

© Formal Methods in Computer-Aided Design, 2008. FMCAD ’08, 2008, p.1-8

IEEE (Institute of Electrical and Electronics Engineers)

Author: Bofill Arasa, Miquel
Nieuwenhuis, Robert
Oliveras Llunell, Albert
Rodríguez Carbonell, Enric
Rubio, Albert
Date: 2008
Abstract: The extensional theory of arrays is one of the most important ones for applications of SAT Modulo Theories (SMT) to hardware and software verification. Here we present a new T-solver for arrays in the context of the DPLL(T) approach to SMT. The main characteristics of our solver are: (i) no translation of writes into reads is needed, (ii) there is no axiom instantiation, and (iii) the T-solver interacts with the Boolean engine by asking to split on equality literals between indices. As far as we know, this is the first accurate description of an array solver integrated in a state-of-the-art SMT solver and, unlike most state-of-the-art solvers, it is not based on a lazy instantiation of the array axioms. Moreover, it is very competitive in practice, specially on problems that require heavy reasoning on array literals
Format: application/pdf
ISBN: 978-1-4244-2736-9 (versió electrònica)
978-1-4244-2735-2 (versió paper)
Document access: http://hdl.handle.net/10256/8405
Language: eng
Publisher: IEEE (Institute of Electrical and Electronics Engineers)
Collection: Versió postprint del document publicat a: http://dx.doi.org/10.1109/FMCAD.2008.ECP.18
Articles publicats (D-IMA)
Is part of: © Formal Methods in Computer-Aided Design, 2008. FMCAD ’08, 2008, p.1-8
Rights: Tots els drets reservats
Subject: Algorismes computacionals
Computer algorithms
Models, Teoria dels
Model theory
Lògica matemàtica
Logic, Symbolic and mathematical
Matrius (Matemàtica)
Matrices
Title: A Write-Based Solver for SAT Modulo the Theory of Arrays
Type: info:eu-repo/semantics/article
Repository: DUGiDocs

Subjects

Authors