Search Results

Documents authored by Lynce, Inês

Document
DOI: 10.4230/DagRep.15.8.80
Optimization and Automated Reasoning for Designing Future Space Missions (Dagstuhl Seminar 25362)

Authors: Max Bannach, Johannes Klaus Fichte, Dario Izzo, Inês Lynce, and Giacomo Acciarini

Published in: Dagstuhl Reports, Volume 15, Issue 8 (2026)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 25362 Optimization and Automated Reasoning for Designing Future Space Missions, which explored fundamental optimization and reasoning tasks that arise in early stages of designing complex space missions. Such tasks include selecting and scheduling the bodies that should be encountered, routing a spacecraft across multiple bodies optimally, or strategically placing facilities to support future missions. Many of these problems are still solved by hand, as current missions only contain a few celestial objects. However, with larger and increasingly complex missions, these problems become more relevant and, thus, there is an increasing need to solve space-related optimization, scheduling, and planning problems automatically. Despite the promising opportunities for collaboration, the entry barrier to many of these problems remains high for those without a background in celestial mechanics. Conversely, modern tools and techniques from constraint reasoning and optimization are still largely unfamiliar to many aerospace researchers. The Dagstuhl Seminar 25362 successfully established a bridge between computer scientists working in automated reasoning and experts from the space domain focused on mission analysis and operations. This Dagstuhl Seminar brought together researchers from academia, industry, and space agencies, fostering interdisciplinary dialogue. Problems and tools from both communities were presented in a language accessible to the other, laying the groundwork for future joint research and development.
Cite as

Max Bannach, Johannes Klaus Fichte, Dario Izzo, Inês Lynce, and Giacomo Acciarini. Optimization and Automated Reasoning for Designing Future Space Missions (Dagstuhl Seminar 25362). In Dagstuhl Reports, Volume 15, Issue 8, pp. 80-94, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@Article{bannach_et_al:DagRep.15.8.80,
  author =	{Bannach, Max and Fichte, Johannes Klaus and Izzo, Dario and Lynce, In\^{e}s and Acciarini, Giacomo},
  title =	{{Optimization and Automated Reasoning for Designing Future Space Missions (Dagstuhl Seminar 25362)}},
  pages =	{80--94},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2026},
  volume =	{15},
  number =	{8},
  editor =	{Bannach, Max and Fichte, Johannes Klaus and Izzo, Dario and Lynce, In\^{e}s and Acciarini, Giacomo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.15.8.80},
  URN =		{urn:nbn:de:0030-drops-257771},
  doi =		{10.4230/DagRep.15.8.80},
  annote =	{Keywords: Automated Reasoning, Satellite Constellation Design, Space Logistics, Trajectory Optimization, Astrodynamics, Global Trajectory Optimization}
}
Document
DOI: 10.4230/LIPIcs.CP.2024.8
Slide&Drill, a New Approach for Multi-Objective Combinatorial Optimization

Authors: João Cortes, Inês Lynce, and Vasco Manquinho

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

Abstract
Following the successful use of Propositional Satisfiability (SAT) algorithms in Boolean optimization (e.g., Maximum Satisfiability), several SAT-based algorithms have been proposed for Multi-Objective Combinatorial Optimization (MOCO). However, these new algorithms either provide a small subset of the Pareto front or follow a more exploratory search procedure and the solutions found are usually distant from the Pareto front. We extend the state of the art with a new SAT-based MOCO solver, Slide and Drill (Slide&Drill), that hones an upper bound set of the exact solution. Moreover, we show that Slide&Drill neatly complements proposed UNSAT-SAT algorithms for MOCO. These algorithms can work in tandem over the same shared "blackboard" formula, in order to enable a faster convergence. Experimental results in several sets of benchmark instances show that Slide&Drill can outperform other SAT-based algorithms for MOCO, in particular when paired with previously proposed UNSAT-SAT algorithms.
Cite as

João Cortes, Inês Lynce, and Vasco Manquinho. Slide&Drill, a New Approach for Multi-Objective Combinatorial Optimization. In 30th International Conference on Principles and Practice of Constraint Programming (CP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 307, pp. 8:1-8:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{cortes_et_al:LIPIcs.CP.2024.8,
  author =	{Cortes, Jo\~{a}o and Lynce, In\^{e}s and Manquinho, Vasco},
  title =	{{Slide\&Drill, a New Approach for Multi-Objective Combinatorial Optimization}},
  booktitle =	{30th International Conference on Principles and Practice of Constraint Programming (CP 2024)},
  pages =	{8:1--8:17},
  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.8},
  URN =		{urn:nbn:de:0030-drops-206932},
  doi =		{10.4230/LIPIcs.CP.2024.8},
  annote =	{Keywords: Multi-Objective Combinatorial Optimization, Satisfiability Algorithms}
}
Document
DOI: 10.4230/DagRep.13.6.106
SAT Encodings and Beyond (Dagstuhl Seminar 23261)

Authors: Marijn J. H. Heule, Inês Lynce, Stefan Szeider, and Andre Schidler

Published in: Dagstuhl Reports, Volume 13, Issue 6 (2024)

