Search Results

Documents authored by Marques-Silva, Joao


Found 2 Possible Name Variants:

Marques-Silva, Joao

Document
Invited Talk
Trustable Explainable AI - SAT to the Rescue (Invited Talk)

Authors: Joao Marques-Silva

Published in: LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)


Abstract
Explainable Artificial Intelligence (XAI) aims to help human decision makers in understanding the operation of complex AI models. However, many XAI solutions, based on non-symbolic methods, offer no formal guarantees and can produce erroneous results. In contrast, logic-based XAI guarantees the rigor of computed explanations, and this is paramount in high-stakes uses of AI. This talk overviews several flagship applications of Boolean satisfiability (SAT) solvers in reasoning about logic-based explanations.

Cite as

Joao Marques-Silva. Trustable Explainable AI - SAT to the Rescue (Invited Talk). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 2:1-2:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)


Copy BibTex To Clipboard

@InProceedings{marquessilva:LIPIcs.SAT.2026.2,
  author =	{Marques-Silva, Joao},
  title =	{{Trustable Explainable AI - SAT to the Rescue}},
  booktitle =	{29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
  pages =	{2:1--2:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-431-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{377},
  editor =	{Ignatiev, Alexey and Szeider, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.2},
  URN =		{urn:nbn:de:0030-drops-263086},
  doi =		{10.4230/LIPIcs.SAT.2026.2},
  annote =	{Keywords: Explainable AI, Boolean Satisfiability}
}
Document
Short Paper
Shapley-Shubik Attribution from Minimal Subsets (Short Paper)

Authors: Pablo Martínez-Naredo, Raúl Mencía, Joao Marques-Silva, and Carlos Mencía

Published in: LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)


Abstract
We address the problem of attributing responsibility to individual clauses for the unsatisfiability of a propositional formula. Recent work adopted the Shapley-Shubik power index, proposing a probabilistic approximation algorithm. However, although polynomial, the required number of SAT solver calls becomes impractical when the input formula is not easy to solve. In such cases, it is often possible to enumerate a partial set of minimal unsatisfiable subsets (MUSes) and minimal correction subsets (MCSes). In this paper, we demonstrate that these subsets can be leveraged to efficiently bound and approximate the Shapley-Shubik index. We introduce a framework that exploits the structural information provided by the available sets to derive useful attribution explanations.

Cite as

Pablo Martínez-Naredo, Raúl Mencía, Joao Marques-Silva, and Carlos Mencía. Shapley-Shubik Attribution from Minimal Subsets (Short Paper). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 33:1-33:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)


Copy BibTex To Clipboard

