About Me

Hi! I am a PhD student at the Theoretical Computer Science - TSC group at KTH Royal Institute of Technology.

Research Interest

Publications

Matching entries: 0
settings...
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. , 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},
  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 12/12/2018.

Research Tools


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