Publications
Efficiently Explaining CSPs with Unsatisfiable Subset Optimization Vrije Universiteit Brussel
We build on a recently proposed method for stepwise explaining the solutions to Constraint Satisfaction Problems (CSPs) in a human understandable way. An explanation here is a sequence of simple inference steps where simplicity is quantified by a cost function. Explanation generation algorithms rely on extracting Minimal Unsatisfiable Subsets (MUSs) of a derived unsatisfiable formula, exploiting a one-to-one correspondence between so-called ...
Mathematical Foundations for Joining Only Knowing and Common Knowledge Vrije Universiteit Brussel
Simplifying Step-wise Explanation Sequences Vrije Universiteit Brussel
Certified Dominance and Symmetry Breaking for Combinatorial Optimisation Vrije Universiteit Brussel
Interactive Model Expansion in an Observable Environment Vrije Universiteit Brussel
Many practical problems can be understood as the search for a state of affairs that extends a fixed partial state of affairs, the environment, while satisfying certain conditions that are formally specified. Such problems are found in, for example, engineering, law or economics. We study this class of problems in a context where some of the relevant information about the environment is not known by the user at the start of the search. During ...
Non-deterministic Approximation Operators: Ultimate Operators, Semi-equilibrium Semantics, and Aggregates Vrije Universiteit Brussel
Symmetry and Dominance Breaking for Pseudo-Boolean Optimization Vrije Universiteit Brussel
It is well-known that highly symmetric problems can often be challenging for combinatorial search and optimization solvers. One technique to avoid this problem is to introduce so-called symmetry breaking constraints, which eliminate some symmetric parts of the search space. In this paper, we focus on pseudo-Boolean optimization problems, which are specified by a set of 0–1 integer linear inequalities (also known as pseudo-Boolean constraints) ...
Certified Core-Guided MaxSAT Solving Vrije Universiteit Brussel
In the last couple of decades, developments in SAT-based optimization have led to highly efficient maximum satisfiability (MaxSAT) solvers, but in contrast to the SAT solvers on which MaxSAT solving rests, there has been little parallel development of techniques to prove the correctness of MaxSAT results. We show how pseudo-Boolean proof logging can be used to certify state-of-the-art core-guided MaxSAT solving, including advanced techniques ...
Computing Abductive Explanations Vrije Universiteit Brussel
We study the computation of constrained explanations in the framework of abductive logic programming. A general characteristic of abductive reasoning is the existence of multiple abductive explanations. Therefore, identifying a subclass of "preferred explanations"is a relevant problem. A typical approach is to "prefer"explanations that are, in some sense, simple. Several concepts of simplicity were considered in the literature, most notably ...