膨大な組み合わせの中から与えられた制約を満たす解を見つけ出す問題は、現実の様々な場面で多様な形で現れます。SATソルバに代表されるこの種の問題を解くソルバは、プランニングやスケジューリング、システム検証などに応用されています。さらに、量的な性質解析（条件がどの程度の確率で満たされるかなど）や解全体の索引化を目的として
