Smallest Explanations and Diagnoses of Rejection in Abstract Argumentation

Deciding acceptance of arguments is a central problem in the realm of abstract argumentation. Beyond mere acceptance status, when an argument is rejected it would be informative to analyze reasons for the rejection. Recently, two complementary notions---explanations and diagnoses---were proposed for capturing underlying reasons for rejection in terms of (small) subsets of arguments or attacks. We provide tight complexity results for deciding and computing argument-based explanations and diagnoses. Computationally, we identify that smallest explanations and diagnoses for argumentation frameworks can be computed as so-called smallest unsatisfiable subsets (SMUSes) and smallest correction sets of propositional formulas. Empirically, we show that SMUS extractors and maximum satisfiability solvers (computing smallest correction sets) offer effective ways of computing smallest explanations and diagnoses.

Clausal Proof Compression

Although clausal propositional proofs are significantly smaller comparedto resolution proofs, their size is still too large for severalapplications. In this paper we present several methods to compressclausal proofs. These methods are based on a two phase approach. Thefirst phase consists of a light-weight compression algorithm that caneasily be added to satisfiability solvers that support the emissionof clausal proofs. In the second phase, we propose to use a powerfuloff-the-shelf general-purpose compression tool, such as bzip2 and7z. Sorting literals before compression facilitates a delta encoding,which combined with variable-byte encoding improves the quality of thecompression. We show that clausal proofs can be compressed by one orderof magnitude by applying both phases.

Generic CDCL -- A Formalization of Modern Propositional Satisfiability Solvers

Modern propositional satisfiability (or SAT) solvers are very powerful due to recent developments on the underlying data structures, the used heuristics to guide the search, the deduction techniques to infer knowledge, and the formula simplification techniques that are used during pre- and inprocessing. However, when all these techniques are put together, the soundness of the combined algorithm is not guaranteed any more, and understanding the complex dependencies becomes non-trivial.In this paper we present a small set of rules that allows to model modern SAT solvers in terms of a state transition system. With these rules all techniques which are applied in modern SAT solvers can be modeled adequately. Furthermore, we show that this set of rules results is sound, complete and confluent. Finnaly, we compare the proposed transition system to related systems, and show how widely used solving techniques can be modeled.

Constraint answer set solver EZCSP and why integration schemas matter

Researchers in answer set programming and constraint programming have spent significant efforts in the development of hybrid languages and solving algorithms combining the strengths of these traditionally separate fields. These efforts resulted in a new research area: constraint answer set programming. Constraint answer set programming languages and systems proved to be successful at providing declarative, yet efficient solutions to problems involving hybrid reasoning tasks. One of the main contributions of this paper is the first comprehensive account of the constraint answer set language and solver ezcsp, a mainstream representative of this research area that has been used in various successful applications. We also develop an extension of the transition systems proposed by Nieuwenhuis et al. in 2006 to capture Boolean satisfiability solvers. We use this extension to describe the ezcsp algorithm and prove formal claims about it. The design and algorithmic details behind ezcsp clearly demonstrate that the development of the hybrid systems of this kind is challenging. Many questions arise when one faces various design choices in an attempt to maximize system's benefits. One of the key decisions that a developer of a hybrid solver makes is settling on a particular integration schema within its implementation. Thus, another important contribution of this paper is a thorough case study based on ezcsp, focused on the various integration schemas that it provides.