Day 9
My Session Status
Sub Sessions
Many important problems from combinatorial problems to industrial domains are computationally hard and often exponential in the worst case. Yet, in practice, many instances of these problems can be solved efficiently by modern constraint solving tools.In this talk, we introduce Boolean Satisfiability (SAT) and its optimization counterpart, Maximum Satisfiability (MaxSAT), as powerful frameworks for solving decision and optimization problems. We discuss the evolution of SAT and MaxSAT solv...
A crucial trade-off in combinatorial optimization paradigms is between expressiveness and performance. SAT and its optimization variant, MaxSAT, are often regarded as having particularly restrictive syntaxes, since they are limited to boolean values and conjunctive clauses. However, solvers for these paradigms are comparatively time- and memory-efficient. This efficiency makes SAT an attractive candidate for solving a variety of combinatorial problems. SAT is also NP-complete, meaning that it...
Explainable AI (XAI) is one cornerstone of trustworthy AI. This is in part explained by the ever-increasing adoption of highly complex machine learning (ML) models in high-stakes uses of artificial intelligence (AI). Most solutions of XAI exploit subsymbolic methods of AI. Unfortunately, the use of subsymbolic methods of AI in XAI has been shown to be unworthy of trust, often yielding results that are either misleading or even erroneous. In contrast, logic-based...
How do you count the solutions to a problem when there are more of them than atoms in the universe? Model counting lives at the breathtaking confluence of logic, combinatorics, and computational hardness, and the answers are anything but obvious.This talk explores two philosophically distinct responses to this challenge: compilation-based approaches, which tame complexity by building compact representations of solution spaces, ...