◎薗部知大・稲葉真理（東大）

近年の並列SATソルバの主流戦略はportfolioであり、探索を行うワーカーが競争的かつ独立に探索を行う。各ワーカーの探索挙動を変更するためにはdiversification (探索の多様化)が必要であり、従来の手法では探索に関わるパラメータを変更することで実現していた。しかし、ワーカー数の多い大規模並列環境では、探索パラメータの組み合わせに限りがあり、十分な多様化を図ることが難しい。この問題に対して本研究では各ワーカーにあらかじめ優先して探索すべき変数を与えられた問題から解析し割り当て、各ワーカーはそれらに対する集中的な探索を行うことで全体として多様な空間への探索を目指す手法を提案する。