9 Search Results for "Luo, Zhaohui"

Document
DOI: 10.4230/LIPIcs.CP.2024.6
Deep Cooperation of Local Search and Unit Propagation Techniques

Authors: Xiamin Chen, Zhendong Lei, and Pinyan Lu

Published in: LIPIcs, Volume 307, 30th International Conference on Principles and Practice of Constraint Programming (CP 2024)

Abstract
Local search (LS) is an efficient method for solving combinatorial optimization problems such as MaxSAT and Pseudo Boolean Problems (PBO). However, due to a lack of reasoning power and global information, LS methods get stuck at local optima easily. In contrast to the LS, Systematic Search utilizes unit propagation and clause learning techniques with strong reasoning capabilities to avoid falling into local optima. Nevertheless, the complete search is generally time-consuming to obtain a global optimal solution. This work proposes a deep cooperation framework combining local search and unit propagation to address their inherent disadvantages. First, we design a mechanism to detect when LS gets stuck, and then a well-designed unit propagation procedure is called upon to help escape the local optima. To the best of our knowledge, we are the first to integrate unit propagation technique within LS to overcome local optima. Experiments based on a broad range of benchmarks from MaxSAT Evaluations, PBO competitions, the Mixed Integer Programming Library, and three real-life cases validate that our method significantly improves three state-of-the-art MaxSAT and PBO local search solvers.
Cite as

