3 Search Results for "Jiang, Hai"

Document
DOI: 10.4230/LIPIcs.SAT.2024.13
Entailing Generalization Boosts Enumeration

Authors: Dror Fried, Alexander Nadel, Roberto Sebastiani, and Yogev Shalmon

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

Abstract
Given a combinational circuit Γ with a single output o, AllSAT-CT is the problem of enumerating all solutions of Γ. Recently, we introduced several state-of-the-art AllSAT-CT algorithms based on satisfying generalization, which generalizes a given total Boolean solution to a smaller ternary solution that still satisfies the circuit. We implemented them in our open-source tool HALL. In this work we draw upon recent theoretical works suggesting that utilizing generalization algorithms, which can produce solutions that entail the circuit without satisfying it, may enhance enumeration. After considering the theory and adapting it to our needs, we enrich HALL’s AllSAT-CT algorithms by incorporating several newly implemented generalization schemes and additional SAT solvers. By conducting extensive experiments we show that entailing generalization substantially boosts HALL’s performance and quality (where quality corresponds to the number of reported generalized solutions per instance), with the best results achieved by combining satisfying and entailing generalization.
Cite as

Dror Fried, Alexander Nadel, Roberto Sebastiani, and Yogev Shalmon. Entailing Generalization Boosts Enumeration. In 27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 305, pp. 13:1-13:14, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{fried_et_al:LIPIcs.SAT.2024.13,
  author =	{Fried, Dror and Nadel, Alexander and Sebastiani, Roberto and Shalmon, Yogev},
  title =	{{Entailing Generalization Boosts Enumeration}},
  booktitle =	{27th International Conference on Theory and Applications of Satisfiability Testing (SAT 2024)},
  pages =	{13:1--13:14},
  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.13},
  URN =		{urn:nbn:de:0030-drops-205351},
  doi =		{10.4230/LIPIcs.SAT.2024.13},
  annote =	{Keywords: Generalization, Minimization, Prime Implicant, AllSAT, SAT, Circuits}
}
Document
DOI: 10.4230/LIPIcs.ECRTS.2024.1
JuMP2start: Time-Aware Stop-Start Technology for a Software-Defined Vehicle System

Authors: Anam Farrukh and Richard West

Published in: LIPIcs, Volume 298, 36th Euromicro Conference on Real-Time Systems (ECRTS 2024)

Abstract
Software-defined vehicle (SDV) systems replace traditional ECU architectures with software tasks running on centralized multicore processors in automotive-grade PCs. However, PC boot delays to cold-start an integrated vehicle management system (VMS) are problematic for time-critical functions, which must process sensor and actuator data within specific time bounds. To tackle this challenge, we present JuMP2start: a time-aware multicore stop-start approach for SDVs. JuMP2start leverages PC-class suspend-to-RAM techniques to capture a system snapshot when the vehicle is stopped. Upon restart, critical services are resumed-from-RAM within order of milliseconds compared to normal cold-start times. This work showcases how JuMP2start manages global suspension and resumption mechanisms for a state-of-the-art dual-domain vehicle management system comprising real-time OS (RTOS) and Linux SMP guests. JuMP2start models automotive tasks as continuable or restartable to ensure timing- and safety-critical function pipelines are reactively resumed with low latency, while discarding stale task state. Experiments with the VMS show that critical CAN traffic processing resumes within 500 milliseconds of waking the RTOS guest, and reaches steady-state throughput in under 7ms.
Cite as

Anam Farrukh and Richard West. JuMP2start: Time-Aware Stop-Start Technology for a Software-Defined Vehicle System. In 36th Euromicro Conference on Real-Time Systems (ECRTS 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 298, pp. 1:1-1:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{farrukh_et_al:LIPIcs.ECRTS.2024.1,
  author =	{Farrukh, Anam and West, Richard},
  title =	{{JuMP2start: Time-Aware Stop-Start Technology for a Software-Defined Vehicle System}},
  booktitle =	{36th Euromicro Conference on Real-Time Systems (ECRTS 2024)},
  pages =	{1:1--1:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-324-9},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{298},
  editor =	{Pellizzoni, Rodolfo},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECRTS.2024.1},
  URN =		{urn:nbn:de:0030-drops-203046},
  doi =		{10.4230/LIPIcs.ECRTS.2024.1},
  annote =	{Keywords: Time-aware stop-start, Real-time power management, Suspend-to-RAM, Partitioning hypervisor, Vehicle management system, Vehicle-OS, Software-defined vehicles (SDV)}
}
Document
DOI: 10.4230/DagSemProc.09261.20
OPTIMIZATION APPROACHES TO AIRLINE INDUSTRY CHALLENGES: Airline Schedule Planning and Recovery

