Author name cluster

Michael Cashmore

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

26 papers

2 author rows

ECAI Conference 2025 Conference Paper

The Subset Sum Matching Problem

Yufei Wu 0012
Manuel R. Torres
Parisa Zehtabi
Alberto Pozanco
Michael Cashmore
Daniel Borrajo
Manuela Veloso

This paper presents a new combinatorial optimisation task, the Subset Sum Matching Problem (SSMP), which is an abstraction of common financial applications such as trades reconciliation. We present three algorithms, two suboptimal and one optimal, to solve this problem. We also generate a benchmark to cover different instances of SSMP varying in complexity, and carry out an experimental evaluation to assess the performance of the approaches.

AAAI Conference 2024 Conference Paper

Accelerating Cutting-Plane Algorithms via Reinforcement Learning Surrogates

Kyle Mana
Fernando Acero
Stephen Mak
Parisa Zehtabi
Michael Cashmore
Daniele Magazzeni
Manuela Veloso

Discrete optimization belongs to the set of N P-hard problems, spanning fields such as mixed-integer programming and combinatorial optimization. A current standard approach to solving convex discrete optimization problems is the use of cutting-plane algorithms, which reach optimal solutions by iteratively adding inequalities known as cuts to refine a feasible set. Despite the existence of a number of general-purpose cut-generating algorithms, large-scale discrete optimization problems continue to suffer from intractability. In this work, we propose a method for accelerating cutting-plane algorithms via reinforcement learning. Our approach uses learned policies as surrogates for N P-hard elements of the cut generating procedure in a way that (i) accelerates convergence, and (ii) retains guarantees of optimality. We apply our method on two types of problems where cutting-plane algorithms are commonly used: stochastic optimization, and mixed-integer quadratic programming. We observe the benefits of our method when applied to Benders decomposition (stochastic optimization) and iterative loss approximation (quadratic programming), achieving up to 45% faster average convergence when compared to modern alternative algorithms.

PDF Details DOI

ECAI Conference 2024 Conference Paper

Temporal Fairness in Decision Making Problems

Manuel R. Torres
Parisa Zehtabi
Michael Cashmore
Daniele Magazzeni
Manuela Veloso

In this work we consider a new interpretation of fairness in decision making problems. Building upon existing fairness formulations, we focus on how to reason over fairness from a temporal perspective, taking into account the fairness of a history of past decisions. After introducing the concept of temporal fairness, we propose three approaches that incorporate temporal fairness in decision making problems formulated as optimization problems. We present a qualitative evaluation of our approach in four different domains and compare the solutions against a baseline approach that does not consider the temporal aspect of fairness.

ICAPS Conference 2023 Conference Paper

A Column Generation Approach to Correlated Simple Temporal Networks

Andrew Murray
Ashwin Arulselvan
Michael Cashmore
Marc Roper
Jeremy Frank

Probabilistic Simple Temporal Networks (PSTN) represent scheduling problems under temporal uncertainty. Strong controllability (SC) of PSTNs involves finding a schedule to a PSTN that maximises the probability that all constraints are satisfied (robustness). Previous approaches to this problem assume independence of probabilistic durations, and approximate the risk by bounding it above using Boole’s inequality. This gives no guarantee of finding the schedule optimising robustness, and fails to consider correlations between probabilistic durations that frequently arise in practical applications. In this paper, we formally define the Correlated Simple Temporal Network (Corr-STN) which generalises the PSTN by removing the restriction of independence. We show that the problem of Corr-STN SC is convex for a large class of multivariate (log-concave) distributions. We then introduce an algorithm capable of finding optimal SC schedules to Corr-STNs, using the column generation method. Finally, we validate our approach on a number of Corr-STNs and find that our method offers more robust solutions when compared with prior approaches.

IJCAI Conference 2023 Conference Paper

A Logic-based Explanation Generation Framework for Classical and Hybrid Planning Problems (Extended Abstract)

Stylianos Loukas Vasileiou
William Yeoh
Son Tran
Ashwin Kumar
Michael Cashmore
Daniele Magazzeni

In human-aware planning systems, a planning agent might need to explain its plan to a human user when that plan appears to be non-feasible or sub-optimal. A popular approach, called model reconciliation, has been proposed as a way to bring the model of the human user closer to the agent's model. In this paper, we approach the model reconciliation problem from a different perspective, that of knowledge representation and reasoning, and demonstrate that our approach can be applied not only to classical planning problems but also hybrid systems planning problems with durative actions and events/processes.

