feed-digest - #formal-methods

アンケートの設定が噛み合っているかをSMTソルバに確かめさせた

アンケート編集画面で自由に設定できる分岐条件や入力バリデーションは、個々には妥当でも組み合わせると矛盾が生じ、回答者がどう入力しても先に進めなくなることがある。総当たりでは組み合わせ数が膨大（20問5択で約95兆通り）で現実的でなく、ランダム試行でも「矛盾が存在しない」ことは証明できない。そこでSMTソルバZ3を用い、アンケート定義を整数・真偽値の制約式に翻訳して充足可能性を判定する手法を紹介。実例として、ページ表示条件と設問の合計値制約が食い違い、特定の回答パターンでは入力可能な値が存在しない（unsat）矛盾をZ3が反例付きで検出できることを示した。上限を決めずに式を書ける点がSATにはないSMTの利点で、既存のQA工程を置き換えるのではなく事前の当たり付けとして活用する使い方を提案している。