Christoph Weidenbach

Fajar Haifani, Patrick Koopmann, Sophie Tourret et al.

Abduction in description logics finds extensions of a knowledge base to make it entail an observation. As such, it can be used to explain why the observation does not follow, to repair incomplete knowledge bases, and to provide possible explanations for unexpected observations. We consider TBox abduction in the lightweight description logic EL, where the observation is a concept inclusion and the background knowledge is a TBox, i.e., a set of concept inclusions. To avoid useless answers, such problems usually come with further restrictions on the solution space and/or minimality criteria that help sort the chaff from the grain. We argue that existing minimality notions are insufficient, and introduce connection minimality. This criterion follows Occam's razor by rejecting hypotheses that use concept inclusions unrelated to the problem at hand. We show how to compute a special class of connection-minimal hypotheses in a sound and complete way. Our technique is based on a translation to first-order logic, and constructs hypotheses based on prime implicates. We evaluate a prototype implementation of our approach on ontologies from the medical domain.

Hannaneh Akrami, Alexander Mayorov, Kurt Mehlhorn et al.

SAT solving has recently been proven effective in tackling open combinatorial problems. We contribute two additional results in the context of fair distribution of indivisible goods. Specifically, we demonstrate that EFX (envy-freeness up to any good) allocations always exist for three agents and seven goods, while we provide a counterexample for the case of $n \ge 3$ agents and $m \ge n + 5$ goods. An allocation is EFX if no agent would envy the allocation of any other agent if any single item were to be removed from the other agent's bundle of goods. Each agent's preferences are modeled by a monotone valuation function on all potential bundles. After analyzing theoretical aspects of the problem, we encode the negation of the EFX instances into SAT. Satisfiability of the respective SAT formula constitute a counter-example to EFX, unsatisfiability of the respective SAT formula implies that EFX holds. The theoretical foundations of the encoding are proven correct in LEAN. For the three agents and seven goods case, we obtained a proof of unsatisfiability using SPASS-SAT of size about 30 GB in about 30 hours. It was shown to be correct by DRAT-trim. In the case of three agents and eight goods, SPASS-SAT computed satisfiability indicating a counterexample in the form of three specific agent valuations in about 20 hours. It was verified by probing all possible bundle assignments; the verification takes seconds. The extension of the counterexample to $n \ge 4$ agents and $m \ge n + 5$ goods does not involve SAT-solving. This counterexample resolves, in the negative, one of the central questions in the theory of discrete fair division.

Yasmine Briefs, Martin Bromberger, Tobias Gehl et al.

The two-watched literal scheme, a core component of efficient CDCL (Conflict-Driven Clause Learning) implementations for propositional logic, is extended to first-order logic. Given a set of first-order clauses and a set of ground literals, our lifted two-watched literal scheme efficiently detects all propagating and false clauses with respect to the ground literals. We present the algorithm as a system of rules and prove its soundness and completeness. Additionally, we provide an implementation of the two-watched literal scheme, which outperforms a standard dynamic programming approach for detecting propagatable literals and conflicts, especially when dealing with long clauses.

Martin Bromberger, Chaahat Jain, Christoph Weidenbach

We show that SCL(FOL) can simulate the derivation of non-redundant clauses by superposition for first-order logic without equality. Superposition-based reasoning is performed with respect to a fixed reduction ordering. The completeness proof of superposition relies on the grounding of the clause set. It builds a ground partial model according to the fixed ordering, where minimal false ground instances of clauses then trigger non-redundant superposition inferences. We define a respective strategy for the SCL calculus such that clauses learned by SCL and superposition inferences coincide. From this perspective the SCL calculus can be viewed as a generalization of the superposition calculus.