SATと算術問題

https://gyazo.com/4379bb734da9878cea5eb90bb07d7238

基本的な考え方”

算術式を考える

算術式を論理命題Xに変換する（算術要素は抽象化される）

SATで充足する組み合わせCを見つける

組み合わせCで実際の算術式が

充足されれれば

OK

充足されなければ

もう1回SAT段階に戻す

その際に，¬Cとなるような論理命題をXに追加して，再度SATソルバをまわす