Stephan Gocht

About Me

Hi! I am a PhD student at Lund University.

Research Interest

SAT solving
integer linear programming
proof complexity,
automated proof generation and verification
automated planning
software analysis and verification.

Publications

Elffers J, Gocht S, McCreesh C and Nordström J (2020), "Justifying All Differences Using Pseudo-Boolean Reasoning.", In Proceedings of the 34th AAAI Conference on Artificial Intelligence. , pp. to appear.

[Abstract] [BibTeX]

Abstract: Constraint programming solvers support rich global constraints and propagators, which make them both powerful and
hard to debug. In the Boolean satisfiability 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 efficient proof logging is still possible for the all-different constraint, through
pseudo-Boolean reasoning. We explain how such proofs can
be expressed and verified mechanistically, describe an implementation, and discuss the broader implications for proof logging in constraint programming.

BibTeX:

@inproceedings{Elffers2020,
  author = {Jan Elffers and Stephan Gocht and Ciaran McCreesh and Jakob Nordström},
  title = {Justifying All Differences Using Pseudo-Boolean Reasoning.},
  booktitle = {Proceedings of the 34th AAAI Conference on Artificial Intelligence},
  year = {2020},
  pages = {to appear}
}

Beckert B, Bormer T, Gocht S, Herda M, Lentzsch D and Ulbrich M (2019), "Using Relational Verification for Program Slicing", In Software Engineering and Formal Methods. SEFM 2019. Vol. 11724, pp. 353-372.

[Abstract] [BibTeX]

Abstract: Program slicing is the process of removing statements from a program such that defined aspects of its behavior are retained. For producing precise slices, i.e., slices that are minimal in size, the program's semantics must be considered. Existing approaches that go beyond a syntactical analysis and do take the semantics into account are not fully automatic and require auxiliary specifications from the user. In this paper, we adapt relational verification to check whether a slice candidate obtained by removing some instructions from a program is indeed a valid slice. Based on this, we propose a framework for precise and automatic program slicing. As part of this framework, we present three strategies for the generation of slice candidates, and we show how dynamic slicing approaches -- that interweave generating and checking slice candidates -- can be used for this purpose. The framework can easily be extended with other strategies for generating slice candidates. We discuss the strengths and weaknesses of slicing approaches that use our framework.

BibTeX:

@inproceedings{Beckert2019,
  author = {Beckert, Bernhard and Bormer, Thorsten and Gocht, Stephan and Herda, Mihai and Lentzsch, Daniel and Ulbrich, Mattias},
  title = {Using Relational Verification for Program Slicing},
  booktitle = {Software Engineering and Formal Methods. SEFM 2019},
  year = {2019},
  volume = {11724},
  pages = {353--372}
}

Gocht S, Nordström J and Yehudayoff A (2019), "On Division Versus Saturation in Pseudo-Boolean Solving", In Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI-19., 7, 2019. , pp. 1711-1718.

[Abstract] [BibTeX] [DOI] [URL]

Abstract: 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.s

BibTeX:

@inproceedings{Gocht2019,
  author = {Gocht, Stephan and Nordström, Jakob and Yehudayoff, Amir},
  title = {On Division Versus Saturation in Pseudo-Boolean Solving},
  booktitle = {Proceedings of the Twenty-Eighth International Joint Conference on Artificial Intelligence, IJCAI-19},
  year = {2019},
  pages = {1711--1718},
  url = {https://doi.org/10.24963/ijcai.2019/237},
  doi = {10.24963/ijcai.2019/237}
}

Elffers J, Giráldez-Cru J, Gocht S, Nordström J and Simon L (2018), "Seeking Practical CDCL Insights from Theoretical SAT Benchmarks.", In Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI-18. , pp. 1300-1308.

[Abstract] [BibTeX]

Abstract: 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.

BibTeX:

@inproceedings{Elffers2018,
  author = {Elffers, Jan and Giráldez-Cru, Jesús and Gocht, Stephan and Nordström, Jakob and Simon, Laurent},
  title = {Seeking Practical CDCL Insights from Theoretical SAT Benchmarks.},
  booktitle = {Proceedings of the Twenty-Seventh International Joint Conference on Artificial Intelligence, IJCAI-18},
  year = {2018},
  pages = {1300--1308}
}

Vinyals M, Elffers J, Giráldez-Cru J, Gocht S and Nordström J (2018), "In between resolution and cutting planes: a study of proof systems for pseudo-Boolean SAT solving", In Theory and Applications of Satisfiability Testing. SAT 2018.. Vol. 10929, pp. 292-310.

[Abstract] [BibTeX]

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.

BibTeX:

@inproceedings{Vinyals2018,
  author = {Vinyals, Marc and Elffers, Jan and Giráldez-Cru, Jesús and Gocht, Stephan and Nordström, Jakob},
  title = {In between resolution and cutting planes: a study of proof systems for pseudo-Boolean SAT solving},
  booktitle = {Theory and Applications of Satisfiability Testing. SAT 2018.},
  year = {2018},
  volume = {10929},
  pages = {292--310}
}

Beckert B, Bormer T, Gocht S, Herda M, Lentzsch D and Ulbrich M (2017), "SemSlice: Exploiting Relational Verification for Automatic Program Slicing", In Integrated Formal Methods. IFM 2017. Vol. 10510, pp. 312-319.

[Abstract] [BibTeX]

Abstract: We present SemSlice, a tool which automatically produces very precise slices for C routines. Slicing is the process of removing statements from a program such that defined aspects of its behavior are retained. For producing precise slices, i.e., slices that are close to the minimal number of statements, the program's semantics must be considered. SemSlice is based on automatic relational regression verification, which SemSlice uses to select valid slices from a set of candidate slices. We present several approaches for producing candidates for precise slices. Evaluation shows that regression verification (based on coupling invariant inference) is a powerful tool for semantics-aware slicing: precise slices for typical slicing challenges can be found automatically and fast.

BibTeX:

@inproceedings{beckert2017,
  author = {Beckert, Bernhard and Bormer, Thorsten and Gocht, Stephan and Herda, Mihai and Lentzsch, Daniel and Ulbrich, Mattiasg},
  title = {SemSlice: Exploiting Relational Verification for Automatic Program Slicing},
  booktitle = {Integrated Formal Methods. IFM 2017},
  year = {2017},
  volume = {10510},
  pages = {312--319}
}

Gocht S and Balyo T (2017), "Accelerating SAT Based Planning with Incremental SAT Solving", In Proceedings of the Twenty-Seventh International Conference on Automated Planning and Scheduling (ICAPS 2017). , pp. 135-139.

[Abstract] [BibTeX]

Abstract: One of the most successful approaches to automated plan-
ning is the translation to propositional satisfiability (SAT).
We employ incremental SAT solving to increase the capabili-
ties of several modern encodings for SAT based planning. Ex-
periments based on benchmarks from the 2014 International
Planning Competition show that an incremental approach sig-
nificantly outperforms non incremental solving. Although we
are using sequential scheduling of makespans, we can outper-
form the state-of-the-art SAT based planning system Mada-
gascar in the number of solved instances.

BibTeX:

@inproceedings{gocht2017accelerating,
  author = {Gocht, Stephan and Balyo, Tomáš},
  title = {Accelerating SAT Based Planning with Incremental SAT Solving},
  booktitle = {Proceedings of the Twenty-Seventh International Conference on Automated Planning and Scheduling (ICAPS 2017)},
  year = {2017},
  pages = {135--139}
}

Research Tools

VeriPB, a tool for verifying refutations of pseudo-Boolean formulas (proofs of unsatisfiability) and more (such as verifying that a valid solution is found).
IncPlan, a tool for SAT base planning with incremental SAT solvers supporting the IPASIR interface.