💻 computer science

Compact SAT and MaxSAT Encodings for Business-to-Business Meeting Scheduling with Idle-Time Balancing

本論文は、ドメインフィルタリングと共有変数を利用することで節数を大幅に削減しメモリ使用量を抑えつつ、参加者のアイドルタイム範囲を最小化する、B2B会議スケジューリングのためのコンパクトなSATおよびMaxSATエンコーディングを導入しており、これは既存の公開されているMaxSAT定式化および商用ソルバであるGurobiの両方を、解決効率において上回るものである。

原著者： Long Duc Nguyen, Tuyen Van Kieu, Khanh Van To

公開日 2026-08-04

📖 1 分で読めます☕ さくっと読める

CC BY 4.0

原著者： Long Duc Nguyen, Tuyen Van Kieu, Khanh Van To

原論文は CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) でライセンスされています。 ✨ これは以下の論文のAI生成解説です。著者が執筆または承認したものではありません。技術的な正確性については原論文を参照してください。免責事項の全文を読む

あなたは、大規模でハイステークスなビジネス・コンベンションのための究極のパーティー・プランナーであると想像してください。何百人もの人々が1対1のミーティングを行う必要がありますが、全員のスケジュールはバラバラであり、部屋のサイズも極端に小さかったり巨大だったりと様々です。さらに、ある会議は他の会議が始まる前に必ず行われなければなりません。あなたの目標は、単に全員にミーティングを設定することではありません。誰もが次の予定までの間に、退屈して座って待つ時間が長くなりすぎないようにすることです。これは、「B2B（企業間）ミーティング・スケジューリング」という混沌としたパズルの問題です。

コンピューター科学者は、この問題を解くために、SAT（充足可能性）と呼ばれる特別な種類の論理ゲームを使用します。SATは、一連のルールが同時に真（成立）になり得るかどうかをチェックする、超スマートな探偵のようなものだと考えてください。もしあなたが探偵に「会議Aは会議Bの前に行われなければならないが、会議Bは会議Aの後に行われなければならない」と言えば、探偵は即座に「不可能！」と答えます。しかし、ルールが複雑であっても成立可能なものであれば、探偵は有効なスケジュールを見つけ出します。もう一つのバージョンであるMaxSATは、単に有効なスケジュールを見つけるだけでなく、人々が待ち時間を最小限に抑えられるよう、いかに「完璧」にするかを追求する探偵です。この論文では、これら複雑なビジネスイベントを تنظيم（整理）する際に、いかにしてこの論理探偵をより速く、よりスマートにするかについて掘り下げています。

問題点：もつれたミーティングの網

ビジネスミーティングの世界では、物事はすぐに混乱します。ミーティングのリスト、タイムスロットのリスト、そして部屋のリストがあります。ルールは厳格です：

重複禁止： 一人の人が同時に二箇所にいることはできません。
部屋の制限： 部屋の収容人数は、開催されるミーティングの数を上回ることはできません。
前後関係（プレシデンス）： ある会議は、他の会議（例えば午後のワークショップの前の午前中のブリーフィングなど）よりも先に必ず行われなければなりません。
「アイドル（空き）」問題： 本当の悩みの種は「アイドルタイム（待ち時間）」です。参加者が午前9時に会議があり、次の会議が午前11時である場合、彼らは2時間の「アイドルタイム」を持つことになります。目標は、ある人が数分しか待っていない一方で、他の人が何時間も待つといったことが起きないよう、これをバランスさせることです。これは公平性と効率性の問題です。

旧来の方法 vs 新しい方法

研究者たちは、すでにかなり優れた手法であった既存の方法（ORG-MAXSATと呼ばれます）に注目しました。しかし、彼らはその方法が、たとえ明らかに不可能な組み合わせであっても、ゲストと時間のあらゆる組み合わせを書き出すことでパーティーを تنظيم（整理）しようとしていることに気づきました。それは嵩張り、遅く、大量のコンピューターメモリを消費していました。

ベトナムのVNU技術大学のチームは、「コンパクト」版を構築することに決めました。彼らは問題を縮小するために、主に3つのトリックを導入しました。

「事前チェック」フィルター（ドメイン・フィルタリング）： コンピューターの探偵にパズルを解かせる前に、スマートなフィルターを追加しました。このフィルターはルールを確認し、不可能な選択肢を即座に除外します。例えば、ある会議が午後2時に終わる会議の「後」に行われなければならない場合、フィルターは即座に午後2時より前のタイムスロットを可能性のリストから削除します。これは、特定のペンを探す前に、デスクの上の散らかりを片付けるようなものです。彼らは、このフィルターが有効な解決策を捨てることは決してなく、単にゴミを取り除くだけであることを証明しました。
「共有された階段」（疎な共有接尾辞エンコーディング）： 「～の前に起こる」というルールを扱う際、旧来の方法では、ミーティングのペアごとに個別のメモを書いていました。もし100のミーティングがあれば、何千ものメモが必要になります。新しい方法は、これらのメモの多くが同じことを言っていることに気づきました。「会議AはBの前」「会議AはCの前」「会議AはDの前」と個別に書く代わりに、彼らは共有された論理の「階段」を作成しました。彼らは、似たような状況に対して変数を再利用しています。これは、すべての鍵に対して新しい鍵を作るのではなく、いくつかのドアに対して一つのマスターキーを使用するようなものです。
「公平性」スコア（アイドルタイムのバランス）： 単に人の休憩回数を数えるのではなく、彼らは「アイドルタイム」を測定する新しい方法を作成しました。彼らは、ある人の「最初の会議」から「最後の会議」までの時間を調べました。もし誰かが9時と11時に会議を持っているなら、その人の「スパン（期間）」は2時間です。もし会議が1回しかなければ、アイドルタイムはゼロです。目標は、最も忙しい人のアイドルタイムと、最も暇な人のアイドルタイムの差をできる限り小さくすることです。

研究結果

研究者たちは、126件の公式テストケースと、さらに多くのミーティングを含む100件の追加「ストレス・テスト」ケースを用いて、彼らの新しい「コンパクト」手法を、旧来の手法およびGurobiやCPLEXのような非常に強力な商用ソフトウェアと比較検証しました。

結果は、非常に印象的なものでした：

サイズの縮小： 新しい手法は、論理的な「節（クローズ）」の数を平均で**40.3%**削減しました。
メモリの節約： ピーク時のメモリ使用量を**55.9%**削減しました。同じパズルを解くのに、半分以下のRAMが必要になるイメージです。
スピードの向上： 問題を解決するための総時間は**14.0%**減少しました。
フィルタリングの力： 「事前チェック」フィルターを使用するだけで、変数を24.1%、ルールを**16.2%**削減できました。
共有の力： 「共有された階段」のトリックは、スケジュールの混雑具合に応じて、ルールをさらに**0.5%から5.5%**削減しました。

結論

最もエキサイティングな部分は、彼らの新しいコンパクトなSATおよびMaxSAT手法が、126件の公式テストケースのすべてを解決できたことです。さらに素晴らしいことに、中央値の時間の面で、主要な商用ソルバーであるGurobiよりも速く解決しました。他の商用ツール（CPLEXやCP Optimizerなど）は、制限時間内にすべてのケースを解決するのに苦戦しましたが、新しいSATベースのアプローチはそれらすべてを処理できました。

この論文は、世界のあらゆるスケジューリング問題を永遠に解決したと主張しているわけではありませんが、ルールを整理し、仕事をよりスマートに共有することで、コンピューターが私たちの忙しい生活を管理することをいかに向上させられるかを明確に示しました。これは、巨大で絡まり合ったミーティングの結び目を、誰もが公平な時間を持ち、廊下で長く待たされることがない、整然としたバランスの取れたスケジュールへと変えるものです。

技術要約：アイドルタイムの均衡化を伴うB2B会議スケジューリングのためのコンパクトなSATおよびMaxSATエンコーディング

問題定義

本論文は、要求されたペアごとの会議を特定のタイムスロットおよび場所に割り当てる組み合わせ最適化問題である、ビジネス・ツー・ビジネス（B2B）会議スケジューリングを取り扱う。スケジューリングは以下の制約を満たす必要がある：

参加者の重複禁止： 参加者は同時に2つの会議に出席することはできない。
場所の容量： いずれかのタイムスロットにおける会議の数は、利用可能な場所の数（ $K$ ）を超えてはならない。
可用性と制限： 会議は、要求されたセッション内、固定スロット内、または禁止されたスロット外で行われなければならない。
先行関係： 有向アーク $(i, j)$ は、会議 $i$ が会議 $j$ よりも前に発生しなければならないことを強制する。

本研究で提案される目的関数は、従来の方式（「ブレイクグループ」を最小化、あるいはブレイク数の格差を抑えるもの）とは異なる。本研究では、少なくとも2つの会議を持つ参加者間における内部アイドルスロット合計の範囲（ $\Delta I$ ）を最小化する。内部アイドルスロットは、ある参加者の最初の割り当てられた会議と最後の会議の間に存在する、空いている時間を定義とする。この指標は、短い中断と長い待ち時間を区別し、バランスの取れたアカデミック・カリキュラム問題（BACP）と同様の負荷分散を目指すものである。また、補完的な指標として、集計されたアイドル時間（ $I_\Sigma$ ）も報告されている。

手法

著者らは、既存の公開されている定式化に対して3つの主要なモデリング上の改善を統合した、コンパクトなSAT（ブール充足可能性）およびMaxSATエンコーディングを提案している。

