Author name cluster

Stephan Gocht

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.

15 papers

2 author rows

IJCAI Conference 2025 Conference Paper

Using Planning for Automated Testing of Video Games

Tomáš Balyo
Roman Barták
Lukáš Chrpa
Michal Červenka
Filip Dvořák
Stephan Gocht
Lukáš Lipčák
Viktor Macek

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.

PDF Details DOI

AAAI Conference 2024 Conference Paper

End-to-End Verification for Subgraph Solving

Stephan Gocht
Ciaran McCreesh
Magnus O. Myreen
Jakob Nordström
Andy Oertel
Yong Kiam Tan

Modern subgraph-finding algorithm implementations consist of thousands of lines of highly optimized code, and this complexity raises questions about their trustworthiness. Recently, some state-of-the-art subgraph solvers have been enhanced to output machine-verifiable proofs that their results are correct. While this significantly improves reliability, it is not a fully satisfactory solution, since end-users have to trust both the proof checking algorithms and the translation of the high-level graph problem into a low-level 0-1 integer linear program (ILP) used for the proofs. In this work, we present the first formally verified toolchain capable of full end-to-end verification for subgraph solving, which closes both of these trust gaps. We have built encoder frontends for various graph problems together with a 0-1 ILP (a.k.a. pseudo-Boolean) proof checker, all implemented and formally verified in the CakeML ecosystem. This toolchain is flexible and extensible, and we use it to build verified proof checkers for both decision and optimization graph problems, namely, subgraph isomorphism, maximum clique, and maximum common (connected) induced subgraph. Our experimental evaluation shows that end-to-end formal verification is now feasible for a wide range of hard graph problems.

PDF Details DOI

KR Conference 2024 Conference Paper

Planning Domain Model Acquisition from State Traces without Action Parameters

Tomáš Balyo
Martin Suda
Lukáš Chrpa
Dominik Šafránek
Stephan Gocht
Filip Dvořák
Roman Barták
G. Michael Youngblood

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.

PDF Details DOI

IJCAI Conference 2023 Conference Paper

Certified CNF Translations for Pseudo-Boolean Solving (Extended Abstract).

Stephan Gocht
Ruben Martins
Jakob Nordström
Andy Oertel

The dramatic improvements in Boolean satisfiability (SAT) solving since the turn of the millennium have made it possible to leverage conflict-driven clause learning (CDCL) solvers for many combinatorial problems in academia and industry, and the use of proof logging has played a crucial role in increasing the confidence that the results these solvers produce are correct. However, the fact that SAT proof logging is performed in conjunctive normal form (CNF) clausal format means that it has not been possible to extend guarantees of correctness to the use of SAT solvers for more expressive combinatorial paradigms, where the first step is an unverified translation of the input to CNF. In this work, we show how cutting-planes-based reasoning can provide proof logging for solvers that translate pseudo-Boolean (a. k. a. 0-1 integer linear) decision problems to CNF and then run CDCL. We are hopeful that this is just a first step towards providing a unified proof logging approach that will extend to maximum satisfiability (MaxSAT) solving and pseudo-Boolean optimization in general.

PDF Details DOI

JAIR Journal 2023 Journal Article

Certified Dominance and Symmetry Breaking for Combinatorial Optimisation

Bart Bogaerts
Stephan Gocht
Ciaran McCreesh
Jakob Nordström

Symmetry and dominance breaking can be crucial for solving hard combinatorial search and optimisation problems, but the correctness of these techniques sometimes relies on subtle arguments. For this reason, it is desirable to produce efficient, machine-verifiable certificates that solutions have been computed correctly. Building on the cutting planes proof system, we develop a certification method for optimisation problems in which symmetry and dominance breaking is easily expressible. Our experimental evaluation demonstrates that we can efficiently verify fully general symmetry breaking in Boolean satisfiability (SAT) solving, thus providing, for the first time, a unified method to certify a range of advanced SAT techniques that also includes cardinality and parity (XOR) reasoning. In addition, we apply our method to maximum clique solving and constraint programming as a proof of concept that the approach applies to a wider range of combinatorial problems.

PDF Details DOI

SAT Conference 2022 Conference Paper

Certified CNF Translations for Pseudo-Boolean Solving

Stephan Gocht
Ruben Martins
Jakob Nordström
Andy Oertel

The dramatic improvements in Boolean satisfiability (SAT) solving since the turn of the millennium have made it possible to leverage state-of-the-art conflict-driven clause learning (CDCL) solvers for many combinatorial problems in academia and industry, and the use of proof logging has played a crucial role in increasing the confidence that the results these solvers produce are correct. However, the fact that SAT proof logging is performed in conjunctive normal form (CNF) clausal format means that it has not been possible to extend guarantees of correctness to the use of SAT solvers for more expressive combinatorial paradigms, where the first step is an unverified translation of the input to CNF. In this work, we show how cutting-planes-based reasoning can provide proof logging for solvers that translate pseudo-Boolean (a. k. a. 0-1 integer linear) decision problems to CNF and then run CDCL. To support a wide range of encodings, we provide a uniform and easily extensible framework for proof logging of CNF translations. We are hopeful that this is just a first step towards providing a unified proof logging approach that will also extend to maximum satisfiability (MaxSAT) solving and pseudo-Boolean optimization in general.

Details

AAAI Conference 2022 Conference Paper

Certified Symmetry and Dominance Breaking for Combinatorial Optimisation

Bart Bogaerts
Stephan Gocht
Ciaran McCreesh
Jakob Nordström

Symmetry and dominance breaking can be crucial for solving hard combinatorial search and optimisation problems, but the correctness of these techniques sometimes relies on subtle arguments. For this reason, it is desirable to produce efficient, machine-verifiable certificates that solutions have been computed correctly. Building on the cutting planes proof system, we develop a certification method for optimisation problems in which symmetry and dominance breaking are easily expressible. Our experimental evaluation demonstrates that we can efficiently verify fully general symmetry breaking in Boolean satisfiability (SAT) solving, thus providing, for the first time, a unified method to certify a range of advanced SAT techniques that also includes XOR and cardinality reasoning. In addition, we apply our method to maximum clique solving and constraint programming as a proof of concept that the approach applies to a wider range of combinatorial problems.

PDF Details

AAAI Conference 2021 Conference Paper

Certifying Parity Reasoning Efficiently Using Pseudo-Boolean Proofs

Stephan Gocht
Jakob Nordström

The dramatic improvements in combinatorial optimization algorithms over the last decades have had a major impact in artificial intelligence, operations research, and beyond, but the output of current state-of-the-art solvers is often hard to verify and is sometimes wrong. For Boolean satisfiability (SAT) solvers proof logging has been introduced as a way to certify correctness, but the methods used seem hard to generalize to stronger paradigms. What is more, even for enhanced SAT techniques such as parity (XOR) reasoning, cardinality detection, and symmetry handling, it has remained beyond reach to design practically efficient proofs in the standard DRAT format. In this work, we show how to instead use pseudo-Boolean inequalities with extension variables to concisely justify XOR reasoning. Our experimental evaluation of a SAT solver integration shows a dramatic decrease in proof logging and verification time compared to existing DRAT methods. Since our method is a strict generalization of DRAT, and readily lends itself to expressing also 0-1 programming and even constraint programming problems, we hope this work points the way towards a unified approach for efficient machine-verifiable proofs for a rich class of combinatorial optimization paradigms.

PDF Details

AAAI Conference 2021 Conference Paper

Cutting to the Core of Pseudo-Boolean Optimization: Combining Core-Guided Search with Cutting Planes Reasoning

Jo Devriendt
Stephan Gocht
Emir Demirović
Jakob Nordström
Peter J. Stuckey

Core-guided techniques have revolutionized Boolean satisfiability approaches to optimization problems (MaxSAT), but the process at the heart of these methods, strengthening bounds on solutions by repeatedly adding cardinality constraints, remains a bottleneck. Cardinality constraints require significant work to be re-encoded to SAT, and SAT solvers are notoriously weak at cardinality reasoning. In this work, we lift core-guided search to pseudo-Boolean (PB) solvers, which deal with more general PB optimization problems and operate natively with cardinality constraints. The cutting planes method used in such solvers allows us to derive stronger cardinality constraints, which yield better updates to solution bounds, and the increased efficiency of objective function reformulation also makes it feasible to switch repeatedly between lower-bounding and upper-bounding search. A thorough evaluation on applied and crafted benchmarks shows that our core-guided PB solver significantly improves on the state of the art in pseudo-Boolean optimization.

PDF Details

AAAI Conference 2020 Conference Paper

Justifying All Differences Using Pseudo-Boolean Reasoning

Jan Elffers
Stephan Gocht
Ciaran McCreesh
Jakob Nordström

Constraint programming solvers support rich global constraints and propagators, which make them both powerful and hard to debug. In the Boolean satisﬁability community, prooflogging is the standard solution for generating trustworthy outputs, and this has become key to the social acceptability of computer-generated proofs. However, reusing this technology for constraint programming requires either much weaker propagation, or an impractical blowup in proof length. This paper demonstrates that simple, clean, and efﬁcient proof logging is still possible for the all-different constraint, through pseudo-Boolean reasoning. We explain how such proofs can be expressed and veriﬁed mechanistically, describe an implementation, and discuss the broader implications for proof logging in constraint programming.

PDF Details

IJCAI Conference 2020 Conference Paper

Subgraph Isomorphism Meets Cutting Planes: Solving With Certified Solutions

Stephan Gocht
Ciaran McCreesh
Jakob Nordström

Modern subgraph isomorphism solvers carry out sophisticated reasoning using graph invariants such as degree sequences and path counts. We show that all of this reasoning can be justified compactly using the cutting planes proofs studied in complexity theory. This allows us to extend a state of the art subgraph isomorphism enumeration solver with proof logging support, so that the solutions it outputs may be audited and verified for correctness and completeness by a simple third party tool which knows nothing about graph theory.

PDF Details DOI

IJCAI Conference 2019 Conference Paper

On Division Versus Saturation in Pseudo-Boolean Solving

Stephan Gocht
Jakob Nordström
Amir Yehudayoff

The conflict-driven clause learning (CDCL) paradigm has revolutionized SAT solving over the last two decades. Extending this approach to pseudo-Boolean (PB) solvers doing 0-1 linear programming holds the promise of further exponential improvements in theory, but intriguingly such gains have not materialized in practice. Also intriguingly, most PB extensions of CDCL use not the division rule in cutting planes as defined in [Cook et al. , '87] but instead the so-called saturation rule. To the best of our knowledge, there has been no study comparing the strengths of division and saturation in the context of conflict-driven PB learning, when all linear combinations of inequalities are required to cancel variables. We show that PB solvers with division instead of saturation can be exponentially stronger. In the other direction, we prove that simulating a single saturation step can require an exponential number of divisions. We also perform some experiments to see whether these phenomena can be observed in actual solvers. Our conclusion is that a careful combination of division and saturation seems to be crucial to harness more of the power of cutting planes.

PDF Details

SAT Conference 2018 Conference Paper

In Between Resolution and Cutting Planes: A Study of Proof Systems for Pseudo-Boolean SAT Solving

Marc Vinyals
Jan Elffers
Jesús Giráldez-Cru
Stephan Gocht
Jakob Nordström

Abstract We initiate a proof complexity theoretic study of subsystems of cutting planes (CP) modelling proof search in conflict-driven pseudo-Boolean (PB) solvers. These algorithms combine restrictions such as that addition of constraints should always cancel a variable and/or that so-called saturation is used instead of division. It is known that on CNF inputs cutting planes with cancelling addition and saturation is essentially just resolution. We show that even if general addition is allowed, this proof system is still polynomially simulated by resolution with respect to proof size as long as coefficients are polynomially bounded. As a further way of delineating the proof power of subsystems of CP, we propose to study a number of easy (but tricky) instances of problems in NP. Most of the formulas we consider have short and simple tree-like proofs in general CP, but the restricted subsystems seem to reveal a much more varied landscape. Although we are not able to formally establish separations between different subsystems of CP—which would require major technical breakthroughs in proof complexity—these formulas appear to be good candidates for obtaining such separations. We believe that a closer study of these benchmarks is a promising approach for shedding more light on the reasoning power of pseudo-Boolean solvers.

Details

IJCAI Conference 2018 Conference Paper

Seeking Practical CDCL Insights from Theoretical SAT Benchmarks

Jan Elffers
Jesús Giráldez-Cru
Stephan Gocht
Jakob Nordström
Laurent Simon

Over the last decades Boolean satisfiability (SAT) solvers based on conflict-driven clause learning (CDCL) have developed to the point where they can handle formulas with millions of variables. Yet a deeper understanding of how these solvers can be so successful has remained elusive. In this work we shed light on CDCL performance by using theoretical benchmarks, which have the attractive features of being a) scalable, b) extremal with respect to different proof search parameters, and c) theoretically easy in the sense of having short proofs in the resolution proof system underlying CDCL. This allows for a systematic study of solver heuristics and how efficiently they search for proofs. We report results from extensive experiments on a wide range of benchmarks. Our findings include several examples where theory predicts and explains CDCL behaviour, but also raise a number of intriguing questions for further study.

PDF Details

ICAPS Conference 2017 Conference Paper

Accelerating SAT Based Planning with Incremental SAT Solving

Stephan Gocht
Tomás Balyo

One of the most successful approaches to automated planning is the translation to propositional satisfiability (SAT). We employ incremental SAT solving to increase the capabilities of several modern encodings for SAT based planning. Experiments based on benchmarks from the 2014 International Planning Competition show that an incremental approach significantly outperforms non incremental solving. Although we are using sequential scheduling of makespans, we can outperform the state-of-the-art SAT based planning system Madagascar in the number of solved instances.

Details