Java & Python　最適化・制約従属の問題解法　プログラムリスト
(C) 森澤利浩

--------
本ファイルは、本書をお買い求めになった方のみご利用いただけます。本書をよくお読みのうえ、ご利用ください。また、本ファイルの著作権は、本書の著作者である、森澤利浩氏に帰属します。
本ファイルを利用したことによる直接あるいは間接的な損害に関して、著作者およびオーム社は、いっさいの責任を負いかねます。利用は利用者個人の責任において行ってください。
--------

第1章 最適化問題と制約充足問題
1.1 最適化問題と制約充足問題とは何か
1.2 最適化問題とは
	1.2.1 最適化問題の表現
	1.2.2 歴史
	1.2.3 代表的な問題
1.3 制約充足問題とは
	1.3.1 制約充足問題の表現
	1.3.2 歴史
	1.3.3 代表的な問題
1.4 本書の構成と使い方

第I部 プログラミング

第2章 ソフトウェアの使い方
2.1 概要
2.2 MIPのためのプログラミング―Python+MIPパッケージ― 
	2.2.1 PuLP
	 - test1_pulp.py : 初めてのPuLP例
	2.2.2 Python-MIP
	 - test1_mip.py : 初めてのPython-MIP例
2.3 CSPプログラミング―Java+Cream―
2.3.1 Creamの使い方
 - AddAB.java : 初めてのcream(Java)例
2.4 SAT変換によるCSPプログラミング―Java+Sugar―
	2.4.1 Sugarの使い方
	 - equal4.csp : 初めてのsugar(CSP)スクリプト(.cspファイル)
	 - CSP_SAT_clasp.java : sugar(CSP)処理用Javaプログラム
	2.4.2 実装の例
	 - 8queen.csp : 8クイーンのsugarスクリプト
	 - ex_logic.csp : 論理処理のsugarスクリプト
2.5 SATソルバの使い方
 - v2.cnf : 初めてのSATスクリプト(.cnfファイル)
2.6 SMTのプログラミング―z3―
	2.6.1 SMT-LIB2+z3
	 - smt2_test.smt2 : 初めてのSMT2スクリプト(.smt2ファイル)
	2.6.2 Python+z3
	 - test.py : 初めてのPython+z3プログラム
	2.6.3 Java+z3
	 - HelloZ3.java : 初めてのJava+z3プログラム
	 - SudokuExample.java : Java+z3による数独プログラム
2.7 SMT-LIB2スクリプトによるプログラミング
	2.7.1 SMT2の処理方法
	 - test01.smt2 : SMT-LIB2スクリプト(.smt2ファイル)
	2.7.2 整数と実数の制約処理の例
	 - int_const.smt2 : 整数制約SMT-LIB2スクリプト
	 - real_const.smt2 : 実数制約SMT-LIB2スクリプト
	2.7.3 論理の証明の処理方法
	 - proof.smt2 : 論理の証明のSMT-LIB2スクリプト

第3章 基本的な処理要素
3.1 概要
3.2 数理最適化パッケージPuLPとPython-MIP
	3.2.1 PuLP
	3.2.2 Python-MIP
3.3 CSPライブラリCream
	3.3.1 問題の定義と解法
	3.3.2 制約変数と制約条件
	3.3.3 ソルバの活用方法
	 - SLV.java : ソルバ活用クラス
	 - test_3_3_3.java : ソルバ活用クラスの利用例
3.4 SAT変換CSPライブラリSugar
	3.4.1 制約変数の定義
	 - domain_int_bool.csp : 制約変数のテスト用CSPスクリプト
	3.4.2 項（term）の定義
	3.4.3 関連（relation）と述語（predicate）
	 - rel.csp : relationテスト用CSPスクリプト
	 - predicate.csp : predicateテスト用CSPスクリプト
	3.4.4 制約
	 - alldifferent.csp : alldifferentテスト用CSPスクリプト
	 - weightedsum.csp : weightedsumテスト用CSPスクリプト
	 - cumulative.csp : cumulativeテスト用CSPスクリプト
	 - element.csp : elementテスト用CSPスクリプト
	 - disjunctive.csp : disjunctiveテスト用CSPスクリプト
	 - lex_less.csp : lex_lessテスト用CSPスクリプト
	 - lex_lesseq.csp : lex_lesseqテスト用CSPスクリプト
	 - nvalue.csp : nvalueテスト用CSPスクリプト
	 - global_cardinality.csp : global_cardinalityテスト用CSPスクリプト
	 - global_cardinality_with_costs.csp : global_cardinality_with_costsテスト用CSPスクリプト
	 - count.csp : countテスト用CSPスクリプト
	3.4.5 最適化
	 - opt_lex_less.csp : opt_lex_lessテスト用CSPスクリプト
3.5 SAT(CNF)
 - test.cnf : テスト用CNFスクリプト