PDF Details DOI

JAIR Journal 2022 Journal Article

A Logic-Based Explanation Generation Framework for Classical and Hybrid Planning Problems

Stylianos Loukas Vasileiou
William Yeoh
Tran Cao Son
Ashwin Kumar
Michael Cashmore
Dianele Magazzeni

In human-aware planning systems, a planning agent might need to explain its plan to a human user when that plan appears to be non-feasible or sub-optimal. A popular approach, called model reconciliation, has been proposed as a way to bring the model of the human user closer to the agent’s model. To do so, the agent provides an explanation that can be used to update the model of human such that the agent’s plan is feasible or optimal to the human user. Existing approaches to solve this problem have been based on automated planning methods and have been limited to classical planning problems only. In this paper, we approach the model reconciliation problem from a different perspective, that of knowledge representation and reasoning, and demonstrate that our approach can be applied not only to classical planning problems but also hybrid systems planning problems with durative actions and events/processes. In particular, we propose a logic-based framework for explanation generation, where given a knowledge base KB a (of an agent) and a knowledge base KB h (of a human user), each encoding their knowledge of a planning problem, and that KB a entails a query q (e.g., that a proposed plan of the agent is valid), the goal is to identify an explanation ε ⊆ KB a such that when it is used to update KB h, then the updated KB h also entails q. More specifically, we make the following contributions in this paper: (1) We formally define the notion of logic-based explanations in the context of model reconciliation problems; (2) We introduce a number of cost functions that can be used to reflect preferences between explanations; (3) We present algorithms to compute explanations for both classical planning and hybrid systems planning problems; and (4) We empirically evaluate their performance on such problems. Our empirical results demonstrate that, on classical planning problems, our approach is faster than the state of the art when the explanations are long or when the size of the knowledge base is small (e.g., the plans to be explained are short). They also demonstrate that our approach is efficient for hybrid systems planning problems. Finally, we evaluate the real-world efficacy of explanations generated by our algorithms through a controlled human user study, where we develop a proof-of-concept visualization system and use it as a medium for explanation communication.

PDF Details DOI

SoCS Conference 2022 Conference Paper

Joint Chance Constrained Probabilistic Simple Temporal Networks via Column Generation (Extended Abstract)

Andrew Murray
Michael Cashmore
Ashwin Arulselvan
Jeremy Frank

Probabilistic Simple Temporal Networks (PSTN) are used to represent scheduling problems under uncertainty. In a temporal network that is Strongly Controllable (SC) there exists a concrete schedule that is robust to any uncertainty. We solve the problem of determining Chance Constrained PSTN SC as a Joint Chance Constrained optimisation problem via column generation, lifting the usual assumptions of independence and Boole

JAIR Journal 2021 Journal Article

Contrastive Explanations of Plans through Model Restrictions

Benjamin Krarup
Senka Krivic
Daniele Magazzeni
Derek Long
Michael Cashmore
David E. Smith

In automated planning, the need for explanations arises when there is a mismatch between a proposed plan and the user’s expectation. We frame Explainable AI Planning as an iterative plan exploration process, in which the user asks a succession of contrastive questions that lead to the generation and solution of hypothetical planning problems that are restrictions of the original problem. The object of the exploration is for the user to understand the constraints that govern the original plan and, ultimately, to arrive at a satisfactory plan. We present the results of a user study that demonstrates that when users ask questions about plans, those questions are usually contrastive, i.e. “why A rather than B?”. We use the data from this study to construct a taxonomy of user questions that often arise during plan exploration. Our approach to iterative plan exploration is a process of successive model restriction. Each contrastive user question imposes a set of constraints on the planning problem, leading to the construction of a new hypothetical planning problem as a restriction of the original. Solving this restricted problem results in a plan that can be compared with the original plan, admitting a contrastive explanation. We formally define model-based compilations in PDDL2.1 for each type of constraint derived from a contrastive user question in the taxonomy, and empirically evaluate the compilations in terms of computational complexity. The compilations were implemented as part of an explanation framework supporting iterative model restriction. We demonstrate its benefits in a second user study.

PDF Details DOI

TIME Conference 2021 Conference Paper

Efficient Anytime Computation and Execution of Decoupled Robustness Envelopes for Temporal Plans

Michael Cashmore
Alessandro Cimatti
Daniele Magazzeni
Andrea Micheli
Parisa Zehtabi

One of the major limitations for the employment of model-based planning and scheduling in practical applications is the need of costly re-planning when an incongruence between the observed reality and the formal model is encountered during execution. Robustness Envelopes characterize the set of possible contingencies that a plan is able to address without re-planning, but their exact computation is expensive; furthermore, general robustness envelopes are not amenable for efficient execution. In this paper, we present a novel, anytime algorithm to approximate Robustness Envelopes, making them scalable and executable. This is proven by an experimental analysis showing the efficiency of the algorithm, and by a concrete case study where the execution of robustness envelopes significantly reduces the number of re-plannings.

TIME Conference 2021 Conference Paper

Olisipo: A Probabilistic Approach to the Adaptable Execution of Deterministic Temporal Plans

Tomás Ribeiro
Oscar Lima
Michael Cashmore
Andrea Micheli
Rodrigo M. M. Ventura

The robust execution of a temporal plan in a perturbed environment is a problem that remains to be solved. Perturbed environments, such as the real world, are non-deterministic and filled with uncertainty. Hence, the execution of a temporal plan presents several challenges and the employed solution often consists of replanning when the execution fails. In this paper, we propose a novel algorithm, named Olisipo, which aims to maximise the probability of a successful execution of a temporal plan in perturbed environments. To achieve this, a probabilistic model is used in the execution of the plan, instead of in the building of the plan. This approach enables Olisipo to dynamically adapt the plan to changes in the environment. In addition to this, the execution of the plan is also adapted to the probability of successfully executing each action. Olisipo was compared to a simple dispatcher and it was shown that it consistently had a higher probability of successfully reaching a goal state in uncertain environments, performed fewer replans and also executed fewer actions. Hence, Olisipo offers a substantial improvement in performance for disturbed environments.

ICAPS Conference 2021 Conference Paper

Task-Aware Waypoint Sampling for Robotic Planning

Sarah Keren
Gerard Canal
Michael Cashmore

To achieve a complex task, a robot often needs to navigate in a physical space in order to complete activities in different locations. For example, it may need to inspect several structures, making multiple observations of each structure from different perspectives. Typically, the positions from which these activities can be performed are represented as waypoints – discrete positions that are sampled from the continuous physical space and used to find a task plan. Existing approaches to waypoint selection either iteratively consider the entire space or use domain knowledge to consider each activity separately. This can lead to task planning problems that are more complex than is necessary or to plans of compromised quality. Moreover, all previous approaches only consider geometric constraints that can be imposed on the waypoint selection process. We present Task-Aware Waypoint Sampling (TAWS), which offers two key novelties. First, it is an anytime approach that combines the benefits of random sampling with the use of domain knowledge in waypoint selection by performing a one-time computation of the connectivity graph from which waypoints are sampled. In addition, TAWS is the first approach that accounts for performance preferences, which are preferences a system operator may have about the generated task plan. These can account, for example, for areas near doorways where it is preferable that the robot does not stop to perform activities. We demonstrate the performance benefits of our approach on simulated automated manufacturing tasks.

AAAI Conference 2020 Conference Paper

A New Approach to Plan-Space Explanation: Analyzing Plan-Property Dependencies in Oversubscription Planning

Rebecca Eifler
Michael Cashmore
Jörg Hoffmann
Daniele Magazzeni
Marcel Steinmetz

In many usage scenarios of AI Planning technology, users will want not just a plan π but an explanation of the space of possible plans, justifying π. In particular, in oversubscription planning where not all goals can be achieved, users may ask why a conjunction A of goals is not achieved by π. We propose to answer this kind of question with the goal conjunctions B excluded by A, i. e. , that could not be achieved if A were to be enforced. We formalize this approach in terms of plan-property dependencies, where plan properties are propositional formulas over the goals achieved by a plan, and dependencies are entailment relations in plan space. We focus on entailment relations of the form g∈A g ⇒ ¬ g∈B g, and devise analysis techniques globally identifying all such relations, or locally identifying the implications of a single given plan property (user question) g∈A g. We show how, via compilation, one can analyze dependencies between a richer form of plan properties, specifying formulas over action subsets touched by the plan. We run comprehensive experiments on adapted IPC benchmarks, and ﬁnd that the suggested analyses are reasonably feasible at the global level, and become signiﬁcantly more effective at the local level.

IROS Conference 2020 Conference Paper

Intent-driven Strategic Tactical Planning for Autonomous Site Inspection using Cooperative Drones

Dorian Buksz
Anusha Mujumdar
Marin Orlic
Swarup Mohalik
Marios Daoutis
Ramamurthy Badrinath
Daniele Magazzeni
Michael Cashmore

Realization of industry-scale, goal-driven, autonomous systems with AI planning technology faces several challenges: flexibly specifying planning goal states in varying situations, synthesizing plans in large state spaces, re-planning in dynamic situations, and facilitating humans to supervise, give feedback and intervene. In this paper, we present Intent-driven Strategic Tactical Planning (ISTP) to address these challenges. We demonstrate its efficacy through its application for radio base station inspection across several locations using drones. The inspection task involves capturing images, thermal images or signal measurements - called knowledge-objects - of various components of the base stations for downstream processing. In the ISTP approach, an operator indicates her goals by flying the drone to different components of interest. These goals are generalized to capture the intent of the operator, which are then instantiated in new situations to generate goals dynamically. Towards planning and re-planning in large state spaces to achieve these goals efficiently, we extend the Strategic-Tactical Planning paradigm. All the components of ISTP are integrated in an intuitive UI and demonstrated through a real life use-case built on the UNITY simulator platform.

JAIR Journal 2020 Journal Article

Planning for Hybrid Systems via Satisfiability Modulo Theories

Michael Cashmore
Daniele Magazzeni
Parisa Zehtabi

Planning for hybrid systems is important for dealing with real-world applications, and PDDL+ supports this representation of domains with mixed discrete and continuous dynamics. In this paper we present a new approach for planning for hybrid systems, based on encoding the planning problem as a Satisfiability Modulo Theories (SMT) formula. This is the first SMT encoding that can handle the whole set of PDDL+ features (including processes and events), and is implemented in the planner SMTPlan. SMTPlan not only covers the full semantics of PDDL+, but can also deal with non-linear polynomial continuous change without discretization. This allows it to generate plans with non-linear dynamics that are correct-by-construction. The encoding is based on the notion of happenings, and can be applied on domains with nonlinear continuous change. We describe the encoding in detail and provide in-depth examples. We apply this encoding in an iterative deepening planning algorithm. Experimental results show that the approach dramatically outperforms existing work in finding plans for PDDL+ problems. We also present experiments which explore the performance of the proposed approach on temporal planning problems, showing that the scalability of the approach is limited by the size of the discrete search space. We further extend the encoding to include planning with control parameters. The extended encoding allows the definition of actions to include infinite domain parameters, called control parameters. We present experiments on a set of problems with control parameters to demonstrate the positive effect they provide to the approach of planning via SMT.

PDF Details DOI

JAIR Journal 2020 Journal Article

Using Machine Learning for Decreasing State Uncertainty in Planning

Senka Krivic
Michael Cashmore
Daniele Magazzeni
Sandor Szedmak
Justus Piater

We present a novel approach for decreasing state uncertainty in planning prior to solving the planning problem. This is done by making predictions about the state based on currently known information, using machine learning techniques. For domains where uncertainty is high, we define an active learning process for identifying which information, once sensed, will best improve the accuracy of predictions. We demonstrate that an agent is able to solve problems with uncertainties in the state with less planning effort compared to standard planning techniques. Moreover, agents can solve problems for which they could not find valid plans without using predictions. Experimental results also demonstrate that using our active learning process for identifying information to be sensed leads to gathering information that improves the prediction process.

PDF Details DOI

ICAPS Conference 2019 Conference Paper

Replanning for Situated Robots

Michael Cashmore
Andrew Coles
Bence Cserna
Erez Karpas
Daniele Magazzeni
Wheeler Ruml

Planning enables intelligent agents, such as robots, to act so as to achieve their long term goals. To make the planning process tractable, a relatively low fidelity model of the world is often used, which sometimes leads to the need to replan. The typical view of replanning is that the robot is given the current state, the goal, and possibly some data from the previous planning process. However, for robots (or teams of robots) that exist in continuous physical space, act concurrently, have deadlines, or must otherwise consider durative actions, things are not so simple. In this paper, we address the problem of replanning for situated robots. Relying on previous work on situated temporal planning, we frame the replanning problem as a situated temporal planning problem, where currently executing actions are handled via Timed Initial Literals (TILs), under the assumption that actions cannot be interrupted. We then relax this assumption, and address situated replanning with interruptible actions. We bridge the gap between the low-level model of the robot and the high-level model used for planning by the novel notion of a bail out action generator, which relies on the low-level model to generate highlevel actions that describe possible ways to interrupt currently executing actions. Because actions can be interrupted at different times during their execution, we also propose a novel algorithm to handle temporal planning with time-dependent durations.

AAAI Conference 2019 Conference Paper

Robustness Envelopes for Temporal Plans

Michael Cashmore
Alessandro Cimatti
Daniele Magazzeni
Andrea Micheli
Parisa Zehtabi

To achieve practical execution, planners must produce temporal plans with some degree of run-time adaptability. Such plans can be expressed as Simple Temporal Networks (STN), that constrain the timing of action activations, and implicitly represent the space of choices for the plan executor. A first problem is to verify that all the executor choices allowed by the STN plan will be successful, i. e. the plan is valid. An even more important problem is to assess the effect of discrepancies between the model used for planning and the execution environment. We propose an approach to compute the ”robustness envelope” (i. e. , alternative action durations or resource consumption rates) of a given STN plan, for which the plan remains valid. Plans can have boolean and numeric variables as well as discrete and continuous change. We leverage Satisfiability Modulo Theories (SMT) to make the approach formal and practical.

IROS Conference 2018 Conference Paper

Strategic-Tactical Planning for Autonomous Underwater Vehicles over Long Horizons

Dorian Buksz
Michael Cashmore
Benjamin Krarup
Daniele Magazzeni
Bram Ridder

In challenging environments where human intervention is expensive, robust and persistent autonomy is a key requirement. AI Planners can efficiently construct plans to achieve this long-term autonomous behaviour. However, in plans which are expected to last over days, or even weeks, the size of the state-space becomes too large for current planners to solve as a single problem. These problems are well-suited to decomposition and abstraction planning techniques. We present a novel approach in the context of persistent autonomy in autonomous underwater vehicles, in which tasks are complex and diverse and plans cannot be precomputed. Our approach performs a decomposition into a two-level hierarchical structure, which dynamically constructs planning problems at the upper level of the hierarchy using solution plans from the lower level. Solution plans are then executed and monitored simultaneously at both levels. We evaluate the approach, showing that compared to strictly top-down hierarchical decompositions, our approach leads to more robust solution plans of higher quality.

ICAPS Conference 2018 Conference Paper

Temporal Planning while the Clock Ticks

Michael Cashmore
Andrew Coles
Bence Cserna
Erez Karpas
Daniele Magazzeni
Wheeler Ruml

One of the original motivations for domain-independent planning was to generate plans that would then be executed in the environment. However, most existing planners ignore the passage of time during planning. While this can work well when absolute time does not play a role, this approach can lead to plans failing when there are external timing constraints, such as deadlines. In this paper, we describe a new approach for time-sensitive temporal planning. Our planner is aware of the fact that plan execution will start only once planning finishes, and incorporates this information into its decision making, in order to focus the search on branches that are more likely to lead to plans that will be feasible when the planner finishes.

IJCAI Conference 2017 Conference Paper

Decreasing Uncertainty in Planning with State Prediction

Senka Krivic
Michael Cashmore
Daniele Magazzeni
Bram Ridder
Sandor Szedmak
Justus Piater

In real world environments the state is almost never completely known. Exploration is often expensive. The application of planning in these environments is consequently more difficult and less robust. In this paper we present an approach for predicting new information about a partially-known state. The state is translated into a partially-known multigraph, which can then be extended using machine-learning techniques. We demonstrate the effectiveness of our approach, showing that it enhances the scalability of our planners, and leads to less time spent on sensing actions.

ICAPS Conference 2017 Conference Paper

Short-Term Human-Robot Interaction through Conditional Planning and Execution

Valerio Sanelli
Michael Cashmore
Daniele Magazzeni
Luca Iocchi

The deployment of robots in public environments is gaining more and more attention and interest both for the research opportunities and for the possibility of developing commercial applications over it. In these scenarios, proper definitions and implementations of human-robot interactions are crucial and the specific characteristics of the environment (in particular, the presence of untrained users) makes the task of defining and implementing effective interactions particularly challenging. In this paper, we describe a method and a fully implemented robotic system using conditional planning for generating and executing short-term interactions by a robot deployed in a public environment. To this end, the proposed method integrates and extends two components already successfully used for planning in robotics: ROSPlan and Petri Net Plans. The contributions of this paper are the problem definition of generating short-term interactions as a conditional planning problem and the description of a solution fully implemented on a real robot. The proposed method is based on the integration between a contingent planner in ROSPlan and the Petri Net Plans execution framework, and it has been tested in different scenarios where the robot interacted with hundreds of untrained users.

ICAPS Conference 2016 Conference Paper

A Compilation of the Full PDDL+ Language into SMT

Michael Cashmore
Maria Fox 0001
Derek Long
Daniele Magazzeni

Planning in hybrid systems is important for dealing with real-world applications. PDDL+ supports this representation of domains with mixed discrete and continuous dynamics, and supports events and processes modelling exogenous change. Motivated by numerous SAT-based planning approaches, we propose an approach to PDDL+ planning through SMT, describing an SMT encoding that captures all the features of the PDDL+ problem as published by Fox and Long. The encoding can be applied on domains with nonlinear continuous change. We apply this encoding in a simple planning algorithm, demonstrating excellent results on a set of benchmark problems.

ICAPS Conference 2015 Conference Paper

ROSPlan: Planning in the Robot Operating System

Michael Cashmore
Maria Fox 0001
Derek Long
Daniele Magazzeni
Bram Ridder
Arnau Carrera
Narcís Palomeras
Natàlia Hurtós

The Robot Operating System (ROS) is a set of software libraries and tools used to build robotic systems. ROS is known for a distributed and modular design. Given a model of the environment, task planning is concerned with the assembly of actions into a structure that is predicted to achieve goals. This can be done in a way that minimises costs, such as time or energy. Task planning is vital in directing the actions of a robotic agent in domains where a causal chain could lock the agent into a dead-end state. Moreover, planning can be used in less constrained domains to provide more intelligent behaviour. This paper describes the ROSP LAN framework, an architecture for embedding task planning into ROS systems. We provide a description of the architecture and a case study in autonomous robotics. Our case study involves autonomous underwater vehicles in scenarios that demonstrate the flexibility and robustness of our approach.

ICRA Conference 2014 Conference Paper

AUV mission control via temporal planning

Michael Cashmore
Maria Fox 0001
Tom Larkworthy
Derek Long
Daniele Magazzeni

Underwater installations require regular inspection and maintenance. We are exploring the idea of performing these tasks using an autonomous underwater vehicle, achieving persistent autonomous behaviour in order to avoid the need for frequent human intervention. In this paper we consider one aspect of this problem, which is the construction of a suitable plan for a single inspection tour. In particular we generate a temporal plan that optimises the time taken to complete the inspection mission. We report on physical trials with the system at the Diver and ROV driver Training Center in Fort William, Scotland, discussing some of the lessons learned.

ICAPS Conference 2013 Conference Paper

Partially Grounded Planning as Quantified Boolean Formula

Michael Cashmore
Maria Fox 0001
Enrico Giunchiglia

This paper describes a technique for translating bounded propositional reachability problems, such as Planning, into Quantified Boolean Formulae (QBF). The key feature of this translation is that the problem, and the resultant encoding is only partially grounded. The technique is applicable to other SAT or QBF encodings as an additional improvement, potentially reducing the size of the resulting formula by an exponential amount. We present experimental results showing that the approach applied to a simple SAT translation greatly improves the time taken to encode and solve problems in which there are many objects of a single type, even solving some problems that cannot be reasonably encoded as SAT.

ECAI Conference 2012 Conference Paper

Planning as Quantified Boolean Formula

Michael Cashmore
Maria Fox 0001
Enrico Giunchiglia

This paper introduces two techniques for translating bounded propositional reachability problems into Quantified Boolean Formulae (QBF). Both exploit the binary-tree structure of the QBF problem to produce encodings logarithmic in the size of the instance and thus exponentially smaller than the corresponding SAT encoding with the same bound. The first encoding is based on the iterative squaring formulation of Rintanen. The second encoding is a compact tree encoding that is more efficient than the first one, requiring fewer alternations of quantifiers and fewer variables. We present experimental results showing that the approach is feasible, although not yet competitive with current state of the art SAT-based solvers.