Xiamin Chen, Zhendong Lei, and Pinyan Lu. Deep Cooperation of Local Search and Unit Propagation Techniques. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 6:1-6:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{chen_et_al:LIPIcs.CP.2024.6,
  author =	{Chen, Xiamin and Lei, Zhendong and Lu, Pinyan},
  title =	{{Deep Cooperation of Local Search and Unit Propagation Techniques}},
  booktitle =	{30th International Conference on Principles and Practice of Constraint Programming (CP 2024)},
  pages =	{6:1--6:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-336-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{307},
  editor =	{Shaw, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2024.6},
  URN =		{urn:nbn:de:0030-drops-206918},
  doi =		{10.4230/LIPIcs.CP.2024.6},
  annote =	{Keywords: PBO, Partial MaxSAT, LS, CDCL}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2023.3
Categorical Models of Subtyping

Authors: Greta Coraglia and Jacopo Emmenegger

Published in: LIPIcs, Volume 303, 29th International Conference on Types for Proofs and Programs (TYPES 2023)

Abstract
Most categorical models for dependent types have traditionally been heavily set based: contexts form a category, and for each we have a set of types in said context - and for each type a set of terms of said type. This is the case for categories with families, categories with attributes, and natural models; in particular, all of them can be traced back to certain discrete Grothendieck fibrations. We extend this intuition to the case of general, not necessarily discrete, fibrations, so that over a given context one has not only a set but a category of types. We argue that the added structure can be attributed to a notion of subtyping that shares many features with that of coercive subtyping, in the sense that it is the product of thinking about subtyping as an abbreviation mechanism: we say that a given type A' is a subtype of A if there is a unique coercion from A' to A. Whenever we need a term of type A, then, it suffices to have a term of type A', which we can "plug-in" into A. For this version of subtyping we provide rules, coherences, and explicit models, and we compare and contrast it to coercive subtyping as introduced by Z. Luo and others. We conclude by suggesting how the tools we present can be employed in finding appropriate rules relating subtyping and certain type constructors.
Cite as

Greta Coraglia and Jacopo Emmenegger. Categorical Models of Subtyping. In 29th International Conference on Types for Proofs and Programs (TYPES 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 303, pp. 3:1-3:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{coraglia_et_al:LIPIcs.TYPES.2023.3,
  author =	{Coraglia, Greta and Emmenegger, Jacopo},
  title =	{{Categorical Models of Subtyping}},
  booktitle =	{29th International Conference on Types for Proofs and Programs (TYPES 2023)},
  pages =	{3:1--3:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-332-4},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{303},
  editor =	{Kesner, Delia and Reyes, Eduardo Hermo and van den Berg, Benno},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2023.3},
  URN =		{urn:nbn:de:0030-drops-204811},
  doi =		{10.4230/LIPIcs.TYPES.2023.3},
  annote =	{Keywords: dependent types, subtyping, coercive subtyping, categorical semantics, categories with families, monad}
}
Document
DOI: 10.4230/LIPIcs.SAT.2024.6
Clausal Congruence Closure

Authors: Armin Biere, Katalin Fazekas, Mathias Fleury, and Nils Froleyks

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract
Many practical applications of satisfiability solving employ multiple steps to encode an original problem formulation into conjunctive normal form. Often circuits are used as intermediate representation before encoding those circuits into clausal form. These circuits however might contain redundant isomorphic sub-circuits. If blindly translated into clausal form, this redundancy is retained and increases solving time unless specific preprocessing algorithms are used. Furthermore, such redundant sub-formula structure might only emerge during solving and needs to be addressed by inprocessing. This paper presents a new approach which extracts gate information from the formula and applies congruence closure to match and eliminate redundant gates. Besides new algorithms for gate extraction, we also describe previous unpublished attempts to tackle this problem. Experiments focus on the important problem of combinational equivalence checking for hardware designs and show that our new approach yields a substantial gain in CNF solver performance.
Cite as

Armin Biere, Katalin Fazekas, Mathias Fleury, and Nils Froleyks. Clausal Congruence Closure. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 6:1-6:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{biere_et_al:LIPIcs.SAT.2024.6,
  author =	{Biere, Armin and Fazekas, Katalin and Fleury, Mathias and Froleyks, Nils},
  title =	{{Clausal Congruence Closure}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{6:1--6:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.6},
  URN =		{urn:nbn:de:0030-drops-205287},
  doi =		{10.4230/LIPIcs.SAT.2024.6},
  annote =	{Keywords: Satisfiability Solving, Congruence Closure, Structural Hashing, SAT Sweeping, Conjunctive Normal Form, Combinational Equivalence Checking, Hardware Equivalence Checking}
}
Document
DOI: 10.4230/LIPIcs.SAT.2024.8
Enhancing MaxSAT Local Search via a Unified Soft Clause Weighting Scheme

Authors: Yi Chu, Chu-Min Li, Furong Ye, and Shaowei Cai

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract
Local search has been widely applied to solve the well-known (weighted) partial MaxSAT problem, significantly influencing many real-world applications. The main difficulty to overcome when designing a local search algorithm is that it can easily fall into local optima. Clause weighting is a beneficial technique that dynamically adjusts the landscape of search space to help the algorithm escape from local optima. Existing works tend to increase the weights of falsified clauses, and such strategies may result in an unpredictable landscape of search space during the optimization process. Therefore, in this paper, we propose a Unified Soft Clause Weighting Scheme called Unified-SW, which increases the weights of all soft clauses in feasible local optima, whether they are satisfied or not, while preserving the hierarchy among them. We implemented Unified-SW in a new local search solver called USW-LS. Experimental results demonstrate that USW-LS, outperforms the state-of-the-art local search solvers across benchmarks from anytime tracks of recent MaxSAT Evaluations. More promisingly, a hybrid solver combining USW-LS and TT-Open-WBO-Inc won all four categories in the anytime track of MaxSAT Evaluation 2023.
Cite as

Yi Chu, Chu-Min Li, Furong Ye, and Shaowei Cai. Enhancing MaxSAT Local Search via a Unified Soft Clause Weighting Scheme. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 8:1-8:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{chu_et_al:LIPIcs.SAT.2024.8,
  author =	{Chu, Yi and Li, Chu-Min and Ye, Furong and Cai, Shaowei},
  title =	{{Enhancing MaxSAT Local Search via a Unified Soft Clause Weighting Scheme}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{8:1--8:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.8},
  URN =		{urn:nbn:de:0030-drops-205301},
  doi =		{10.4230/LIPIcs.SAT.2024.8},
  annote =	{Keywords: Weighted Partial MaxSAT, Local Search Method, Weighting Scheme}
}
Document
DOI: 10.4230/LIPIcs.SAT.2024.27
Revisiting SATZilla Features in 2024

Authors: Hadar Shavit and Holger H. Hoos

Published in: LIPIcs, Volume 305, 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)

Abstract
Boolean satisfiability (SAT) is an NP-complete problem with important applications, notably in hardware and software verification. Characterising a SAT instance by a set of features has shown great potential for various tasks, ranging from algorithm selection to benchmark generation. In this work, we revisit the widely used SATZilla features and introduce a new version of the tool used to compute them. In particular, we utilise a new preprocessor and SAT solvers, adjust the code to accommodate larger formulas, and determine better settings of the feature extraction time limits. We evaluate the extracted features on three downstream tasks: satisfiability prediction, running time prediction, and algorithm selection. We observe that our new tool is able to extract features from a broader range of instances than before. We show that the new version of the feature extractor produces features that achieve up to 26% lower RMSE for running time prediction, up to 3% higher accuracy for satisfiability prediction, and up to 15 times higher closed gap for algorithm selection on benchmarks from recent SAT competitions.
Cite as

Hadar Shavit and Holger H. Hoos. Revisiting SATZilla Features in 2024. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 27:1-27:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{shavit_et_al:LIPIcs.SAT.2024.27,
  author =	{Shavit, Hadar and Hoos, Holger H.},
  title =	{{Revisiting SATZilla Features in 2024}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{27:1--27:26},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-334-8},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{305},
  editor =	{Chakraborty, Supratik and Jiang, Jie-Hong Roland},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2024.27},
  URN =		{urn:nbn:de:0030-drops-205496},
  doi =		{10.4230/LIPIcs.SAT.2024.27},
  annote =	{Keywords: Satisfiability, feature extraction, running time prediction, satisfiability prediction}
}
Document
DOI: 10.4230/LIPIcs.FSCD.2024.21
Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti

Authors: Thiago Felicissimo and Théo Winterhalter

Published in: LIPIcs, Volume 299, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)

Abstract
Proof assistants such as Coq implement a type theory featuring three important features: impredicativity, cumulativity and product covariance. This combination has proven difficult to be expressed in the logical framework Dedukti, and previous attempts have failed in providing an encoding that is proven confluent, sound and conservative. In this work we solve this longstanding open problem by providing an encoding of these three features that we prove to be confluent, sound and to satisfy a restricted (but, we argue, strong enough) form of conservativity. Our proof of confluence is a contribution by itself, and combines various criteria and proof techniques from rewriting theory. Our proof of soundness also contributes a new strategy in which the result is shown in terms of an inverse translation function, fixing a common flaw made in some previous encoding attempts.
Cite as

Thiago Felicissimo and Théo Winterhalter. Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 21:1-21:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{felicissimo_et_al:LIPIcs.FSCD.2024.21,
  author =	{Felicissimo, Thiago and Winterhalter, Th\'{e}o},
  title =	{{Impredicativity, Cumulativity and Product Covariance in the Logical Framework Dedukti}},
  booktitle =	{9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024)},
  pages =	{21:1--21:23},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-323-2},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{299},
  editor =	{Rehof, Jakob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2024.21},
  URN =		{urn:nbn:de:0030-drops-203503},
  doi =		{10.4230/LIPIcs.FSCD.2024.21},
  annote =	{Keywords: Dedukti, Rewriting, Confluence, Dependent types, Cumulativity, Universes}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2022.9
A Metatheoretic Analysis of Subtype Universes

Authors: Felix Bradley and Zhaohui Luo

Published in: LIPIcs, Volume 269, 28th International Conference on Types for Proofs and Programs (TYPES 2022)

Abstract
Subtype universes were initially introduced as an expressive mechanisation of bounded quantification extending a modern type theory. In this paper, we consider a dependent type theory equipped with coercive subtyping and a generalisation of subtype universes. We prove results regarding the metatheoretic properties of subtype universes, such as consistency and strong normalisation. We analyse the causes of undecidability in bounded quantification, and discuss how coherency impacts the metatheoretic properties of theories implementing bounded quantification. We describe the effects of certain choices of subtyping inference rules on the expressiveness of a type theory, and examine various applications in natural language semantics, programming languages, and mathematics formalisation.
Cite as

Felix Bradley and Zhaohui Luo. A Metatheoretic Analysis of Subtype Universes. In 28th International Conference on Types for Proofs and Programs (TYPES 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 269, pp. 9:1-9:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{bradley_et_al:LIPIcs.TYPES.2022.9,
  author =	{Bradley, Felix and Luo, Zhaohui},
  title =	{{A Metatheoretic Analysis of Subtype Universes}},
  booktitle =	{28th International Conference on Types for Proofs and Programs (TYPES 2022)},
  pages =	{9:1--9:21},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-285-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{269},
  editor =	{Kesner, Delia and P\'{e}drot, Pierre-Marie},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2022.9},
  URN =		{urn:nbn:de:0030-drops-184520},
  doi =		{10.4230/LIPIcs.TYPES.2022.9},
  annote =	{Keywords: Type theory, coercive subtyping, subtype universes}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2020.9
Subtype Universes

Authors: Harry Maclean and Zhaohui Luo

Published in: LIPIcs, Volume 188, 26th International Conference on Types for Proofs and Programs (TYPES 2020)

Abstract
We introduce a new concept called a subtype universe, which is a collection of subtypes of a particular type. Amongst other things, subtype universes can model bounded quantification without undecidability. Subtype universes have applications in programming, formalisation and natural language semantics. Our construction builds on coercive subtyping, a system of subtyping that preserves canonicity. We prove Strong Normalisation, Subject Reduction and Logical Consistency for our system via transfer from its parent system UTT[ℂ]. We discuss the interaction between subtype universes and other sorts of universe and compare our construction to previous work on Power types.
Cite as

Harry Maclean and Zhaohui Luo. Subtype Universes. In 26th International Conference on Types for Proofs and Programs (TYPES 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 188, pp. 9:1-9:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{maclean_et_al:LIPIcs.TYPES.2020.9,
  author =	{Maclean, Harry and Luo, Zhaohui},
  title =	{{Subtype Universes}},
  booktitle =	{26th International Conference on Types for Proofs and Programs (TYPES 2020)},
  pages =	{9:1--9:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-182-5},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{188},
  editor =	{de'Liguoro, Ugo and Berardi, Stefano and Altenkirch, Thorsten},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2020.9},
  URN =		{urn:nbn:de:0030-drops-138880},
  doi =		{10.4230/LIPIcs.TYPES.2020.9},
  annote =	{Keywords: Type theory, coercive subtyping, subtype universe}
}
Document
DOI: 10.4230/LIPIcs.TYPES.2016.13
On Subtyping in Type Theories with Canonical Objects

Authors: Georgiana Elena Lungu and Zhaohui Luo

Published in: LIPIcs, Volume 97, 22nd International Conference on Types for Proofs and Programs (TYPES 2016)

Abstract
How should one introduce subtyping into type theories with canonical objects such as Martin-Löf's type theory? It is known that the usual subsumptive subtyping is inadequate and it is understood, at least theoretically, that coercive subtyping should instead be employed. However, it has not been studied what the proper coercive subtyping mechanism is and how it should be used to capture intuitive notions of subtyping. In this paper, we introduce a type system with signatures where coercive subtyping relations can be specified, and argue that this provides a suitable subtyping mechanism for type theories with canonical objects. In particular, we show that the subtyping extension is well-behaved by relating it to the previous formulation of coercive subtyping. The paper then proceeds to study the connection with intuitive notions of subtyping. It first shows how a subsumptive subtyping system can be embedded faithfully. Then, it studies how Russell-style universe inclusions can be understood as coercions in our system. And finally, we study constructor subtyping as an example to illustrate that, sometimes, injectivity of coercions need be assumed in order to capture properly some notions of subtyping.
Cite as

Georgiana Elena Lungu and Zhaohui Luo. On Subtyping in Type Theories with Canonical Objects. In 22nd International Conference on Types for Proofs and Programs (TYPES 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 97, pp. 13:1-13:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{lungu_et_al:LIPIcs.TYPES.2016.13,
  author =	{Lungu, Georgiana Elena and Luo, Zhaohui},
  title =	{{On Subtyping in Type Theories with Canonical Objects}},
  booktitle =	{22nd International Conference on Types for Proofs and Programs (TYPES 2016)},
  pages =	{13:1--13:31},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-065-1},
  ISSN =	{1868-8969},
  year =	{2018},
  volume =	{97},
  editor =	{Ghilezan, Silvia and Geuvers, Herman and Ivetic, Jelena},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TYPES.2016.13},
  URN =		{urn:nbn:de:0030-drops-98496},
  doi =		{10.4230/LIPIcs.TYPES.2016.13},
  annote =	{Keywords: subtyping, type theory, conservative extension, canonical objects}
}
  • Refine by Author
  • 3 Luo, Zhaohui
  • 1 Biere, Armin
  • 1 Bradley, Felix
  • 1 Cai, Shaowei
  • 1 Chen, Xiamin
  • Show More...

  • Refine by Classification
  • 4 Theory of computation → Type theory
  • 1 Mathematics of computing → Combinatorial optimization
  • 1 Theory of computation → Automated reasoning
  • 1 Theory of computation → Categorical semantics
  • 1 Theory of computation → Equational logic and rewriting
  • Show More...

  • Refine by Keyword
  • 3 coercive subtyping
  • 2 Type theory
  • 2 subtyping
  • 1 CDCL
  • 1 Combinational Equivalence Checking
  • Show More...

  • Refine by Type
  • 9 document

  • Refine by Publication Year
  • 6 2024
  • 1 2018
  • 1 2021
  • 1 2023

© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact