About Me

Hi! I am a PhD student at Lund University.

Research Interest

Publications

Matching entries: 0
settings...
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. To appear.
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. To appear},
  year = {2020}
}
Stephan Gocht Ciaran McCreesh and Nordström. J (2020), "Subgraph Isomorphism Meets Cutting Planes: Solving with Certified Solutions.", In Proceedings of the 29th International Joint Conference on Artificial Intelligence (IJCAI '20), July 2020. To appear.
Abstract: 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
BibTeX:
@inproceedings{Gocht2020,
  author = {Stephan Gocht, Ciaran McCreesh, and Jakob Nordström.},
  title = {Subgraph Isomorphism Meets Cutting Planes: Solving with Certified Solutions.},
  booktitle = {Proceedings of the 29th International Joint Conference on Artificial Intelligence (IJCAI '20), July 2020. To appear},
  year = {2020}
}
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: 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: 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). , pp. 1300-1308.
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)},
  year = {2018},
  pages = {1300--1308},
  url = {https://www.ijcai.org/proceedings/2018/181},
  doi = {10.24963/ijcai.2018/181}
}
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 International Conference on Theory and Applications of Satisfiability Testing. , pp. 292-310.
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 = {International Conference on Theory and Applications of Satisfiability Testing},
  year = {2018},
  pages = {292--310},
  url = {https://link.springer.com/chapter/10.1007/978-3-319-94144-8_18},
  doi = {10.1007/978-3-319-94144-8_18}
}
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. , pp. 312-319.
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},
  year = {2017},
  pages = {312--319},
  url = {https://link.springer.com/chapter/10.1007/978-3-319-66845-1_20}
}
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: 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},
  url = {https://www.aaai.org/ocs/index.php/ICAPS/ICAPS17/paper/view/15580}
}
Gocht S (2017), "Incremental SAT Solving for SAT Based Planning". Thesis at: Karlsruhe Institute of Technology (KIT).
Abstract: One of the most successful approaches to automated planning is the translation to proposi-
tional satisfiability (SAT). This thesis evaluates incremental SAT solving for 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, planning specific heuristics and advanced scheduling of makespans is not used,
it is possible to outperform the state-of-the-art SAT based planning systems Madagascar
and PDRPlan in the number of solved instances.
BibTeX:
@thesis{gocht2017incremental,
  author = {Gocht, Stephan},
  title = {Incremental SAT Solving for SAT Based Planning},
  school = {Karlsruhe Institute of Technology (KIT)},
  year = {2017},
  url = {https://algo2.iti.kit.edu/3324.php}
}
Gocht S (2014), "Refinement of Path Conditions for Information Flow Analysis". Thesis at: Karlsruhe Institute of Technology (KIT).
Abstract: Path conditions are a static analysis tool for information flow control (IFC). They can be
used to produce witnesses for an illegal flow, which do not necessarily represent a concrete
execution of the program. This bachelor thesis will provide a detailed approach to eliminate
these false witnesses using counterexample guided abstraction refinement (CEGAR) and
thereby increase precision.
As not all values satisfying the PC need to occur simultaneously during a program execution,
a property is introduced which is true iff the values occur during the program execution.
Some values are always occurring simultaneously if a flow exists. This information can be
used to increase precision and is added to the described property, without using temporal
logic. Finally, the CEGAR approach is adopted to provide an algorithm for checking this
property.
BibTeX:
@thesis{gocht2014refinement,
  author = {Gocht, Stephan},
  title = {Refinement of Path Conditions for Information Flow Analysis},
  school = {Karlsruhe Institute of Technology (KIT)},
  year = {2014},
  url = {https://asa.iti.kit.edu/130_441.php}
}
Created by JabRef on 17/06/2020.

Research Tools


This is a personal web page. More information. Generated by jekyll. Theme: here.