DIMACS CNF format

SAT solver の論理式のCNFの入力フォーマットとして使われている, デファクトスタンダード
p 形式 変数数 項数

否定は -

$$(P_1\vee P_2)\wedge (\neg P_1\vee P_2)\wedge (\neg P_1\vee \neg P_2)$$

p cnf 2 3
1 2 0
-1 2 0
-1 -2 0

SAT
-1 2 0