解を保存するドメインフィルタリング（前処理）：
論理積標準形（CNF）を生成する前に、著者らはサポートされていない割り当てを除去する前処理アルゴリズム（アルゴリズム1）を適用する。これには以下が含まれる：
- エンドポイント境界フィルタ： パスに沿った先行関係の伝播（直接アークまたは推移的閉包を使用）。
- 参加者ごとのマッチング： 特定の参加者にとってコンフリクトのないスケジュールの一部となり得ない割り当ての除去。
- 飽和スロットの伝播： 容量が強制的な割り当てによって既にフル活用されているスロットの排除。
- 主張： このプロセスは、すべての実行可能なスケジュールを保持しながらドメインサイズを縮小し、それによって変数と節の数を削減する。
疎な共有サフィックス先行関係エンコーディング（SPARSESUFFIX）：
先行関係をペアごとの節を用いてエンコードする（ドメインサイズに対して二次関数的になり得る）代わりに、著者らは疎なエンコーディングを導入する。
- これは、制約がアクティブになる先行ドメイン内の明確な「カットポイント」のみを具体化する。
- 異なる関係間で共通のカットに対して補助変数を再利用する。
- この手法は、ペアごとの節と等価であることが証明されており、特にドメイン削減と組み合わせた場合に、節の数を大幅に削減する。
範囲ベースのアイドルタイム目的関数：
著者らは、内部アイドルスロットの範囲（ $\Delta I$ ）を最小化するための厳密なエンコーディングを導入する。
- 各参加者の最初の占有スロットと最後の占 موردスロットを導出する。
- 関連するすべての参加者における最大値と最小値の差を計算するために、線形数の補助変数を使用する。

本研究では、これらのコンポーネントを、ベースラインとなるORG-MAXSAT（公開されたモデルの適応版）および商用ソルバー（Gurobi, CPLEX, CP Optimizer）と比較評価している。評価は、126の公式ベンチマークインスタンスと、先行関係の密度が異なる100の派生した「ストレス」インスタンスを対象としている。

主な貢献

本論文は、以下の3つの具体的な貢献を特定している。

前処理手順： CNF生成前にサポートされていない割り当てを除去するフィルタ統合。命題1は、これが実現可能性を保持することを証明しており、実証結果は、割り当て変数を24.1%、節を16.2%削減することを示している。
疎な共有サフィックス表現： 必要な先行ドメインのカットポイントのみを具体化する厳密なエンコーディング（SPARSESUFFIX）。命題3は、これがペアごとの節と等価であることを証明している。本研究は、ドメイン削減が変数数を低下させる一方で、サフィックス共有が独立して節数を低下させることを示している。
B2B特有の目的関数： 内部待ち時間の格差を測定する範囲ベースのアイドルタイム目的関数であり、線形数の補助変数でエンコードされている。

実験結果

実験は、4コアのマシンで7,200秒のタイムリミットを設定して行われた。主な知見は以下の通りである：

式のサイズとメモリ： 適応されたORG-MAXSATベースラインと比較して、提案されたコンパクトなエンコーディングは、中央値としての節数を40.3%削減し、中央値としてのピークメモリ使用量を55.9%削減した。
ドメイン削減の影響： ドメインフィルタリング単独で、割り当て変数を24.1%、節を16.2%削減し、式サイズの削減において最大のシェアを占めた。
先行関係のエンコーディング： SPARSESUFFIXエンコーディングは、公式の先行関係インスタンスにおいて中央値の節数を0.5%～1.0%削減し、最も密度の高い派生インスタンス（推移的閉包と組み合わせた場合）では最大**5.5%**削減した。
ソルバーの性能：
- 提案された3つのSAT/MaxSAT手法（Incremental SAT, Non-Incremental SAT, UWrMaxSAT）は、すべて126の公式インスタンスを解いた。
- すべてのインスタンスを解いた唯一の商用ソルバーであるGurobiと比較して、提案されたSAT/MaxSAT手法はより低い中央値の総実行時間を達成した。
- Incremental SATは、完全な手法の中で最も低い中央値（0.227秒）を達成した。
- CP Optimizerは最も低い中央値（0.110秒）を示したが、11のインスタンスでタイムリミット内に解くことができなかった。

意義と主張

本論文は、提案されたコンパクトなエンコーディングが、B2B会議スケジューリングにおける既存のブール形式に対して大幅な効率向上を提供すると主張している。ドメインフィルタリングを先行関係の表現から分離することにより、著者らは、ドメイン削減が式のサイズを縮小する主要な要因であり、疎な共有サフィックスエンコーディングが関係集合とは独立して追加の節削減を提供することを実証している。

本研究は、新しいアイドルタイム範囲目的関数が、従来の「ブレイクグループ」指標よりも洗練されたスケジュールの質を測定できる（短い中断と長い待ち時間を区別できる）と断言している。さらに、結果は、これらのコンパクトなエンコーディングを備えた現代的なSATおよびMaxSATソルバーが、この特定のクラスの問題において、中央値の解決時間の面で主要なMIPおよびCPソルバーを上回ることができることを示している。

著者らは、現在の研究は単一実行のタイミングに焦点を当てていることを指摘し、将来の研究では、繰り返しのタイミング実行や、レキシコグラフィック的目的関数（ $I_\Sigma$ の前に $\Delta I$ を最小化する）を探索できる可能性があるとし、謙虚な姿勢を維持している。