CNF
সংযোজক প্রামাণ্য রূপ
Conjunctive Normal Form — AND of ORs। `(a ∨ ¬b) ∧ (¬a ∨ c)`। সব আধুনিক SAT solver শুধু এই রূপ নেয়।
also: conjunctive normal form, product of sums, POS
CNF = clause-দের AND, যেখানে প্রতিটা clause literal-দের OR।
(p ∨ ¬q) ∧ (¬p ∨ q ∨ r) ∧ (¬r)Truth table থেকে বানানো: যেসব row-তে ফল F, প্রতিটার জন্য
একটা clause — কিন্তু literal উল্টে (variable T হলে ¬x,
F হলে x)।
কেন এটা গুরুত্বপূর্ণ: SAT solver-এর প্রামাণ্য input format
(DIMACS) হলো CNF। আর SAT solver চলছে chip verification-এ,
program analysis-এ, AI planning-এ, আর আপনার package manager-এর
ভেতরে (apt, cargo, npm — dependency resolution আক্ষরিকভাবে SAT)।
সতর্কতা: যেকোনো expression CNF-এ আনা যায়, কিন্তু আকার exponentially বাড়তে পারে। তাই বাস্তব solver Tseytin transformation ব্যবহার করে — নতুন সহায়ক variable ঢুকিয়ে আকার linear রাখে, বিনিময়ে formula-টা আর logically equivalent থাকে না, শুধু equisatisfiable থাকে।
Hardware ডিজাইনে একই রূপকে বলা হয় POS (product of sums)।