4 Search Results for "Salhi, Yakoub"

Document
DOI: 10.4230/LIPIcs.SAT.2024.17
Parallel Clause Sharing Strategy Based on Graph Structure of SAT Problem

Authors: Yoichiro Iida, Tomohiro Sonobe, and Mary Inaba

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

Abstract
Parallelization of SAT solvers is an important technique for improving solver performance. The selection of the learnt clauses to share among parallel workers is crucial for its efficiency. Literal block distance (LBD) is often used to evaluate the quality of clauses to select. We propose a new method, Parallel Clause sharing based on graph Structure (PaCS), to select good clauses for sharing. First, we conducted three preliminary experiments to assess the performance of LBD in parallel clause sharing: a performance comparison between the LBD and clause size, an analysis of the utilization of shared clauses, and a comparison of the LBD values of shared clauses at originating and receiving workers. These experiments indicate that the LBD may not be optimal for learnt clause sharing. We attribute the results to the LBD’s inherent dependency on decision trees. Each parallel worker has a unique decision tree; thus, a sharing clause that is good for its originating worker may not be good for others. Therefore, we propose PaCS, a search-independent method that uses the graph structure derived from the input CNF of SAT problems. PaCS evaluates clauses using their edges' weight in the variable incidence graph. Using the input CNF’s graph is effective for parallel clause sharing because it is the common input for all parallel workers. Furthermore, using edge weight can select clauses whose variables' Boolean values are more likely to be determined. Performance evaluation experiments demonstrate that our strategy outperforms LBD by 4% in the number of solved instances and by 12% in PAR-2. This study opens avenues for further improvements in parallel-solving strategies using the structure of SAT problems and reinterpretations of the quality of learnt clauses.
Cite as

Yoichiro Iida, Tomohiro Sonobe, and Mary Inaba. Parallel Clause Sharing Strategy Based on Graph Structure of SAT Problem. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 17:1-17:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{iida_et_al:LIPIcs.SAT.2024.17,
  author =	{Iida, Yoichiro and Sonobe, Tomohiro and Inaba, Mary},
  title =	{{Parallel Clause Sharing Strategy Based on Graph Structure of SAT Problem}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{17:1--17: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.17},
  URN =		{urn:nbn:de:0030-drops-205392},
  doi =		{10.4230/LIPIcs.SAT.2024.17},
  annote =	{Keywords: SAT Solver, Structure of SAT, Parallel application, Clause Learning}
}
Document
DOI: 10.4230/LIPIcs.TIME.2023.5
Prime Scenarios in Qualitative Spatial and Temporal Reasoning

Authors: Yakoub Salhi and Michael Sioutis

Published in: LIPIcs, Volume 278, 30th International Symposium on Temporal Representation and Reasoning (TIME 2023)

Abstract
The concept of prime implicant is a fundamental tool in Boolean algebra, which is used in Boolean circuit design and, recently, in explainable AI. This study investigates an analogous concept in qualitative spatial and temporal reasoning, called prime scenario. Specifically, we define a prime scenario of a qualitative constraint network (QCN) as a minimal set of decisions that can uniquely determine solutions of this QCN. We propose in this paper a collection of algorithms designed to address various problems related to prime scenarios. The first three algorithms aim to generate a prime scenario from a scenario of a QCN. The main idea consists in using path consistency to identify the constraints that can be ignored to generate a prime scenario. The next two algorithms focus on generating a set of prime scenarios that cover all the scenarios of the original QCN: The first algorithm examines every branch of the search tree, while the second is based on the use of a SAT encoding. Our last algorithm is concerned with computing a minimum-size prime scenario by using a MaxSAT encoding built from countermodels of the original QCN. We show that this algorithm is particularly useful for measuring the robustness of a QCN. Finally, a preliminary experimental evaluation is performed with instances of Allen’s Interval Algebra to assess the efficiency of our algorithms and, hence, also the difficulty of the newly introduced problems here.
Cite as

Yakoub Salhi and Michael Sioutis. Prime Scenarios in Qualitative Spatial and Temporal Reasoning. In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 5:1-5:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{salhi_et_al:LIPIcs.TIME.2023.5,
  author =	{Salhi, Yakoub and Sioutis, Michael},
  title =	{{Prime Scenarios in Qualitative Spatial and Temporal Reasoning}},
  booktitle =	{30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
  pages =	{5:1--5:14},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-298-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{278},
  editor =	{Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.5},
  URN =		{urn:nbn:de:0030-drops-190957},
  doi =		{10.4230/LIPIcs.TIME.2023.5},
  annote =	{Keywords: Spatial and Temporal Reasoning, Qualitative Constraints, Prime Scenario, Prime Implicant, Robustness Measurement}
}
Document
Extended Abstract
DOI: 10.4230/LIPIcs.TIME.2023.16
A Decomposition Framework for Inconsistency Handling in Qualitative Spatial and Temporal Reasoning (Extended Abstract)

Authors: Yakoub Salhi and Michael Sioutis

Published in: LIPIcs, Volume 278, 30th International Symposium on Temporal Representation and Reasoning (TIME 2023)

Abstract
Dealing with inconsistency is a central problem in AI, due to the fact that inconsistency can arise for many reasons in real-world applications, such as context dependency, multi-source information, vagueness, noisy data, etc. Among the approaches that are involved in inconsistency handling, we can mention argumentation, non-monotonic reasoning, and paraconsistency, e.g., see [Philippe Besnard and Anthony Hunter, 2008; Gerhard Brewka et al., 1997; Koji Tanaka et al., 2013]. In the work of [Yakoub Salhi and Michael Sioutis, 2023], we are interested in dealing with inconsistency in the context of Qualitative Spatio-Temporal Reasoning (QSTR) [Ligozat, 2013]. QSTR is an AI framework that aims to mimic, natural, human-like representation and reasoning regarding space and time. This framework is applied to a variety of domains, such as qualitative case-based reasoning and learning [Thiago Pedro Donadon Homem et al., 2020] and visual sensemaking [Jakob Suchan et al., 2021]; the interested reader is referred to [Michael Sioutis and Diedrich Wolter, 2021] for a recent survey. Motivation. In [Yakoub Salhi and Michael Sioutis, 2023], we study the decomposition of an inconsistent constraint network into consistent subnetworks under, possible, mandatory constraints. To illustrate the interest of such a decomposition, we provide a simple example described in Figure 1. The QCN depicted in the top part of the figure corresponds to a description of an inconsistent plan. Further, we assume that the constraint Task A {before} Task B is mandatory. To handle inconsistency, this plan can be transformed into a decomposition of two consistent plans, depicted in the bottom part of the figure; this decomposition can be used, e.g., to capture the fact that Task C must be performed twice. More generally, network decomposition can be involved in inconsistency handling in several ways: it can be used to identify potential contexts that explain the presence of inconsistent information; it can also be used to restore consistency through a compromise between the components of a decomposition, e.g., by using belief merging [Jean-François Condotta et al., 2010]; in addition, QCN decomposition can be used as the basis for defining inconsistency measures. Contributions. We summarize the contributions of [Yakoub Salhi and Michael Sioutis, 2023] as follows. First, we propose a theoretical study of a problem that consists in decomposing an inconsistent QCN into a bounded number of consistent QCNs that may satisfy a specified part in the original QCN; intuitively, the required common part corresponds to the constraints that are considered necessary, if any. To this end, we provide upper bounds for the minimum number of components in a decomposition as well as computational complexity results. Secondly, we provide two methods for solving our decomposition problem. The first method corresponds to a greedy constraint-based algorithm, a variant of which involves the use of spanning trees; the basic idea of this variant is that any acyclic constraint graph in QSTR is consistent, and such a graph can be used as a starting point for building consistent components. The second method corresponds to a SAT-based encoding; every model of this encoding is used to construct a valid decomposition. Thirdly, we consider two optimization versions of the initial decomposition problem that focus on minimizing the number of components and maximizing the similarity between components, respectively. The similarity between two QCNs is quantified by the number of common non-universal constraints; the interest in maximizing the similarity lies mainly in the fact that it reduces the number of constraints that allow each component to be distinguished from the rest. Of course, our previous methods are adapted to tackle these optimization versions, too. Additionally, we introduce two inconsistency measures based on QCN decomposition, which can be seen as counterparts of measures for propositional KBs introduced in [Matthias Thimm, 2016; Meriem Ammoura et al., 2017], and show that they satisfy several desired properties in the literature. Finally, we provide implementations of our methods for computing decompositions and experimentally evaluate them using different metrics.
Cite as

Yakoub Salhi and Michael Sioutis. A Decomposition Framework for Inconsistency Handling in Qualitative Spatial and Temporal Reasoning (Extended Abstract). In 30th International Symposium on Temporal Representation and Reasoning (TIME 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 278, pp. 16:1-16:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{salhi_et_al:LIPIcs.TIME.2023.16,
  author =	{Salhi, Yakoub and Sioutis, Michael},
  title =	{{A Decomposition Framework for Inconsistency Handling in Qualitative Spatial and Temporal Reasoning}},
  booktitle =	{30th International Symposium on Temporal Representation and Reasoning (TIME 2023)},
  pages =	{16:1--16:3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-298-3},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{278},
  editor =	{Artikis, Alexander and Bruse, Florian and Hunsberger, Luke},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2023.16},
  URN =		{urn:nbn:de:0030-drops-191062},
  doi =		{10.4230/LIPIcs.TIME.2023.16},
  annote =	{Keywords: Spatial and Temporal Reasoning, Qualitative Constraints, Inconsistency Handling, Decomposition, Inconsistency Measures}
}
Document
DOI: 10.4230/LIPIcs.TIME.2019.9
Qualitative Reasoning and Data Mining

Authors: Yakoub Salhi

Published in: LIPIcs, Volume 147, 26th International Symposium on Temporal Representation and Reasoning (TIME 2019)

Abstract
In this paper, we introduce a new data mining framework that is based on qualitative reasoning. We consider databases where the item domains are of different types, such as numerical values, time intervals and spatial regions. Then, for the considered tasks, we associate to each item a constraint network in a qualitative formalism representing the relations between all the pairs of objects of the database w.r.t. this item. In this context, the introduced data mining problems consist in discovering qualitative covariations between items. In a sense, our framework can be seen as a generalization of gradual itemset mining. In order to solve the introduced problem, we use a declarative approach based on the satisfiability problem in classical propositional logic (SAT). Indeed, we define SAT encodings where the models represent the desired patterns.
Cite as

Yakoub Salhi. Qualitative Reasoning and Data Mining. In 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 147, pp. 9:1-9:15, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{salhi:LIPIcs.TIME.2019.9,
  author =	{Salhi, Yakoub},
  title =	{{Qualitative Reasoning and Data Mining}},
  booktitle =	{26th International Symposium on Temporal Representation and Reasoning (TIME 2019)},
  pages =	{9:1--9:15},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-127-6},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{147},
  editor =	{Gamper, Johann and Pinchinat, Sophie and Sciavicco, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TIME.2019.9},
  URN =		{urn:nbn:de:0030-drops-113677},
  doi =		{10.4230/LIPIcs.TIME.2019.9},
  annote =	{Keywords: Qualitative Database, Qualitative Pattern Mining, Declarative Approach, SAT Modeling}
}
  • Refine by Author
  • 3 Salhi, Yakoub
  • 2 Sioutis, Michael
  • 1 Iida, Yoichiro
  • 1 Inaba, Mary
  • 1 Sonobe, Tomohiro

  • Refine by Classification
  • 3 Theory of computation → Constraint and logic programming
  • 2 Computing methodologies → Spatial and physical reasoning
  • 2 Computing methodologies → Temporal reasoning
  • 1 Computing methodologies → Heuristic function construction
  • 1 Computing methodologies → Knowledge representation and reasoning
  • Show More...

  • Refine by Keyword
  • 2 Qualitative Constraints
  • 2 Spatial and Temporal Reasoning
  • 1 Clause Learning
  • 1 Declarative Approach
  • 1 Decomposition
  • Show More...

  • Refine by Type
  • 4 document

  • Refine by Publication Year
  • 2 2023
  • 1 2019
  • 1 2024

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact