6 papers
Certified Branch-and-Bound MaxSAT Solving (Extended Version)
Dieter Vandesande, Jordi Coll, Bart Bogaerts
Over the past few decades, combinatorial solvers have seen remarkable performance improvements, enabling their practical use in real-world applications. In some of these applicatio…
Efficient and Reliable Hitting-Set Computations for the Implicit Hitting Set Approach
Hannes Ihalainen, Dieter Vandesande, André Schidler +3
The implicit hitting set (IHS) approach offers a general framework for solving computationally hard combinatorial optimization problems declaratively. IHS iterates between a decisi…
Preference Elicitation for Step-Wise Explanations in Logic Puzzles
Marco Foschini, Marianne Defresne, Emilio Gamba +2
Step-wise explanations can explain logic puzzles and other satisfaction problems by showing how to derive decisions step by step. Each step consists of a set of constraints that de…
Using Certifying Constraint Solvers for Generating Step-wise Explanations
Ignace Bleukx, Maarten Flippo, Bart Bogaerts +2
In the field of Explainable Constraint Solving, it is common to explain to a user why a problem is unsatisfiable. A recently proposed method for this is to compute a sequence of ex…
Certifying Pareto-Optimality in Multi-Objective Maximum Satisfiability
Christoph Jabs, Jeremias Berg, Bart Bogaerts +1
Due to the wide employment of automated reasoning in the analysis and construction of correct systems, the results reported by automated reasoning engines must be trustworthy. For…
Exploiting Symmetries in MUS Computation (Extended version)
Ignace Bleukx, Hélène Verhaeghe, Bart Bogaerts +1
In eXplainable Constraint Solving (XCS), it is common to extract a Minimal Unsatisfiable Subset (MUS) from a set of unsatisfiable constraints. This helps explain to a user why a co…