@InProceedings{martineznaredo_et_al:LIPIcs.SAT.2026.33,
  author =	{Mart{\'\i}nez-Naredo, Pablo and Menc{\'\i}a, Ra\'{u}l and Marques-Silva, Joao and Menc{\'\i}a, Carlos},
  title =	{{Shapley-Shubik Attribution from Minimal Subsets}},
  booktitle =	{29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
  pages =	{33:1--33:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-431-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{377},
  editor =	{Ignatiev, Alexey and Szeider, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.33},
  URN =		{urn:nbn:de:0030-drops-263398},
  doi =		{10.4230/LIPIcs.SAT.2026.33},
  annote =	{Keywords: Unsatisfiability, Shapley-Shubik index, MUSes and MCSes}
}
Document
Efficient Explanations for Rule Ensembles

Authors: Hao Hu, Alexey Ignatiev, and Joao Marques-Silva

Published in: LIPIcs, Volume 379, 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)


Abstract
Tree ensembles (TEs) are among the most widely used machine learning models, yet explaining their predictions remains a computational challenge. Recent work in formal explainable AI (FXAI) has focused on computing abductive explanations for TEs using Boolean satisfiability (SAT) and maximum satisfiability (MaxSAT). However, these methods often fail to scale with the growth of the number and depth of the trees in the ensemble. This paper addresses these scalability limitations by shifting focus to Rule Ensembles (REs), a structurally simpler alternative to TEs. We make three primary contributions. First, we adapt an existing MaxSAT-based explanation framework designed for TEs to function with general REs. Second, we devise a dedicated logic encoding for REs combining SAT solving with pseudo-Boolean (PB) constraints for determining the winning class. Finally, empirical experiments on standard tabular and image datasets demonstrate a significant advantage of the proposed SAT-based approach for REs over the state-of-the-art MaxSAT-based approach for TEs.

Cite as

Hao Hu, Alexey Ignatiev, and Joao Marques-Silva. Efficient Explanations for Rule Ensembles. In 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 379, pp. 29:1-29:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)


Copy BibTex To Clipboard

@InProceedings{hu_et_al:LIPIcs.CP.2026.29,
  author =	{Hu, Hao and Ignatiev, Alexey and Marques-Silva, Joao},
  title =	{{Efficient Explanations for Rule Ensembles}},
  booktitle =	{32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)},
  pages =	{29:1--29:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-432-1},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{379},
  editor =	{Beldiceanu, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2026.29},
  URN =		{urn:nbn:de:0030-drops-266616},
  doi =		{10.4230/LIPIcs.CP.2026.29},
  annote =	{Keywords: Explainable Artifical Intelligence, Rule Ensembles, Boolean Satisfiability}
}
Document
Extending the Synergies Between SAT and Description Logics (Dagstuhl Seminar 21361)

Authors: Joao Marques-Silva, Rafael Peñaloza, and Uli Sattler

Published in: Dagstuhl Reports, Volume 11, Issue 8 (2022)


Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 21361 "Extending the Synergies Between SAT and Description Logics". Propositional satisfiability (SAT) and description logics (DL) are two successful areas of computational logic where automated reasoning plays a fundamental role. While they share a common core (formalised on logic), the developments in both areas have diverged in their scopes, methods, and applications. The goal of this seminar was to reconnect the SAT and DL communities (understood in a broad sense) so that they can benefit from each other. The seminar thus focused on explaining the foundational principles, main results, and open problems of each area, and discussing potential avenues for collaborative progress.

Cite as

Joao Marques-Silva, Rafael Peñaloza, and Uli Sattler. Extending the Synergies Between SAT and Description Logics (Dagstuhl Seminar 21361). In Dagstuhl Reports, Volume 11, Issue 8, pp. 1-10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@Article{marquessilva_et_al:DagRep.11.8.1,
  author =	{Marques-Silva, Joao and Pe\~{n}aloza, Rafael and Sattler, Uli},
  title =	{{Extending the Synergies Between SAT and Description Logics (Dagstuhl Seminar 21361)}},
  pages =	{1--10},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2022},
  volume =	{11},
  number =	{8},
  editor =	{Marques-Silva, Joao and Pe\~{n}aloza, Rafael and Sattler, Uli},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.11.8.1},
  URN =		{urn:nbn:de:0030-drops-157661},
  doi =		{10.4230/DagRep.11.8.1},
  annote =	{Keywords: description logics, propositional satisfiability, reasoning services, standard and non-standard inferences}
}
Document
On the Tractability of Explaining Decisions of Classifiers

Authors: Martin C. Cooper and João Marques-Silva

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)


Abstract
Explaining decisions is at the heart of explainable AI. We investigate the computational complexity of providing a formally-correct and minimal explanation of a decision taken by a classifier. In the case of threshold (i.e. score-based) classifiers, we show that a complexity dichotomy follows from the complexity dichotomy for languages of cost functions. In particular, submodular classifiers allow tractable explanation of positive decisions, but not negative decisions (assuming P≠NP). This is an example of the possible asymmetry between the complexity of explaining positive and negative decisions of a particular classifier. Nevertheless, there are large families of classifiers for which explaining both positive and negative decisions is tractable, such as monotone or linear classifiers. We extend tractable cases to constrained classifiers (when there are constraints on the possible input vectors) and to the search for contrastive rather than abductive explanations. Indeed, we show that tractable classes coincide for abductive and contrastive explanations in the constrained or unconstrained settings.

Cite as

Martin C. Cooper and João Marques-Silva. On the Tractability of Explaining Decisions of Classifiers. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 21:1-21:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{cooper_et_al:LIPIcs.CP.2021.21,
  author =	{Cooper, Martin C. and Marques-Silva, Jo\~{a}o},
  title =	{{On the Tractability of Explaining Decisions of Classifiers}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{21:1--21:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.21},
  URN =		{urn:nbn:de:0030-drops-153125},
  doi =		{10.4230/LIPIcs.CP.2021.21},
  annote =	{Keywords: machine learning, tractability, explanations, weighted constraint satisfaction}
}

Marques-Silva, João

Document
Invited Talk
Trustable Explainable AI - SAT to the Rescue (Invited Talk)

Authors: Joao Marques-Silva

Published in: LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)


