(Work supported by the by the project LogicTools (TIN2004-03382) funded by
the Spanish Ministry of Science and Technology and the EU program
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.
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
The solver for difference logic can be seen an extension of a
shortest-path algorithm aimed at determining, given a consistent set
of difference constraints S, all literals in the original formula that are
logically entailed by S. For each of these consequences, the solver can
compute a minimal (wrt set inclusion) subset of S from which the literal
can also be entailed. For further details see Scott Cotton and Oded Maler's paper at SAT'06: Fast and Flexible Difference Constraint Propagation for DPLL(T).
"Fast Congruence Closure and Extensions" Robert Nieuwenhuis,
Information and Computation (to appear).
"Congruence Closure with Integer Offsets" Robert Nieuwenhuis,
10th International Conference on Logic for Programming, Artificial Intelligence
and Reasoning (LPAR). September 2003, Almaty (Kazakhstan).
"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).
"Proof-producing Congruence Closure" Robert Nieuwenhuis,
16th International Conference on Rewriting Techniques and Applications (RTA). April 2005, Nara (Japan).
"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).
"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).