Abstract
This report documents the program and the outcomes of Dagstuhl Seminar 23261 "SAT Encodings and Beyond." The seminar facilitated an intense examination and discussion of current results and challenges related to encodings for SAT and related solving paradigms. The seminar featured presentations and group work that provided theoretical, practical, and industrial viewpoints. The goal was to foster more profound insights and advancements in encoding techniques, which are pivotal in enhancing solvers' efficiency.
Cite as

Marijn J. H. Heule, Inês Lynce, Stefan Szeider, and Andre Schidler. SAT Encodings and Beyond (Dagstuhl Seminar 23261). In Dagstuhl Reports, Volume 13, Issue 6, pp. 106-122, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{heule_et_al:DagRep.13.6.106,
  author =	{Heule, Marijn J. H. and Lynce, In\^{e}s and Szeider, Stefan and Schidler, Andre},
  title =	{{SAT Encodings and Beyond (Dagstuhl Seminar 23261)}},
  pages =	{106--122},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2024},
  volume =	{13},
  number =	{6},
  editor =	{Heule, Marijn J. H. and Lynce, In\^{e}s and Szeider, Stefan and Schidler, Andre},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.13.6.106},
  URN =		{urn:nbn:de:0030-drops-196409},
  doi =		{10.4230/DagRep.13.6.106},
  annote =	{Keywords: constraint propagation, lower and upper bounds, problem formulation, propositional satisfiability, symmetry breaking}
}
Document
DOI: 10.4230/OASIcs.ICLP.2018.23
Model Revision of Logical Regulatory Networks Using Logic-Based Tools

Authors: Filipe Gouveia, Inês Lynce, and Pedro T. Monteiro

Published in: OASIcs, Volume 64, Technical Communications of the 34th International Conference on Logic Programming (ICLP 2018)

Abstract
Recently, biological data has been increasingly produced calling for the existence of computational models able to organize and computationally reproduce existing observations. In particular, biological regulatory networks have been modeled relying on the Sign Consistency Model or the logical formalism. However, their construction still completely relies on a domain expert to choose the best functions for every network component. Due to the number of possible functions for k arguments, this is typically a process prone to error. Here, we propose to assist the modeler using logic-based tools to verify the model, identifying crucial network components responsible for model inconsistency. We intend to obtain a model building procedure capable of providing the modeler with repaired models satisfying a set of pre-defined criteria, therefore minimizing possible modeling errors.
Cite as

Filipe Gouveia, Inês Lynce, and Pedro T. Monteiro. Model Revision of Logical Regulatory Networks Using Logic-Based Tools. In Technical Communications of the 34th International Conference on Logic Programming (ICLP 2018). Open Access Series in Informatics (OASIcs), Volume 64, pp. 23:1-23:10, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2018)

Copy BibTex To Clipboard

@InProceedings{gouveia_et_al:OASIcs.ICLP.2018.23,
  author =	{Gouveia, Filipe and Lynce, In\^{e}s and Monteiro, Pedro T.},
  title =	{{Model Revision of Logical Regulatory Networks Using Logic-Based Tools}},
  booktitle =	{Technical Communications of the 34th International Conference on Logic Programming (ICLP 2018)},
  pages =	{23:1--23:10},
  series =	{Open Access Series in Informatics (OASIcs)},
  ISBN =	{978-3-95977-090-3},
  ISSN =	{2190-6807},
  year =	{2018},
  volume =	{64},
  editor =	{Dal Palu', Alessandro and Tarau, Paul and Saeedloei, Neda and Fodor, Paul},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.ICLP.2018.23},
  URN =		{urn:nbn:de:0030-drops-98892},
  doi =		{10.4230/OASIcs.ICLP.2018.23},
  annote =	{Keywords: Logical Regulatory Networks, Model Revision, Answer Set Programming, Boolean Satisfiability, Logic-based tools}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.CSL.2012.12
Satisfiability: where Theory meets Practice (Invited Talk)

Authors: Inês Lynce

Published in: LIPIcs, Volume 16, Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL (2012)

Abstract
Propositional Satisfiability (SAT) is a keystone in the history of computer science. SAT was the first problem shown to be NP-complete in 1971 by Stephen Cook. Having passed more than 40 years from then, SAT is now a lively research field where theory and practice have a natural intermixing. In this talk, we overview the use of SAT in practical domains, where SAT is thought in a broad sense, i.e. including SAT extensions such as Maximum Satisfiability (MaxSAT), Pseudo-Boolean Optimization (PBO) and Quantified Boolean Formulas (QBF).
Cite as

Inês Lynce. Satisfiability: where Theory meets Practice (Invited Talk). In Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL. Leibniz International Proceedings in Informatics (LIPIcs), Volume 16, pp. 12-13, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{lynce:LIPIcs.CSL.2012.12,
  author =	{Lynce, In\^{e}s},
  title =	{{Satisfiability: where Theory meets Practice}},
  booktitle =	{Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL},
  pages =	{12--13},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-42-2},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{16},
  editor =	{C\'{e}gielski, Patrick and Durand, Arnaud},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2012.12},
  URN =		{urn:nbn:de:0030-drops-36600},
  doi =		{10.4230/LIPIcs.CSL.2012.12},
  annote =	{Keywords: Propositional Satisfiability, SAT solvers, Applications}
}
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
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact