In this demonstration, we present a system that automates regression testing for video games using automated planning techniques. Traditional test scripts are a common method for testing both video games and software in general. While effective, they require manual creation and frequent updates throughout development, making the process labor-intensive. Our system eliminates this burden by automatically generating and maintaining test scripts. The test engineer only needs to define the game’s rules using the Planning Domain Definition Language (PDDL) and specify initial states and goals for individual test cases. This significantly reduces human effort while ensuring test scripts remain up to date. Additionally, our system integrates with game engine editors—supporting both Unity and Unreal to execute and evaluate test cases directly within the game. It collects detailed logs, telemetry data, and video recordings, allowing users to review test results efficiently.

Existing planning action domain model acquisition approaches consider different types of state traces from which they learn. The differences in state traces refer to the level of observability of state changes (from full to none) and whether the observations have some noise (the state changes might be inaccurately logged). However, to the best of our knowledge, all the existing approaches consider state traces in which each state change corresponds to an action specified by its name and all its parameters (all objects that are relevant to the action). Furthermore, the names and types of all the parameters of the actions to be learned are given. These assumptions are too strong. In this paper, we propose a method that learns action schema from state traces with fully observable state changes but without the parameters of actions responsible for the state changes (only action names are part of the state traces). Although we can easily deduce the number (and names) of the actions that will be in the learned domain model, we still need to deduce the number and types of the parameters of each action alongside its precondition and effects. We show that this task is at least as hard as graph isomorphism. However, our experimental evaluation on a large collection of IPC benchmarks shows that our approach is still practical as the number of required parameters is usually small. Compared to the state-of-the-art learning tools SAM and Extended SAM our new algorithm can provide better results in terms of learning action models more similar to reference models, even though it uses less information and has fewer restrictions on the input traces.

Unit propagation is the hottest path in CDCL SAT solvers, therefore the related data-structures, algorithms and implementation details are well studied and highly optimized. State-of-the-art implementations are based on reduced occurrence tracking with two watched literals per clause and one blocking literal per watcher in order to further reduce the number of clause accesses. In this paper, we show that using runtime statistics for watched literal selection can improve the performance of state-of-the-art SAT solvers. We present a method for efficiently keeping track of spans during which literals are satisfied and using this statistic to improve watcher selection. An implementation of our method in the SAT solver CaDiCaL can solve more instances of the SAT Competition 2019 and 2020 benchmark sets and is specifically strong on satisfiable cryptographic instances.

This paper presents how state-of-the-art parallel algorithms designed to solve the Satisfiability (SAT) problem can be applied in the domain of product configuration. During an interactive configuration process, a user selects features step-by-step to find a suitable configuration that fulfills his desires and the set of product constraints. A configuration system can be used to guide the user through the process by validating the selections and providing feedback. Each validation of a user selection is formulated as a SAT problem. Furthermore, an optimization problem is identified to find solutions with the minimum amount of changes compared to the previous configuration. Another additional constraint is deterministic computation, which is not trivial to achieve in well performing parallel SAT solvers. In the paper we propose five new deterministic parallel algorithms and experimentally compare them. Experiments show that reasonable speedups are achieved by using multiple threads over the sequential counterpart.

Hierarchical Task Networks (HTN) are one of the most expressive representations for automated planning problems. On the other hand, in recent years, the performance of SAT solvers has been drastically improved. To take advantage of these advances, we investigate how to encode HTN problems as SAT problems. In this paper, we propose two new encodings: GCT (Grammar-Constrained Tasks) and SMS (Stack Machine Simulation), which, contrary to previous encodings, address recursive task relationships in HTN problems. We evaluate both encodings on benchmark domains from the International Planning Competition (IPC), setting a new baseline in SAT planning on modern HTN domains.

Automatic heuristic configuration and algorithm selection can tremendously improve performance in industrial use-cases of SAT solving. In contrast to attempting to select the best heuristic for the problem, portfolio approaches in parallel SAT solving run different heuristics and even algorithms in parallel. This kind of diversification can be very successful because different heuristics and heuristic configurations have better runtimes on different problems. However, such approaches often suffer from high memory consumption. We present a parallel portfolio SAT solver that is based on several totally different branching heuristics and configurations. In contrast to similar approaches, our portfolio solver uses a shared clause database. We show how to asynchronously manage concurrent access to a shared clause database in a parallel portfolio of solvers that can also perform inprocessing.

We propose an exact algorithm for solving the longest path problem between two given vertices in undirected weighted graphs. By using graph partitioning and dynamic programming, we obtain an algorithm that is significantly faster than other state-of-the-art methods. This enables us to solve instances that were previously unsolved and solve hard instances significantly faster. We also present a parallel version of the algorithm.

One of the classical approaches to automated planning is the reduction to propositional satisfiability (SAT). Recently, it has been shown that incremental SAT solving can increase the capabilities of several modern encodings for SAT-based planning. In this paper, we present a further improvement to SAT-based planning by introducing a new algorithm named PASAR based on the principles of counterexample guided abstraction refinement (CEGAR). As an abstraction of the original problem, we use a simplified encoding where interference between actions is generally allowed. Abstract plans are converted into actual plans where possible or otherwise used as a counterexample to refine the abstraction. Using benchmark domains from recent International Planning Competitions, we compare our approach to different state-of-the-art planners and find that, in particular, combining PASAR with forward state-space search techniques leads to promising results.

Algorithm configuration tools have been successfully used to speed up local search satisfiability (SAT) solvers and other search algorithms by orders of magnitude. In this paper, we show that such tools are also very useful for generating hard SAT formulas with a planted solution, which is useful for benchmarking SAT solving algorithms and also has cryptographic applications. Our experiments with state-of-the-art local search SAT solvers show that by using this approach we can randomly generate satisfiable formulas that are considerably harder than uniform random formulas of the same size from the phase-transition region or formulas generated by state-of-the-art approaches. Additionally, we show how to generate small satisfiable formulas that are hard to solve by CDCL solvers.

We give an overview of SAT Competition 2016, the 2016 edition of thefamous competition for Boolean satisfiability (SAT) solvers with over 20 years of history. A key aim is to point out ``what's hot'' in SAT competitions in 2016, i.e., new developments in thecompetition series, including new competition tracks and new solver techniquesimplemented in some of the award-winning solvers.

The game of Sokoban is an interesting platform for algorithm research. It is hard for humans and computers alike. Even small levels can take a lot of computation for all known algorithms. In this paper we will describe how a search based Sokoban solver can be structured and which algorithms can be used to realize each critical part. We implement a variety of those, construct a number of different solvers and combine them into an algorithm portfolio. The solver we construct this way can outperform existing solvers when run in parallel, that is, our solver with 16 processors outperforms the previous sequential solvers.

Solving planning problems via translation to propositional satisfiability (SAT) is one of the most successful approaches to automated planning. An important aspect of this approach is the encoding, i.e., the construction of a propositional formula from a given planning problem instance. Numerous encoding schemes have been proposed in the recent years each aiming to outperform the previous encodings on the majority of the benchmark problems. In this paper we take a different approach. Instead of trying to develop a new encoding that is better for all kinds of benchmarks we take recently developed specialized encoding schemes and design a method to automatically select the proper encoding for a given planning problem instance. In the paper we also examine ranking heuristics for the Relaxed Relaxed Exists-Step encoding, which plays an important role in our algorithm. Experiments show that our new approach significantly outperforms the state-of-the-art encoding schemes when compared on the benchmarks of the 2011 International Planning Competition.

Satisficing planning engines are often able to generate plans in a reasonable time, however, plans are often far from optimal. Such plans often contain a high number of redundant actions, that are actions, which can be removed without affecting the validity of the plans. Existing approaches for determining and eliminating redundant actions work in polynomial time, however, do not guarantee eliminating the "best" set of redundant actions, since such a problem is NP-complete. We introduce an approach which encodes the problem of determining the "best" set of redundant actions (i.e. having the maximum total-cost) as a weighted MaxSAT problem. Moreover, we adapt the existing polynomial technique which greedily tries to eliminate an action and its dependants from the plan in order to eliminate more expensive redundant actions. The proposed approaches are empirically compared to existing approaches on plans generated by state-of-the-art planning engines on standard planning benchmarks.

Solving planning problems via translation to satisfiability (SAT) is one of the most successful approaches to automated planning. We propose a new encoding scheme which encodes a planning problem represented in the SAS+ formalism using a relaxed Exist-Step semantics of parallel actions. The encoding by design allows more actions to be put inside one parallel step than other encodings and thus a planning problem can be solved with fewer SAT solver calls. The experiments confirm this property. In several non-trivial cases the entire plans fit inside only one parallel step. In our experiments we also compared our encoding with other state-of-the-art encodings such as SASE and Rintanen's Exist-Step encoding using standard IPC benchmark domains. Our encoding can outperform both these encodings in the number of solved problems within a given limit as well as in the number of SAT solver calls needed to find a plan.

There exist planning algorithms that can quickly find sub-optimal plans even for large problems and planning algorithms finding optimal plans but only for smaller problems. In this paper we attempt to integrate both approaches. We present an anytime technique for improving plan quality, in particular for decreasing the plan make span, via substituting parts of the plan by make span-optimal sub-plans. The technique guarantees optimality, though it is primarily intended to quickly improve plan quality. We experimentally compare various approaches to local improvements and we show that our method has significantly better make span score than the SASE planner, which is one of the best optimal planners.

There exist planning algorithms that can quickly find sub-optimal plans even for large problems and planning algorithms finding optimal plans but only for smaller problems. We attempt to integrate both approaches. We present an anytime technique for improving plan quality (decreasing the plan makespan) via substituting parts of the plan by better sub-plans. The technique guarantees optimality though it is primarily intended to quickly improve plan quality. We experimentally compare various approaches to local improvements.