研究したくねぇ
誰か僕の修論書いておいてください．
Horn SATとは2-SAT同様，高速に解けるSATの特殊ケースらしいです．
のしさん教えてくれてありがとう
問題定義
以下のようなSATです．
和積標準形の形で，各節に肯定リテラルが高々1個のものです．
メモ
これは解けます．
仮に，肯定リテラルのみの節が1つもない場合を最初に考えます． この場合，全てのリテラルを0にしてやればいいです． 各節，否定リテラルが1つはあるので，そいつが1になってみんな幸せです．
じゃあ肯定リテラルが1つのみの節があったらどうするかです．
この場合，そのリテラルを必ず1にしなければなりません．
そしてその影響で他のリテラルを決定するかもしれません．
のような場合，a=1でなければなりません．
このことから真ん中の節を考慮するとb=1でなければなりません．
同じようにc=1でなければなりません．
上で議論したことをふまえると，1にしないといけないリテラルをそうして，あとは全て0にしてしまえばいいんじゃないか，という気持ちになります． なんかそれでいいです．
なぜなら否定でも肯定でもいいなら否定にしておいて絶対に損をしないからです． 最初の議論的にそんな気がします．多分．
実装をします．
できました．
1にしないといけないところを1にして，残りを全て0にして最後に全ての節がtrueになるかをチェックして終わりです．
verifyはDashboard - The 2020 ICPC Asia Shenyang Regional Programming Contest - CodeforcesのCです．