Abstract
Explainable Artificial Intelligence (XAI) aims to help human decision makers in understanding the operation of complex AI models. However, many XAI solutions, based on non-symbolic methods, offer no formal guarantees and can produce erroneous results. In contrast, logic-based XAI guarantees the rigor of computed explanations, and this is paramount in high-stakes uses of AI. This talk overviews several flagship applications of Boolean satisfiability (SAT) solvers in reasoning about logic-based explanations.

Cite as

Joao Marques-Silva. Trustable Explainable AI - SAT to the Rescue (Invited Talk). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 2:1-2:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)


Copy BibTex To Clipboard

@InProceedings{marquessilva:LIPIcs.SAT.2026.2,
  author =	{Marques-Silva, Joao},
  title =	{{Trustable Explainable AI - SAT to the Rescue}},
  booktitle =	{29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
  pages =	{2:1--2:10},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-431-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{377},
  editor =	{Ignatiev, Alexey and Szeider, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.2},
  URN =		{urn:nbn:de:0030-drops-263086},
  doi =		{10.4230/LIPIcs.SAT.2026.2},
  annote =	{Keywords: Explainable AI, Boolean Satisfiability}
}
Document
Short Paper
Shapley-Shubik Attribution from Minimal Subsets (Short Paper)

Authors: Pablo Martínez-Naredo, Raúl Mencía, Joao Marques-Silva, and Carlos Mencía

Published in: LIPIcs, Volume 377, 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)


Abstract
We address the problem of attributing responsibility to individual clauses for the unsatisfiability of a propositional formula. Recent work adopted the Shapley-Shubik power index, proposing a probabilistic approximation algorithm. However, although polynomial, the required number of SAT solver calls becomes impractical when the input formula is not easy to solve. In such cases, it is often possible to enumerate a partial set of minimal unsatisfiable subsets (MUSes) and minimal correction subsets (MCSes). In this paper, we demonstrate that these subsets can be leveraged to efficiently bound and approximate the Shapley-Shubik index. We introduce a framework that exploits the structural information provided by the available sets to derive useful attribution explanations.

Cite as

Pablo Martínez-Naredo, Raúl Mencía, Joao Marques-Silva, and Carlos Mencía. Shapley-Shubik Attribution from Minimal Subsets (Short Paper). In 29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 377, pp. 33:1-33:13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)


Copy BibTex To Clipboard

@InProceedings{martineznaredo_et_al:LIPIcs.SAT.2026.33,
  author =	{Mart{\'\i}nez-Naredo, Pablo and Menc{\'\i}a, Ra\'{u}l and Marques-Silva, Joao and Menc{\'\i}a, Carlos},
  title =	{{Shapley-Shubik Attribution from Minimal Subsets}},
  booktitle =	{29th International Conference on Theory and Applications of Satisfiability Testing (SAT 2026)},
  pages =	{33:1--33:13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-431-4},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{377},
  editor =	{Ignatiev, Alexey and Szeider, Stefan},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.SAT.2026.33},
  URN =		{urn:nbn:de:0030-drops-263398},
  doi =		{10.4230/LIPIcs.SAT.2026.33},
  annote =	{Keywords: Unsatisfiability, Shapley-Shubik index, MUSes and MCSes}
}
Document
Efficient Explanations for Rule Ensembles

Authors: Hao Hu, Alexey Ignatiev, and Joao Marques-Silva

Published in: LIPIcs, Volume 379, 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)


Abstract
Tree ensembles (TEs) are among the most widely used machine learning models, yet explaining their predictions remains a computational challenge. Recent work in formal explainable AI (FXAI) has focused on computing abductive explanations for TEs using Boolean satisfiability (SAT) and maximum satisfiability (MaxSAT). However, these methods often fail to scale with the growth of the number and depth of the trees in the ensemble. This paper addresses these scalability limitations by shifting focus to Rule Ensembles (REs), a structurally simpler alternative to TEs. We make three primary contributions. First, we adapt an existing MaxSAT-based explanation framework designed for TEs to function with general REs. Second, we devise a dedicated logic encoding for REs combining SAT solving with pseudo-Boolean (PB) constraints for determining the winning class. Finally, empirical experiments on standard tabular and image datasets demonstrate a significant advantage of the proposed SAT-based approach for REs over the state-of-the-art MaxSAT-based approach for TEs.

Cite as

Hao Hu, Alexey Ignatiev, and Joao Marques-Silva. Efficient Explanations for Rule Ensembles. In 32nd International Conference on Principles and Practice of Constraint Programming (CP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 379, pp. 29:1-29:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)


Copy BibTex To Clipboard