Authors: Cynthia Barnhart, Hai Jiang, and Lavanya Marla

Published in: Dagstuhl Seminar Proceedings, Volume 9261, Models and Algorithms for Optimization in Logistics (2009)

Abstract
The airline industry has a long history of developing and applying optimization approaches to their myriad of scheduling problems. These problems have several challenging characteristics, the two most challenging of which include: 1) they span long- and short-term horizons, from strategic planning of flight schedules operated several months into the future, to real-time operations in which strategies must be developed and implemented immediately to recover scheduled operations from disruptions; and 2) they include multiple resources that must be coordinated, such as aircraft, crews, and passengers. While optimization approaches have been essential to the airline industry and effective in developing aircraft and crew schedules, historical models and approaches often fail to capture the complexity of airline operations. For example, approaches, often by necessity, involve a sequential, rather than an integrated process to develop schedules for aircraft and crews, and moreover, the process involves simplifying assumptions, including that future demands are known and deterministic, and that schedules are operated as planned. In more recent research on airline schedule optimization, advances have led to new schedule optimization models and approaches that more accurately reflect reality. As described in this presentation, the most notable contributions to these advances include: 1. Integrated Aircraft and Crew Schedule Optimization Approaches in which some of the aircraft and crew schedule decisions previously taken sequentially are integrated, moving closer to producing globally optimal schedules; 2. Dynamic Scheduling Approaches in which schedules are adjusted during the passenger booking period to reflect increased knowledge of booking patterns and to increase the schedule’s associated total revenue; and 3. Robust Optimization Approaches in which the stochastic nature of airline operations is modeled and realized schedule performance is optimized.
Cite as

Cynthia Barnhart, Hai Jiang, and Lavanya Marla. OPTIMIZATION APPROACHES TO AIRLINE INDUSTRY CHALLENGES: Airline Schedule Planning and Recovery. In Models and Algorithms for Optimization in Logistics. Dagstuhl Seminar Proceedings, Volume 9261, pp. 1-3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2009)

Copy BibTex To Clipboard

@InProceedings{barnhart_et_al:DagSemProc.09261.20,
  author =	{Barnhart, Cynthia and Jiang, Hai and Marla, Lavanya},
  title =	{{OPTIMIZATION APPROACHES TO AIRLINE INDUSTRY CHALLENGES:  Airline Schedule Planning and Recovery}},
  booktitle =	{Models and Algorithms for Optimization in Logistics},
  pages =	{1--3},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2009},
  volume =	{9261},
  editor =	{Cynthia Barnhart and Uwe Clausen and Ulrich Lauther and Rolf H. M\"{o}hring},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagSemProc.09261.20},
  URN =		{urn:nbn:de:0030-drops-21880},
  doi =		{10.4230/DagSemProc.09261.20},
  annote =	{Keywords: Airline aircraft and crew optimization, robust scheduling, dynamic scheduling}
}
  • Refine by Author
  • 1 Barnhart, Cynthia
  • 1 Farrukh, Anam
  • 1 Fried, Dror
  • 1 Jiang, Hai
  • 1 Marla, Lavanya
  • Show More...

  • Refine by Classification
  • 1 Computer systems organization → Embedded systems
  • 1 Computer systems organization → Real-time system architecture
  • 1 Mathematics of computing → Solvers

  • Refine by Keyword
  • 1 Airline aircraft and crew optimization
  • 1 AllSAT
  • 1 Circuits
  • 1 Generalization
  • 1 Minimization
  • Show More...

  • Refine by Type
  • 3 document

  • Refine by Publication Year
  • 2 2024
  • 1 2009

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