Abdallah Saffidine

TCS Journal 2026 Journal Article

A piecewise approach for the analysis of exact algorithms

• Katie Clinch
• Serge Gaspers
• Zixu He
• Abdallah Saffidine
• Tiankuang Zhang

To analyze the worst-case running time of branching algorithms, the majority of work in exponential time algorithms focuses on designing complicated branching rules over developing better analysis methods for simple algorithms. In the mid-$2000$s, Fomin et al. [2005] introduced measure & conquer, an advanced general analysis method, sparking widespread adoption for obtaining tighter worst-case running time upper bounds for many fundamental NP-complete problems. Yet, much potential in this direction remains untapped, as most subsequent work applied it without further advancement. Motivated by this, we present piecewise analysis, a new general method that analyzes the running time of branching algorithms. Our approach is to define a similarity ratio that divides instances into groups and then analyze the running time within each group separately. The similarity ratio is a scale between two parameters of an instance I. Instead of relying on a single measure and a single analysis for the whole instance space, our method allows to take advantage of different intrinsic properties of instances with different similarity ratios. To showcase its potential, we reanalyze two $17$-year-old algorithms from Fomin et al. [2007] that solve $4$-Coloring and #$3$-Coloring respectively. The original analysis in their paper gave running times of $O(1. 7272^n)$ and $O(1. 6262^n)$ respectively for these algorithms, our analysis improves these running times to $O(1. 7207^n)$ and $O(1. 6225^n)$.

STOC Conference 2025 Conference Paper

Refuting the Direct Sum Conjecture for Total Functions in Deterministic Communication Complexity

• Simon Mackenzie
• Abdallah Saffidine

In communication complexity the input of a function f:X×Y→Z is distributed between two players Alice and Bob. If Alice knows only x∈X and Bob only y∈Y, how much information must Alice and Bob share to be able to elicit the value of f(x,y)? Do we need ℓ more resources to solve ℓ instances of a problem? This question is the direct sum question and has been studied in many computational models. In this paper we focus on the case of 2-party deterministic communication complexity and give a counterexample to the direct sum conjecture in its strongest form. To do so we exhibit a family of functions for which the complexity of solving ℓ instances is less than (1−ϵ)ℓ times the complexity of solving one instance for some small enough ϵ>0. We use a customised method in the analysis of our family of total functions, showing that one can force the alternation of rounds between players. This idea allows us to exploit the integrality of the complexity measure to create an increasing gap between the complexity of solving the instances independently with that of solving them together.

KR Conference 2025 Conference Paper

Repairing General Game Descriptions

• Yifan He
• Munyque Mittelmann
• Aniello Murano
• Abdallah Saffidine
• Michael Thielscher

The Game Description Language (GDL) is a widely used formalism for specifying the rules of general games. Writing correct GDL descriptions can be challenging, especially for non-experts. Automated theorem proving has been proposed to assist game design by verifying if a GDL description satisfies desirable logical properties. However, when a description is proved to be faulty, the repair task itself can only be done manually. Motivated by the work on repairing unsolvable planning domain descriptions, we define a more general problem of finding minimal repairs for GDL descriptions that violate formal requirements, and we provide complexity results for various computational problems related to minimal repair. Moreover, we present an Answer Set Programming-based encoding for solving the minimal repair problem and demonstrate its application for automatically repairing ill-defined game descriptions.

NMR Workshop 2025 Conference Paper

Verification of General Games with QBF Solvers

• Yifan He 0008
• Abdallah Saffidine
• Michael Thielscher

The Game Description Language (GDL) is a lightweight formalism for representing the rules of arbitrary finite perfect information games. Its purpose is to build general game-playing systems, that is, automated players that can understand the rules of games and learn how to play them without human intervention. Coalition Logic (CL) is a logical framework capable of expressing strategic behaviors of a set of players that involve finitely many successive game states, which can formulate important properties such as whether one player can enforce a win of the game within a certain number of steps, regardless of the actions of the other players. In this paper, we investigate how to define the CL model-checking problem in the context of GGP and how to reason about CL properties of general games using Quantified Boolean Formula (QBF) solvers. This work extends our earlier AAMAS 2024 paper [1]. We evaluate the efficiency of our approach through a case study involving two-player general games and show that it has the potential to assist general game-playing agents with endgame analysis.