@InProceedings{hu_et_al:LIPIcs.CP.2026.29,
  author =	{Hu, Hao and Ignatiev, Alexey and Marques-Silva, Joao},
  title =	{{Efficient Explanations for Rule Ensembles}},
  booktitle =	{32nd International Conference on Principles and Practice of Constraint Programming (CP 2026)},
  pages =	{29:1--29:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-432-1},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{379},
  editor =	{Beldiceanu, Nicolas},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2026.29},
  URN =		{urn:nbn:de:0030-drops-266616},
  doi =		{10.4230/LIPIcs.CP.2026.29},
  annote =	{Keywords: Explainable Artifical Intelligence, Rule Ensembles, Boolean Satisfiability}
}
Document
Extending the Synergies Between SAT and Description Logics (Dagstuhl Seminar 21361)

Authors: Joao Marques-Silva, Rafael Peñaloza, and Uli Sattler

Published in: Dagstuhl Reports, Volume 11, Issue 8 (2022)


Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 21361 "Extending the Synergies Between SAT and Description Logics". Propositional satisfiability (SAT) and description logics (DL) are two successful areas of computational logic where automated reasoning plays a fundamental role. While they share a common core (formalised on logic), the developments in both areas have diverged in their scopes, methods, and applications. The goal of this seminar was to reconnect the SAT and DL communities (understood in a broad sense) so that they can benefit from each other. The seminar thus focused on explaining the foundational principles, main results, and open problems of each area, and discussing potential avenues for collaborative progress.

Cite as

Joao Marques-Silva, Rafael Peñaloza, and Uli Sattler. Extending the Synergies Between SAT and Description Logics (Dagstuhl Seminar 21361). In Dagstuhl Reports, Volume 11, Issue 8, pp. 1-10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


Copy BibTex To Clipboard

@Article{marquessilva_et_al:DagRep.11.8.1,
  author =	{Marques-Silva, Joao and Pe\~{n}aloza, Rafael and Sattler, Uli},
  title =	{{Extending the Synergies Between SAT and Description Logics (Dagstuhl Seminar 21361)}},
  pages =	{1--10},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2022},
  volume =	{11},
  number =	{8},
  editor =	{Marques-Silva, Joao and Pe\~{n}aloza, Rafael and Sattler, Uli},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.11.8.1},
  URN =		{urn:nbn:de:0030-drops-157661},
  doi =		{10.4230/DagRep.11.8.1},
  annote =	{Keywords: description logics, propositional satisfiability, reasoning services, standard and non-standard inferences}
}
Document
On the Tractability of Explaining Decisions of Classifiers

Authors: Martin C. Cooper and João Marques-Silva

Published in: LIPIcs, Volume 210, 27th International Conference on Principles and Practice of Constraint Programming (CP 2021)


Abstract
Explaining decisions is at the heart of explainable AI. We investigate the computational complexity of providing a formally-correct and minimal explanation of a decision taken by a classifier. In the case of threshold (i.e. score-based) classifiers, we show that a complexity dichotomy follows from the complexity dichotomy for languages of cost functions. In particular, submodular classifiers allow tractable explanation of positive decisions, but not negative decisions (assuming P≠NP). This is an example of the possible asymmetry between the complexity of explaining positive and negative decisions of a particular classifier. Nevertheless, there are large families of classifiers for which explaining both positive and negative decisions is tractable, such as monotone or linear classifiers. We extend tractable cases to constrained classifiers (when there are constraints on the possible input vectors) and to the search for contrastive rather than abductive explanations. Indeed, we show that tractable classes coincide for abductive and contrastive explanations in the constrained or unconstrained settings.

Cite as

Martin C. Cooper and João Marques-Silva. On the Tractability of Explaining Decisions of Classifiers. In 27th International Conference on Principles and Practice of Constraint Programming (CP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 210, pp. 21:1-21:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


Copy BibTex To Clipboard

@InProceedings{cooper_et_al:LIPIcs.CP.2021.21,
  author =	{Cooper, Martin C. and Marques-Silva, Jo\~{a}o},
  title =	{{On the Tractability of Explaining Decisions of Classifiers}},
  booktitle =	{27th International Conference on Principles and Practice of Constraint Programming (CP 2021)},
  pages =	{21:1--21:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-211-2},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{210},
  editor =	{Michel, Laurent D.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2021.21},
  URN =		{urn:nbn:de:0030-drops-153125},
  doi =		{10.4230/LIPIcs.CP.2021.21},
  annote =	{Keywords: machine learning, tractability, explanations, weighted constraint satisfaction}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail