Barcelogic for SMT



(Work supported by the by the project LogicTools (TIN2004-03382) funded by the Spanish Ministry of Science and Technology and the EU program FEDER.)

Barcelogic for SMT is the SMT-solver developed by our group at the Technical University of Catalonia. The aim of our group is the development of efficient logic-based tools, not only for verification applications (SAT, and SAT Modulo Theories), but also for other problems such as, e.g, sports scheduling or optimization problems. Currently, the active members of the group are: Miquel Bofill, Robert Nieuwenhuis, Albert Oliveras, Albert Rubio and Enric Rodríguez-Carbonell.

See the results of the 2005 SMT competition, where our SMT-solver won all four categories in which it could compete. In the 2006 SMT competition, Barcelogic came second in all categories it could compete in.

Architecture

Barcelogic for SMT is an efficient implementation of the DPLL(T) framework [
Ganzingeretal2004CAV, Nieuwenhuisetal2005LPAR]. A DPLL(T) system consists of a general DPLL(X) engine, very similar in nature to a SAT solver, whose parameter X can be instantiated with a solver for a theory T. Once the DPLL(X) engine has been implemented, this approach becomes extremely flexible: new theories can be dealt with by simply plugging in new theory solvers. These solvers only must be able to deal with conjunctions of theory literals and conform to a minimal and simple interface [Ganzingeretal2004CAV].

Currently, Barcelogic for SMT supports difference logic over the integers of the reals, equality with uninterpreted function symbols (EUF) and the interpreted function symbols predecessor and successor, or combinations of these theories. The input formulas given to the system have to be in the SMT-LIB format.

Algorithms and data structures

Barcelogic for SMT is written in C++. Apart from the parser and the CNF translator, three are the main components of the system:

Publications (in chronological order):

JOURNAL ARTICLES:

  1. "Solving SAT an SAT Modulo Theories: from an Abstract Davis-Putnam-Logemann-Loveland Procedure to DPLL(T)"
    Robert Nieuwenhuis, Albert Oliveras and Cesare Tinelli.
    Journal of the ACM (to appear). 
    [ Paper ]

  2. "Fast Congruence Closure and Extensions"
    Robert Nieuwenhuis, Albert Oliveras.
    Information and Computation (to appear). 
    [ Paper ]

CONFERENCE PAPERS:

  1. "Congruence Closure with Integer Offsets"
    Robert Nieuwenhuis, Albert Oliveras.
    10th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). September 2003, Almaty (Kazakhstan). 
    [ Paper | Slides | BibTeX ]

  2. "DPLL(T): Fast Decision Procedures"
    Harald Ganzinger, George Hagen, Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli
    16th International Conference on Computer Aided Verification (CAV), July 2004, Boston (USA).
    [ Paper | Detailed experimental results | Slides | BibTeX ]

  3. "Abstract DPLL and Abstract DPLL Modulo Theories"
    Robert Nieuwenhuis, Albert Oliveras, and Cesare Tinelli
    11th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). March 2005, Montevideo (Uruguay).
    [ Paper | Slides | BibTeX ]

  4. "Proof-producing Congruence Closure"
    Robert Nieuwenhuis, Albert Oliveras.
    16th International Conference on Rewriting Techniques and Applications (RTA). April 2005, Nara (Japan).
    [ Paper | BibTeX ]

  5. "DPLL(T) with Exhaustive Theory Propagation and its Application to Difference Logic"
    Robert Nieuwenhuis
    , Albert Oliveras.
    17th International Conference on Computer Aided Verification (CAV), July 2005, Edinburgh (Scotland).
    [ Paper | Detailed experimental results | BibTeX ]

  6. "Decision procedures for SAT, SAT Modulo Theories and Beyond. The BarcelogicTools. (Invited Paper)"
    Robert Nieuwenhuis
    , Albert Oliveras.
    12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). December 2005, Montego Bay (Jamaica).
    [ Paper | BibTeX ]

  7. "SMT Techniques for Fast Predicate Abstraction"
    Shuvendu K. Lahiri
    , Robert Nieuwenhuis and Albert Oliveras.
    18th International Conference on Computer Aided Verification (CAV), August 2006, Seattle (USA).
    [ Paper | Slides | BibTeX ]

  8. "On SAT Modulo Theories and Optimization Problems"
    Robert Nieuwenhuis
    and Albert Oliveras.
    9th International Conference on Theory and Applications of Satisfiability Testing (SAT), August 2006, Seattle (USA).
    [ Paper | BibTeX ]

  9. "Splitting on Demand in Satisfiability Modulo Theories"
    Clark Barrett
    , Robert Nieuwenhuis, Albert Oliveras and Cesare Tinelli.
    13th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). November 2006, Phnom Penh (Cambodia). 
    [ Paper | Slides | BibTeX ]

Download

An executable of the system in Linux can be downloaded
here. Executables for other platforms are available on demand.

Contact

If you have any comment or question, please contact
Albert Oliveras or Robert Nieuwenhuis.


Last modified: 10/03/2005 11:57
This page has been visited times.