ECAI Conference 2024 Conference Paper

Enhancing Reinforcement Learning Through Guided Search

• Jérôme Arjonilla
• Abdallah Saffidine
• Tristan Cazenave

With the aim of improving performance in Markov Decision Problem in an Off-Policy setting, we suggest taking inspiration from what is done in Offline Reinforcement Learning (RL). In Offline RL, it is a common practice during policy learning to maintain proximity to a reference policy to mitigate uncertainty, reduce potential policy errors, and help improve performance. We find ourselves in a different setting, yet it raises questions about whether a similar concept can be applied to enhance performance i. e. , whether it is possible to find a guiding policy capable of contributing to performance improvement, and how to incorporate it into our RL agent. Our attention is particularly focused on algorithms based on Monte Carlo Tree Search (MCTS) as a guide. MCTS renowned for its state-of-the-art capabilities across various domains, catches our interest due to its ability to converge to equilibrium in single-player and two-player contexts. By harnessing the power of MCTS as a guide for our RL agent, we observed a significant performance improvement, surpassing the outcomes achieved by utilizing each method in isolation. Our experiments were carried out on the Atari 100k benchmark.

MFCS Conference 2024 Conference Paper

Generalizing Roberts' Characterization of Unit Interval Graphs

• Virginia Ardévol Martínez
• Romeo Rizzi
• Abdallah Saffidine
• Florian Sikora
• Stéphane Vialette

For any natural number d, a graph G is a (disjoint) d-interval graph if it is the intersection graph of (disjoint) d-intervals, the union of d (disjoint) intervals on the real line. Two important subclasses of d-interval graphs are unit and balanced d-interval graphs (where every interval has unit length or all the intervals associated to a same vertex have the same length, respectively). A celebrated result by Roberts gives a simple characterization of unit interval graphs being exactly claw-free interval graphs. Here, we study the generalization of this characterization for d-interval graphs. In particular, we prove that for any d ⩾ 2, if G is a K_{1, 2d+1}-free interval graph, then G is a unit d-interval graph. However, somehow surprisingly, under the same assumptions, G is not always a disjoint unit d-interval graph. This implies that the class of disjoint unit d-interval graphs is strictly included in the class of unit d-interval graphs. Finally, we study the relationships between the classes obtained under disjoint and non-disjoint d-intervals in the balanced case and show that the classes of disjoint balanced 2-intervals and balanced 2-intervals coincide, but this is no longer true for d > 2.

AAMAS Conference 2024 Conference Paper

Solving Two-player Games with QBF Solvers in General Game Playing

• Yifan He
• Abdallah Saffidine
• Michael Thielscher

Game solving is a relatively less explored area in general game playing. This paper introduces a translation from the Game Description Language GDL to Quantified Boolean Formulas (QBF) that lets us leverage QBF solvers to compute winning strategies in two-player games described in GDL. We implement this approach and measure the computation time needed by state-of-the-art QBF solvers on a range of two-player zero-sum turn-taking games. We introduce a variety of optimizations to the translation and evaluate them experimentally. Our empirical analysis establishes that our proposed approach is suitable for solving small games and can potentially help general game players evaluate endgame positions.

KR Conference 2024 Conference Paper

Verification of General Games with Imperfect Information Using Strategy Logic

• Yifan He
• Munyque Mittelmann
• Aniello Murano
• Abdallah Saffidine
• Michael Thielscher

The Game Description Language with Imperfect Information (GDL-II) is a lightweight formalism for representing the rules of arbitrary games, including those where players have private information. Its purpose is to build general game-playing systems, that is, automated players that can understand the rules of games and learn how to play them without human intervention. Epistemic Strategy Logic (SLK), on the other hand, is a rich logical framework for reasoning about multi-agent systems and the strategic behavior of agents with partial observability. To enable a general game-playing system to take advantage of this rich formalism for the automatic verification of properties of games, we present a formal translation from GDL-II to SLK models. We prove the correctness of this translation and show how crucial properties of general games, including playability and the existence of Nash equilibria, can be expressed as formulas in SLK. Finally, we demonstrate the application of an existing model-checking system for SLK to verify the properties of GDL-II games.

SAT Conference 2022 Conference Paper

QBF Programming with the Modeling Language Bule

• Jean Christoph Jung
• Valentin Mayer-Eichberger
• Abdallah Saffidine

We introduce Bule, a modeling language for problems from the complexity class PSPACE via quantified Boolean formulas (QBF) - that is, propositional formulas in which the variables are existentially or universally quantified. Bule allows the user to write a high-level representation of the problem in a natural, rule-based language, that is inspired by stratified Datalog. We implemented a tool of the same name that converts the high-level representation into DIMACS format and thus provides an interface to aribtrary QBF solvers, so that the modeled problems can also be solved. We analyze the complexity-theoretic properties of our modeling language, provide a library for common modeling patterns, and evaluate our language and tool on several examples.

JAIR Journal 2021 Journal Article

Safe Multi-Agent Pathfinding with Time Uncertainty

• Tomer Shahar
• Shashank Shekhar
• Dor Atzmon
• Abdallah Saffidine
• Brendan Juba
• Roni Stern

In many real-world scenarios, the time it takes for a mobile agent, e.g., a robot, to move from one location to another may vary due to exogenous events and be difficult to predict accurately. Planning in such scenarios is challenging, especially in the context of Multi-Agent Pathfinding (MAPF), where the goal is to find paths to multiple agents and temporal coordination is necessary to avoid collisions. In this work, we consider a MAPF problem with this form of time uncertainty, where we are only given upper and lower bounds on the time it takes each agent to move. The objective is to find a safe solution, which is a solution that can be executed by all agents and is guaranteed to avoid collisions. We propose two complete and optimal algorithms for finding safe solutions based on well-known MAPF algorithms, namely, A* with Operator Decomposition (A* + OD) and Conflict-Based Search (CBS). Experimentally, we observe that on several standard MAPF grids the CBS-based algorithm performs better. We also explore the option of online replanning in this context, i.e., modifying the agents' plans during execution, to reduce the overall execution cost. We consider two online settings: (a) when an agent can sense the current time and its current location, and (b) when the agents can also communicate seamlessly during execution. For each setting, we propose a replanning algorithm and analyze its behavior theoretically and empirically. Our experimental evaluation confirms that indeed online replanning in both settings can significantly reduce solution cost.

AIJ Journal 2020 Journal Article

Knowledge-based programs as succinct policies for partially observable domains

• Bruno Zanuttini
• Jérôme Lang
• Abdallah Saffidine
• François Schwarzentruber

We suggest to express policies for contingent planning by knowledge-based programs (KBPs). KBPs, introduced by Fagin et al. (1995) [32], are high-level protocols describing the actions that the agent should perform as a function of their current knowledge: branching conditions are epistemic formulas that are interpretable by the agent. The main aim of our paper is to show that KBPs can be seen as a succinct language for expressing policies in single-agent contingent planning. KBP are conceptually very close to languages used for expressing policies in the partially observable planning literature: like them, they have conditional and looping structures, with actions as atomic programs and Boolean formulas on beliefs for choosing the execution path. Now, the specificity of KBPs is that branching conditions refer to the belief state and not to the observations. Because of their structural proximity, KBPs and standard languages for representing policies have the same power of expressivity: every standard policy can be expressed as a KBP, and every KBP can be “unfolded” into a standard policy. However, KBPs are more succinct, more readable, and more explainable than standard policies. On the other hand, they require more online computation time, but we show that this is an unavoidable tradeoff. We study knowledge-based programs along four criteria: expressivity, succinctness, complexity of online execution, and complexity of verification.

SAT Conference 2020 Conference Paper

Positional Games and QBF: The Corrective Encoding

• Valentin Mayer-Eichberger
• Abdallah Saffidine

Abstract Positional games are a mathematical class of two-player games comprising Tic-tac-toe and its generalizations. We propose a novel encoding of these games into Quantified Boolean Formulas (QBFs) such that a game instance admits a winning strategy for first player if and only if the corresponding formula is true. Our approach improves over previous QBF encodings of games in multiple ways. First, it is generic and lets us encode other positional games, such as Hex. Second, structural properties of positional games together with a careful treatment of illegal moves let us generate more compact instances that can be solved faster by state-of-the-art QBF solvers. We establish the latter fact through extensive experiments. Finally, the compactness of our new encoding makes it feasible to translate realistic game problems. We identify a few such problems of historical significance and put them forward to the QBF community as milestones of increasing difficulty.

SoCS Conference 2018 Conference Paper

Bounded Suboptimal Game Tree Search

• Dor Atzmon
• Roni Stern
• Abdallah Saffidine

Finding the minimax value of a game is an important problem in a variety of fields, including game theory, decision theory, statistics, philosophy, economics, robotics, and security. Classical algorithms such as the Minimax algorithm can be used to find the minimax value, but require iterating over the entire game tree, which is in many cases too large. Alpha-Beta pruning identifies portions of the game tree that are not necessary for finding the minimax value, but in many cases the remaining part of the game tree is still too large to search in reasonable time. For such cases, we propose a class of algorithms that accepts a parameter e and returns a value that is guaranteed to be at most e away from the true minimax value. We lay the theoretical foundation for building such algorithms and present one such algorithm based on Alpha-Beta. Experimentally, we show that our algorithm allows controlling this runtime/solution quality tradeoff effectively.

AAAI Conference 2018 Conference Paper

Knowledge-Based Policies for Qualitative Decentralized POMDPs

• Abdallah Saffidine
• François Schwarzentruber
• Bruno Zanuttini

Qualitative Decentralized Partially Observable Markov Decision Problems (QDec-POMDPs) constitute a very general class of decision problems. They involve multiple agents, decentralized execution, sequential decision, partial observability, and uncertainty. Typically, joint policies, which prescribe to each agent an action to take depending on its full history of (local) actions and observations, are huge, which makes it difficult to store them onboard, at execution time, and also hampers the computation of joint plans. We propose and investigate a new representation for joint policies in QDec-POMDPs, which we call Multi-Agent Knowledge-Based Programs (MAKBPs), and which uses epistemic logic for compactly representing conditions on histories. Contrary to standard representations, executing an MAKBP requires reasoning at execution time, but we show that MAKBPs can be exponentially more succinct than any reactive representation.

AAAI Conference 2018 Conference Paper

Minesweeper with Limited Moves

• Serge Gaspers
• Stefan Rümmele
• Abdallah Saffidine
• Kevin Tran

We consider the problem of playing Minesweeper with a limited number of moves: Given a partially revealed board, a number of available clicks k, and a target probability p, can we win with probability p. We win if we do not click on a mine, and, after our sequence of at most k clicks (which reveal information about the neighboring squares) can correctly identify the placement of all mines. We make the assumption, that, at all times, all placements of mines consistent with the currently revealed squares are equiprobable. Our main results are that the problem is PSPACE-complete, and it remains PSPACE-complete when p is a constant, in particular when p = 1. When k = 0 (i. e. , we are not allowed to click anywhere), the problem is PP-complete in general, but co-NP-complete when p is a constant, and in particular when p = 1.

IJCAI Conference 2018 Conference Paper

The Complexity of Limited Belief Reasoning—The Quantifier-Free Case

• Yijia Chen
• Abdallah Saffidine
• Christoph Schwering

The classical view of epistemic logic is that an agent knows all the logical consequences of their knowledge base. This assumption of logical omniscience is often unrealistic and makes reasoning computationally intractable. One approach to avoid logical omniscience is to limit reasoning to a certain belief level, which intuitively measures the reasoning "depth". This paper investigates the computational complexity of reasoning with belief levels. First we show that while reasoning remains tractable if the level is constant, the complexity jumps to PSPACE-complete -- that is, beyond classical reasoning -- when the belief level is part of the input. Then we further refine the picture using parameterized complexity theory to investigate how the belief level and the number of non-logical symbols affect the complexity.

IJCAI Conference 2017 Conference Paper

Mechanisms for Online Organ Matching

• Nicholas Mattei
• Abdallah Saffidine
• Toby Walsh

Matching donations from deceased patients to patients on the waiting list account for over 85\% of all kidney transplants performed in Australia. We propose a simple mechanisms to perform this matching and compare this new mechanism with the more complex algorithm currently under consideration by the Organ and Tissue Authority in Australia. We perform a number of experiments using real world data provided by the Organ and Tissue Authority of Australia. We find that our simple mechanism is more efficient and fairer in practice compared to the other mechanism currently under consideration.

AAAI Conference 2016 Conference Paper

Nested Monte Carlo Search for Two-Player Games

• Tristan Cazenave
• Abdallah Saffidine
• Michael Schofield
• Michael Thielscher

The use of the Monte Carlo playouts as an evaluation function has proved to be a viable, general technique for searching intractable game spaces. This facilitate the use of statistical techniques like Monte Carlo Tree Search (MCTS), but is also known to require significant processing overhead. We seek to improve the quality of information extracted from the Monte Carlo playout in three ways. Firstly, by nesting the evaluation function inside another evaluation function; secondly, by measuring and utilising the depth of the playout; and thirdly, by incorporating pruning strategies that eliminate unnecessary searches and avoid traps. Our experimental data, obtained on a variety of two-player games from past General Game Playing (GGP) competitions and others, demonstrate the usefulness of these techniques in a Nested Player when pitted against a standard, optimised UCT player.

TCS Journal 2016 Journal Article

On the complexity of connection games

• Édouard Bonnet
• Florian Jamain
• Abdallah Saffidine

In this paper, we study three connection games among the most widely played: havannah, twixt, and slither. We show that determining the outcome of an arbitrary input position is PSPACE-complete in all three cases. Our reductions are based on the popular graph problem generalized geography and on hex itself. We also consider the complexity of generalizations of hex parameterized by the length of the solution and establish that while short generalized hex is W[1]-hard, short hex is FPT. Finally, we prove that the ultra-weak solution to the empty starting position in hex cannot be fully adapted to any of these three games.

JAAMAS Journal 2016 Journal Article

Positional scoring-based allocation of indivisible goods

• Dorothea Baumeister
• Sylvain Bouveret
• Abdallah Saffidine

Abstract We define a family of rules for dividing m indivisible goods among agents, parameterized by a scoring vector and a social welfare aggregation function. We assume that agents’ preferences over sets of goods are additive, but that the input is ordinal: each agent reports her preferences simply by ranking single goods. Similarly to positional scoring rules in voting, a scoring vector \(s = (s_1, \ldots, s_m)\) consists of m nonincreasing, nonnegative weights, where \(s_i\) is the score of a good assigned to an agent who ranks it in position i. The global score of an allocation for an agent is the sum of the scores of the goods assigned to her. The social welfare of an allocation is the aggregation of the scores of all agents, for some aggregation function \(\star \) such as, typically, \(+\) or \(\min \). The rule associated with s and \(\star \) maps a profile to (one of) the allocation(s) maximizing social welfare. After defining this family of rules, and focusing on some key examples, we investigate some of the social-choice-theoretic properties of this family of rules, such as various kinds of monotonicity, and separability. Finally, we focus on the computation of winning allocations, and on their approximation: we show that for commonly used scoring vectors and aggregation functions this problem is NP-hard and we exhibit some tractable particular cases.

SoCS Conference 2015 Conference Paper

A Preliminary Selection of Problems in Heuristic Search

• Carlos Linares López
• Abdallah Saffidine

The Heuristic Search community has been concentrating much effort during the last decades in solving more and more efficiently the SHORTEST PATH problem (SPP). As a result, a valuable body of scientific results has been produced, mostly in the form of heuristics and search algorithms. However, not much attention has been given to other problems even if they result from slight variations of the typical problems addressed by the community. Furthermore, other communities attempt at solving hard combinatorial problems which might be well solved with heuristic search. In this paper, an attempt is presented to introduce a preliminary selection of relevant problems that goes well beyond the classical SPP.

ECAI Conference 2014 Conference Paper

A Systematic Solution to the (De-)Composition Problem in General Game Playing

• Timothy Joseph Cerexhe
• David Rajaratnam
• Abdallah Saffidine
• Michael Thielscher

General game players can drastically reduce the cost of search if they are able to solve smaller subproblems individually and synthesise the resulting solutions. To provide a systematic solution to this (de-)composition problem, we start off with generalising the standard decomposition problem in planning by allowing the composition of individual solutions to be further constrained by domain-dependent requirements of the global planning problem. We solve this generalised problem based on a systematic analysis of composition operators for transition systems, and we demonstrate how this solution can be further generalised to general game playing.

AAAI Conference 2014 Conference Paper

Solving the Inferential Frame Problem in the General Game Description Language

• Javier Romero Davila
• Abdallah Saffidine
• Michael Thielscher

The Game Description Language GDL is the standard input language for general game-playing systems. While players can gain a lot of traction by an efficient inference algorithm for GDL, state-of-the-art reasoners suffer from a variant of a classical KR problem, the inferential frame problem. We present a method by which general game players can transform any given game description into a representation that solves this problem. Our experimental results demonstrate that with the help of automatically generated domain knowledge, a significant speedup can thus be obtained for the majority of the game descriptions from the AAAI competition.

IJCAI Conference 2013 Conference Paper

Monte Carlo *-Minimax Search

• Marc Lanctot
• Abdallah Saffidine
• Joel Veness
• Chris Archibald
• Mark H. M. Winands

This paper introduces Monte Carlo *-Minimax Search (MCMS), a Monte Carlo search algorithm for turned-based, stochastic, two-player, zero-sum games of perfect information. The algorithm is designed for the class of densely stochastic games; that is, games where one would rarely expect to sample the same successor state multiple times at any particular chance node. Our approach combines sparse sampling techniques from MDP planning with classic pruning techniques developed for adversarial expectimax planning. We compare and contrast our algorithm to the traditional *-Minimax approaches, as well as MCTS enhanced with the Double Progressive Widening, on four games: Pig, EinStein Würfelt Nicht! , Can’t Stop, and Ra. Our results show that MCMS can be competitive with enhanced MCTS variants in some domains, while consistently outperforming the equivalent classic approaches given the same amount of thinking time.

IJCAI Conference 2013 Conference Paper

On the Complexity of Trick-Taking Card Games

• Édouard Bonnet
• Florian Jamain
• Abdallah Saffidine

Determining the complexity of perfect information trick-taking card games is a long standing open problem. This question is worth addressing not only because of the popularity of these games among human players, e. g. , DOUBLE DUMMY BRIDGE, but also because of its practical importance as a building block in state-of-the-art playing engines for CON- TRACT BRIDGE, SKAT, HEARTS, and SPADES. We define a general class of perfect information twoplayer trick-taking card games dealing with arbitrary numbers of hands, suits, and suit lengths. We investigate the complexity of determining the winner in various fragments of this game class. Our main result is a proof of PSPACE-completeness for a fragment with bounded number of hands, through a reduction from Generalized Geography. Combining our results with Wästlund’s tractability results gives further insight in the complexity landscape of trick-taking card games.

TARK Conference 2013 Conference Paper

Strategic voting and the logic of knowledge

• Hans van Ditmarsch
• Jérôme Lang
• Abdallah Saffidine

