(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.
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.
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,
Albert Oliveras.
Information and Computation (to appear).
[ Paper
]
CONFERENCE PAPERS:
"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
]
"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
]
"Proof-producing Congruence Closure" Robert Nieuwenhuis,
Albert Oliveras.
16th International Conference on Rewriting Techniques and Applications (RTA). April 2005, Nara (Japan).
[ Paper
| BibTeX
]
"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
]
"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
]
"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
]
"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
]
"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
]