3.6 SMT-LIB2
	3.6.1 SMT-LIB2の言語の要素
	3.6.2 論理と理論
	3.6.3 その他、注意など
	3.6.4 SMT-LIB2スクリプトの例
	＜＜smt_lib2.txtのスクリプトを個別にファイルにする＞＞
	 - basic_boolean.smt2 : ブール変数の扱い
	 - option_setting.smt2 : オプション設定
	 - integer_val.smt2 : 整数変数と値
	 - abc_cba.smt2 : 9xabc=2xcba
	 - div_mod.smt2 : 除算と剰余
	 - lp_min_max.smt2 : 線形計画法min-max問題
	 - push_pop.smt2 : push, pop例
	 - new_sort.smt2 : ソートAの定義
	 - get_info.smt2 : get-info
	 - func_decl.smt2 : ソート定義と関数定義
	 - define_fun.smt2 : 関数定義
	 - assignment.smt2 : get-assignment
	 - get_assertions.smt2 : get-assertions
	 - let.smt2 : let表現
	 - exclamation1.smt2 : !(exclamation)表現
	 - exclamation2.smt2 : !(exclamation)表現
	 - datatype.smt2 : declare-datatype
	 - get_proof.smt2 : 証明の取得
	 - get_unsat_core.smt2 : unsat_core取得
	 - options.smt2 : option設定のテスト(cvc4を利用のこと)
	 - bit_vector.smt2 : ビットベクトルのテスト
	 - bit_vec_hex.smt2 : ビットベクトルのテスト2
	 - bit_vec_gcd.smt2 : ビットベクトルのGCD
	 - bit_vec_comp.smt2 : ビットベクトルの比較
	 - bit_vec_op.smt2 : ビットベクトルの演算
	 - array_select.smt2 : arrayのselect演算
	 - array_store.smt2 : arrayのstore演算
	 - bv_array.smt2 : bvソートのarray
	 - store_select.smt2 : arrayのstoreとselect演算
	 - array_comp.smt2 : array要素の比較演算
	 - array_append.smt2 : array要素の追加
	 - array33.smt2 : arrayによる3x3魔方陣
	 - swap_ssa.smt2 : SSAによるスワップ
	 - swap_bv.smt2 : SSAによるスワップ(ビットベクトル使用)
	 - comb_rel.smt2 : 組合せの関係制約
	 - q_bool.smt2 : 量子化ブール演算
	 - id_eq.smt2 : 関数と値域、領域の演算
	 - mean_def.smt2 : 相加・相乗平均
	 - array_setting.smt2 : Arrayの設定
	 - transposition.smt2 : 置換
	 - d3.smt2 : dihedral group D3
	 - concat.smt2 : 文字列の接続
	 - strcmp.smt2 : 文字列の比較
	 - str_xy_yx.smt2 : 文字列の並び１
	 - str_ab_ab.smt2 : 文字列の並び２
	 - regex.smt2 : 正規表現
	 - list.smt2 : リスト
3.7 PythonのSMTライブラリz3
	3.7.1 変数の定義
	3.7.2 制約の設定
	3.7.3 ビットベクトルの制約
	3.7.4 充足可能性判定と解
	3.7.5 対話的な使い方
	3.7.6 証明
	3.7.7 一階述語論理
	 - sec_python_z3.txt : Pythonにおける対話処理の入力
3.8 JavaのSMTライブラリz3
3.8.1 ソースコード記述のパターン
	 - solve_pattern.txt : モデルを求める典型的な記述(モデル求解パターン)
	 - prove_pattern.txt : 証明の典型的な記述(証明パターン)
	 - method_template.txt : メソッドの雛型
3.8.2 JavaExample
3.8.3 z3 API for Java

第II部 定式化

第4章 求解式
4.1 概要
4.2 線形計画法
 - 4_2_neutrition.py : 栄養問題
 - 4_2_production.py : 生産計画問題
 - 4_2_transport.py : 輸送問題
4.3 絶対値問題
 - 4_3_abs.py : 絶対値問題
4.4 分数計画問題
 - 4_4_fraction.py : 分数問題
4.5 min-max問題
 - 4_5_minimax.py : min-max問題
4.6 鶴亀算，連立方程式
 - 4_6_sim_eq_pulp.py : 連立方程式(PuLP)
 - 4_6_sim_eq_mip.py : 連立方程式(Python-MIP)
 - 4_6_sim_eq.txt : numpyなどによる計算の確認
4.7 線形回帰
 - 4_7_lin_reg.py : 線形回帰
4.8 整数変数の方程式
 - IntegerEq.java : 整数変数問題
4.9 分数問題
 - FracProb.java : 分数問題
4.10 ガウス記号を含む割算
 - FloorFunc.java : ガウス記号による不等式問題

第5章 範囲の制約
5.1 概要
5.2 部分和問題
 - part_sum.py : 部分和問題
5.3 ナップザック問題
 - knapsack.py : ナップザック問題
5.4 ビンパッキング問題
 - bin_packing.py : ビンパッキング問題
5.5 min-max 問題(範囲の制約として)
 - minmax.py : min-max問題
5.6 1対多の選択
 - OneToMore.java : 1対多の選択
5.7 点配置問題
 - point_location.py : 点配置問題(PuLP)
 - point_location_z3.py : 点配置問題(z3)
5.8 施設配置問題
 - facility_pc.py : p-center法
 - facility_pm.py : p-median法
 - facility_sc.py : 集合被覆法
 - facility_mc.py : 最大被覆法
5.9 地図配色問題
 - node_coloring.py : 頂点彩色問題
5.10 グラフ彩色問題
 - edge_coloring.py : 辺彩色問題

第6章 数あてはめ
6.1 概要
6.2 All Different
 - AllDifferent.java : Creamの例(NotEquals)
 - all_different.py : Python-MIPによるスケジューリングの例
 - all_different_index.py : Python-MIPによる二次元配列による例
6.3 分割
 - Partition.java : 分割の例
6.4 NQueens 問題
 - Queens.java : creamの例
 - nqueen.py : PuLPの例
6.5 数独(ナンバープレース)
 - SudokuExample.java : Java+z3の例
6.6 覆面算
 - Cripathrithm.java : 覆面算
6.7 カプレカ数
 - Kaprekar.java : カプレカ数
6.8 魔方陣
 - magic_squre.py : Python-MIPによる例
 - magic_squre_pulp.py : PuLPによる例
6.9 直交ラテン方陣
 - orth_latin_square.java : 直交ラテン方陣
6.10 ブロックデザイン
 - D2_7_3_1.java : D2-(7,3,1)デザイン
 - D2_16_4_1.java : D2-(16,4,1)デザイン
6.11 ナーススケジューリング
 - nurce.py : ナーススケジューリング
6.12 リーグ戦
 - league.java : リーグ戦
6.13 トーナメント戦

第7章 グラフ
7.1 概要
7.2 最短経路問題
 - shortest_path.py : 最短経路問題
7.3 経路問題
 - ee_search.java : 経路問題
7.4 ハミルトン路
 - hamilton.py : ハミルトン路
7.5 ハミルトン閉路
 - hamilton_circuit.py : ハミルトン閉路
7.6 騎士の巡回
 - knight.py : 騎士の巡回
7.7 騎士の周遊
 - knight_circuit.py : 騎士の周遊
7.8 巡回セールスマン問題
 - tsp2.py : 巡回セールスマン問題
7.9 最大フロー問題
 - max_flow.py : 最大フロー問題
7.10 最小カット問題
 - min_cut.py : 最小カット問題
7.11 最小費用フロー問題
 - min_cost_flow.py :  最小費用フロー問題
7.12 多品種フロー問題
 - mix_max_flow.py : 多品種フロー問題
7.13 多品種最小費用フロー問題
 - max_min_cost_flow.py : 多品種最小費用フロー問題
7.14 二部グラフの最大マッチング
 - max_matching.py : 二部グラフの最大マッチング
7.15 二部グラフの最小重み最大マッチング
 - min_weight_matching.py : 二部グラフの最小重み最大マッチング
 - min_weight_matching2.py : 二部グラフの最小重み最大マッチング(入出側にインデクスを分けたもの)
7.16 割当て問題
 - assignment.py : 割当て問題
7.17 二部グラフのマッチング(稜線法)
 - edge_matching.java : 二部グラフのマッチング(稜線法)
7.18 二部グラフのマッチング(数対応付け)
 - number_matching.java : 二部グラフのマッチング(数対応付け)
7.19 三角形分割
 - triangulation.java : 三角形分割

第8章 順序処理
8.1 概要
8.2 ジョブショップスケジューリング問題
 - 1machine_sche_d.py : 1機械問題、納期付き
 - 4machine_sche.py : 4機械問題(PuLP)
 - sche.java : 4機械問題(cream)
 - jobshop_1machine.csp : 1機械問題(sugar)
 - jobshop_2machine.csp : 2機械問題(sugar)
 - jobshop_4machine.cps : 4機械問題(sugar)
8.3 All Different による順序変数の扱い(先行順序制約)
 - order_all_different.java : AllDifferent先行順序制約
8.4 条件付き先行順序制約
 - cond_prec.java : 条件付き先行順序制約
8.5 トポロジカルソート
 - t_sort.java : トポロジカルソート
8.6 ソート
 - sort.py : ソート(Python+z3)
 - sort.smt2 : ソート(SMT2)
8.7 置換
 - permutation.java : 置換

第9章 論理
9.1 概要
9.2 単項、二項論理演算
9.3 論理演算の整数制約プログラミングによる実装
 - logic_test.java : 論理演算の例
9.4 整数制約プログラミングのための論理演算の定式化
 - and1.java : 要素制約による論理演算の例
9.5 論理と整数制約プログラミング
 - 9_5_1.py : 論理によるプログラミングの例1
 - ex9_5_1.py : 整数制約プログラミングによるプログラミングの例1
 - 9_5_2.py : 論理によるプログラミングの例2
 - ex9_5_2.py : 整数制約プログラミングによるプログラミングの例2
9.6 述語論理としての検索
 - grandfather.java : 祖父問題
 - grandmother.java : 祖母問題
9.7 TAGIRON
 - tagiron2.java : TAGIRON



