About Me

Hi! I am a PhD student at Lund University.

Research Interest

Publications

Matching entries: 0
settings...
Devriendt J, Gocht S, Demirović, Emir, Nordström J and Stuckey P (2021), "Cutting to the Core of Pseudo-Boolean Optimization: Combining Core-Guided Search with Cutting Planes Reasoning", In Proceedings of the AAAI Conference on Artificial Intelligence. Vol. 35(5), pp. 3768-3777.
Abstract: 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.
BibTeX:
@inproceedings{DGDNS21Cutting,
  author = {Jo Devriendt and Stephan Gocht and Demirović and Emir and Jakob Nordström and Peter Stuckey},
  title = {Cutting to the Core of Pseudo-Boolean Optimization: Combining Core-Guided Search with Cutting Planes Reasoning},
  booktitle = {Proceedings of the AAAI Conference on Artificial Intelligence},
  year = {2021},
  volume = {35},
  number = {5},
  pages = {3768--3777},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/16494}
}
Gocht S and Nordström J (2021), "Certifying Parity Reasoning Efficiently Using Pseudo-Boolean Proofs", In Proceedings of the AAAI Conference on Artificial Intelligence. Vol. 35(5), pp. 3768-3777.
Abstract: 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.
BibTeX:
@inproceedings{GN21CertifyingParity,
  author = {Stephan Gocht and Jakob Nordström},
  title = {Certifying Parity Reasoning Efficiently Using Pseudo-Boolean Proofs},
  booktitle = {Proceedings of the AAAI Conference on Artificial Intelligence},
  year = {2021},
  volume = {35},
  number = {5},
  pages = {3768--3777},
  url = {https://ojs.aaai.org/index.php/AAAI/article/view/16494}
}
Elffers J, Gocht S, McCreesh C and Nordström J (2020), "Justifying All Differences Using Pseudo-Boolean Reasoning", In Proceedings of the AAAI Conference on Artificial Intelligence. Vol. 34(02), pp. 1486-1494. AAAI Press.
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 AAAI Conference on Artificial Intelligence},
  publisher = {AAAI Press},
  year = {2020},
  volume = {34},
  number = {02},
  pages = {1486--1494},
  url = {https://doi.org/10.1609/aaai.v34i02.5507}
}
Gocht S, McBride R, McCreesh C, Nordström J, Prosser P and Trimble J (2020), "Certifying Solvers for Clique and Maximum Common (Connected) Subgraph Problems", In Proceedings of the 26th International Conference on Principles and Practice of Constraint Programming, CP 2020. Vol. 12333, pp. 338-357. Springer.
Abstract: An algorithm is said to be certifying if it outputs, together with a solution to the problem it solves, a proof that this solution is correct. We explain how state of the art maximum clique, maximum weighted clique, maximal clique enumeration and maximum common (connected) induced subgraph algorithms can be turned into certifying solvers by using pseudo-Boolean models and cutting planes proofs, and demonstrate that this approach can also handle reductions between problems. The generality of our results suggests that this method is ready for widespread adoption in solvers for combinatorial graph problems.
BibTeX:
@inproceedings{DBLP:conf/cp/GochtMMNPT20,
  author = {Stephan Gocht and Ross McBride and Ciaran McCreesh and Jakob Nordström and Patrick Prosser and James Trimble},
  editor = {Helmut Simonis},
  title = {Certifying Solvers for Clique and Maximum Common (Connected) Subgraph Problems},
  booktitle = {Proceedings of the 26th International Conference on Principles and Practice of Constraint Programming, CP 2020},
  publisher = {Springer},
  year = {2020},
  volume = {12333},
  pages = {338--357},
  url = {https://doi.org/10.1007/978-3-030-58475-7_20}
}
Gocht S, McCreesh C and Nordström J (2020), "Subgraph Isomorphism Meets Cutting Planes: Solving With Certified Solutions", In Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, IJCAI-20. , pp. 1134-1140.
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 = {Gocht, Stephan and McCreesh, Ciaran and Nordström, Jakob},
  title = {Subgraph Isomorphism Meets Cutting Planes: Solving With Certified Solutions},
  booktitle = {Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, IJCAI-20},
  year = {2020},
  pages = {1134--1140},
  url = {https://doi.org/10.24963/ijcai.2020/158}
}
Soos M, Gocht S and Meel KS (2020), "Tinted, Detached, and Lazy CNF-XOR Solving and Its Applications to Counting and Sampling", In Computer Aided Verification, CAV 2020. Vol. 12224, pp. 463-484. Springer.
Abstract: Given a Boolean formula, the problem of counting seeks to estimate the
number of solutions of F while the problem of uniform sampling seeks
to sample solutions uniformly at random. Counting and uniform sampling
are fundamental problems in computer science with a wide range of
applications ranging from constrained random simulation, probabilistic
inference to network reliability and beyond. The past few years have
witnessed the rise of hashing-based approaches that use XORbased
hashing and employ SAT solvers to solve the resulting CNF formulas
conjuncted with XOR constraints. Since over 99% of the runtime of
hashing-based techniques is spent inside the SAT queries, improving
CNF-XOR solvers has emerged as a key challenge.
In this paper, we identify the key performance bottlenecks in the
recently proposed BIRD architecture, and we focus on overcoming these
bottlenecks by accelerating the XOR handling within the SAT solver and
on improving the solver integration through a smarter use of (partial)
solutions. We integrate the resulting system, called BIRD2, with the
state of the art approximate model counter, ApproxMC3, and the state
of the art almost-uniform model sampler UniGen2. Through an extensive
evaluation over a large benchmark set of over 1896 instances, we
observe that BIRD2 leads to consistent speed up for both counting and
sampling, and in particular, we solve 77 and 51 more instances for
counting and sampling respectively.
BibTeX:
@inproceedings{DBLP:conf/cav/SoosGM20,
  author = {Mate Soos and Stephan Gocht and Kuldeep S. Meel},
  title = {Tinted, Detached, and Lazy CNF-XOR Solving and Its Applications to Counting and Sampling},
  booktitle = {Computer Aided Verification, CAV 2020},
  publisher = {Springer},
  year = {2020},
  volume = {12224},
  pages = {463--484},
  url = {https://doi.org/10.1007/978-3-030-53288-8_22}
}
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},
  url = {https://doi.org/10.1007/978-3-030-30446-1_19}
}
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. , 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}
}
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: 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},
  url = {https://www.ijcai.org/proceedings/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}
}
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 (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 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 (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 20/10/2021.

Research Tools


Generated by jekyll. Using the Researcher Tempalte.