We propose a general framework for strategic voting when a voter may lack knowledge about other votes or about other voters’ knowledge about her own vote. In this setting we define notions of manipulation and equilibrium. We also model action changing knowledge about votes, such as a voter revealing its preference or as a central authority performing a voting poll. Some forms of manipulation are preserved under such updates and others not. Another form of knowledge dynamics is the effect of a voter declaring its vote. We envisage Stackelberg games for uncertain profiles. The purpose of this investigation is to provide the epistemic background for the analysis and design of voting rules that incorporate uncertainty.

AAAI Conference 2012 Conference Paper

Alpha-Beta Pruning for Games with Simultaneous Moves

• Abdallah Saffidine
• Hilmar Finnsson
• Michael Buro

Alpha-Beta pruning is one of the most powerful and fundamental MiniMax search improvements. It was designed for sequential two-player zero-sum perfect information games. In this paper we introduce an Alpha-Beta-like sound pruning method for the more general class of “stacked matrix games” that allow for simultaneous moves by both players. This is accomplished by maintaining upper and lower bounds for achievable payoffs in states with simultaneous actions and dominated action pruning based on the feasibility of certain linear programs. Empirical data shows considerable savings in terms of expanded nodes compared to naive depth-first move computation without pruning.

JELIA Conference 2012 Conference Paper

Minimal Proof Search for Modal Logic K Model Checking

• Abdallah Saffidine

Abstract Most modal logics such as S5, LTL, or ATL are extensions of Modal Logic K. While the model checking problems for LTL and to a lesser extent ATL have been very active research areas for the past decades, the model checking problem for the more basic MMLK has important applications as a formal framework for perfect information multi-player games on its own. We present MPS, an effort number based algorithm solving the model checking problem for MMLK. We prove two important properties for MPS beyond its correctness. The (dis)proof exhibited by MPS is of minimal cost for a general definition of cost, and MPS is an optimal algorithm for finding (dis)proofs of minimal cost. Optimality means that any comparable algorithm either needs to explore a bigger or equal state space than MPS, or is not guaranteed to find a (dis)proof of minimal cost on every input. As such, our work relates to A* and AO* in heuristic search, to Proof Number Search and DFPN + in two-player games, and to counterexample minimization in software model checking.

ECAI Conference 2012 Conference Paper

Multiple-Outcome Proof Number Search

• Abdallah Saffidine
• Tristan Cazenave

We present Multiple-Outcome Proof Number Search (MOPNS), a Proof Number based algorithm able to prove positions in games with multiple outcomes. MOPNS is a direct generalization of Proof Number Search (PNS) in the sense that both behave exactly the same way in games with two outcomes. However, MOPNS targets a wider class of games. When a game features more than two outcomes, PNS can be used multiple times with different objectives to finally deduce the value of a position. On the contrary, MOPNS is called only once to produce the same information. We present experimental results on solving various positions of the games CONNECT FOUR and WOODPUSH showing that in most problems, the total number of node creations of MOPNS is lower than the cumulative number of node creations of PNS, even in the best case where PNS does not need to perform a binary search.

AAMAS Conference 2012 Conference Paper

Strategic voting and the logic of knowledge

• Hans van Ditmarsch
• J
• eacute; r
• ocirc; me Lang
• Abdallah Saffidine

IJCAI Conference 2011 Conference Paper

Choosing Collectively Optimal Sets of Alternatives Based on the Condorcet Criterion

• Edith Elkind
• J
• eacute; r
• ocirc; me Lang
• Abdallah Saffidine

In elections, an alternative is said to be a Condorcet winner if it is preferred to any other alternative by a majority of voters. While this is a very attractive solution concept, many elections do not have a Condorcet winner. In this paper, we propose a setvalued relaxation of this concept, which we call a Condorcet winning set: such sets consist of alternatives that collectively dominate any other alternative. We also consider a more general version of this concept, where instead of domination by a majority of voters we require domination by a given fraction theta of voters; we refer to this concept as theta-winning set. We explore social choice-theoretic and algorithmic aspects of these solution concepts, both theoretically and empirically.