DPLL(Agg): An efficient SMT module for aggregates

The use of aggregates often allow for a compact and natural encoding of many real-life problems. FO(Agg) is an extension of first order logic (FO) with aggregates. In this paper, we present algorithms for a satisfiability checking module for aggregate expressions in the context of the DPLL(T) architecture, achieving bound consistency. We consider among others cardinality, sum and maximum aggregates. The module can be used in all DPLL-based SAT, SMT and ASP solvers. The algorithms have a low complexity. We report on the incorporation of the algorithms in Minisat and the IDP-system, including an experimental evaluation.status: publishe