論文の概要: A Comparative Study of SMT and MILP for the Nurse Rostering Problem

• arxiv url: http://arxiv.org/abs/2505.10328v1
• Date: Thu, 15 May 2025 14:12:39 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-05-16 22:29:06.35284
• Title: A Comparative Study of SMT and MILP for the Nurse Rostering Problem
• Title（参考訳）: 看護ロスター問題に対するSMTとMILPの比較検討
• Authors: Alvin Combrink, Stephie Do, Kristofer Bengtsson, Sabino Francesco Roselli, Martin Fabian,
• Abstract要約: 本研究では,多種多様な実世界のスケジューリング制約をモデル化可能な汎用制約定式化を提案する。 我々は、学術的および現実世界にインスパイアされたロスター問題に関して、Z3 と Gurobi を比較した。
• 参考スコア（独自算出の注目度）: 3.2117987125606517
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The effects of personnel scheduling on the quality of care and working conditions for healthcare personnel have been thoroughly documented. However, the ever-present demand and large variation of constraints make healthcare scheduling particularly challenging. This problem has been studied for decades, with limited research aimed at applying Satisfiability Modulo Theories (SMT). SMT has gained momentum within the formal verification community in the last decades, leading to the advancement of SMT solvers that have been shown to outperform standard mathematical programming techniques. In this work, we propose generic constraint formulations that can model a wide range of real-world scheduling constraints. Then, the generic constraints are formulated as SMT and MILP problems and used to compare the respective state-of-the-art solvers, Z3 and Gurobi, on academic and real-world inspired rostering problems. Experimental results show how each solver excels for certain types of problems; the MILP solver generally performs better when the problem is highly constrained or infeasible, while the SMT solver performs better otherwise. On real-world inspired problems containing a more varied set of shifts and personnel, the SMT solver excels. Additionally, it was noted during experimentation that the SMT solver was more sensitive to the way the generic constraints were formulated, requiring careful consideration and experimentation to achieve better performance. We conclude that SMT-based methods present a promising avenue for future research within the domain of personnel scheduling.
• Abstract（参考訳）: 医療従事者のケアの質と労働条件に及ぼす人事計画の影響を概説した。 しかし、常に変化する需要と大きな制約が、医療スケジュールを特に困難にしている。 この問題は何十年にもわたって研究され、Satisfiability Modulo Theories (SMT) の適用を目的とした限定的な研究が続けられてきた。 過去数十年間、SMTは公式な検証コミュニティの中で勢いを増し、標準的な数学的プログラミング技術より優れていることが示されているSMTソルバの進歩につながった。 本研究では,多種多様な実世界のスケジューリング制約をモデル化可能な汎用制約定式化を提案する。 次に、一般的な制約をSMTおよびMILP問題として定式化し、各最先端の解法であるZ3とGurobiを比較して、学術的および実世界のロスターリング問題と比較する。 実験の結果、各解法がある種の問題に対してどのように優れているかが示され、MILP解法は一般に、高い制約がある場合や実現不可能である場合、SMT解法はより良い性能を示す。 より多様なシフトと人員を含む現実世界のインスピレーションを受けた問題について、SMTソルバは優れている。 さらに、SMTソルバは一般的な制約の定式化方法に敏感であり、より優れた性能を達成するためには慎重な考慮と実験が必要であることが実験中に指摘された。 我々は,人事スケジューリング分野における今後の研究の道筋として,SMTに基づく手法が期待できると結論付けた。

関連論文リスト

• Evaluating SAT and SMT Solvers on Large-Scale Sudoku Puzzles [0.0]
  Z3, CVC5, DPLL(T) における現代の SMT ソルバの性能を DPLL の SAT ソルバに対して評価した。 以上の結果から,現代のSMTソルバは従来のSATソルバよりも有意に優れていた。
  論文  参考訳（メタデータ） (2025-01-15T04:31:56Z)
• VC Search: Bridging the Gap Between Well-Defined and Ill-Defined Problems in Mathematical Reasoning [46.25056744404318]
  5000以上の不確定な数学的問題を含むPMC(Issue with Missing and Contradictory conditions)というベンチマークを開発した。 VCSEARCHは、解決不可能な問題を特定する精度を、さまざまな大きな言語モデルで少なくとも12%向上させる。
  論文  参考訳（メタデータ） (2024-06-07T16:24:12Z)
• MindStar: Enhancing Math Reasoning in Pre-trained LLMs at Inference Time [51.5039731721706]
  MindStarは、大言語モデルの純粋に推論に基づく探索手法である。 推論タスクを探索問題として定式化し、最適な推論経路を特定するための2つの探索アイデアを提案する。 Llama-2-13BやMistral-7Bのようなオープンソースモデルの推論能力を大幅に向上させ、GPT-3.5やGrok-1に匹敵する性能を実現している。
  論文  参考訳（メタデータ） (2024-05-25T15:07:33Z)
• iMTSP: Solving Min-Max Multiple Traveling Salesman Problem with Imperative Learning [8.747306544853961]
  MTSP(Min-Max Multiple Traveling Salesman)問題の検討 目標は、最長ツアーの長さを最小化しながら、各エージェントが一括してすべての都市を訪れるツアーを見つけることである。 我々は、命令型MTSP(iMTSP)と呼ばれる、新しい自己教師型双方向エンドツーエンド学習フレームワークを導入する。
  論文  参考訳（メタデータ） (2024-05-01T02:26:13Z)
• Test-Time Adaptation for Combating Missing Modalities in Egocentric Videos [92.38662956154256]
  現実のアプリケーションは、プライバシの懸念、効率性の必要性、ハードウェアの問題により、不完全なモダリティを伴う問題に直面することが多い。 再トレーニングを必要とせずに,テスト時にこの問題に対処する新しい手法を提案する。 MiDlは、欠落したモダリティをテスト時にのみ扱う、自己管理型のオンラインソリューションとしては初めてのものだ。
  論文  参考訳（メタデータ） (2024-04-23T16:01:33Z)
• When MOE Meets LLMs: Parameter Efficient Fine-tuning for Multi-task Medical Applications [57.342772288710044]
  我々はMOELoRAと呼ばれるマルチタスク医療応用のためのパラメータ効率の良い微調整フレームワークを提案する。 MOEとLoRAを統一するために、トレーニング可能なパラメータとして複数の専門家を考案し、トレーニング可能なパラメータの小さなサイズを保持するために、各専門家は2つの低ランク行列から構成される。 マルチタスク医療データセットを用いて実験を行い、MOELoRAが既存のパラメータを効率よく微調整する手法よりも優れていることを示す。
  論文  参考訳（メタデータ） (2023-10-21T17:18:09Z)
• On Pitfalls of Test-Time Adaptation [82.8392232222119]
  TTA(Test-Time Adaptation)は、分散シフトの下で堅牢性に取り組むための有望なアプローチとして登場した。 TTABは,10の最先端アルゴリズム,多種多様な分散シフト,および2つの評価プロトコルを含むテスト時間適応ベンチマークである。
  論文  参考訳（メタデータ） (2023-06-06T09:35:29Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。