Browsing by Author "Conati, Ari"

Judgment aggregation (JA) offers a generic formal framework for modeling various settings involving information aggregation by social choice mechanisms. For many judgment aggregation rules, computing collective judgments is computationally notoriously hard. The central outcome determination problem, in particular, is often complete for higher levels of the polynomial hierarchy. This complexity barrier makes it challenging to develop practical, generic algorithmic approaches to outcome determination. In this work, we develop practical algorithms for outcome determination by harnessing Boolean satisfiability (SAT) based solvers as the underlying reasoning engines, under a range of the most central JA rules. For the Kemeny, Slater, MaxHamming, Young, and Dodgson rules, we detail a direct approach based on maximum satisfiability (MaxSAT) solving, using propositional logic as a declarative language. For the Reversal scoring, Condorcet, Ranked agenda, and LexiMax rules, we develop iterative SAT-based algorithms, including algorithms based on the counterexample-guided abstraction refinement (CEGAR) paradigm. The procedures we develop for these settings make use of recent advances in incremental MaxSAT solving and preferential SAT-based reasoning. We provide an open-source implementation of the algorithms, and empirically evaluate them using both real-world and synthetic preference data. We compare the performance of our implementation to a recent approach which makes use of declarative solver technology for answer set programming (ASP). The results demonstrate that our SAT-based approaches scale significantly beyond the reach of the ASP-based algorithms for all of the judgment aggregation rules considered.