Definition talk:CNF Satisfiability Problem

Should this page be renamed Definition:CNF Satisfiability Problem containing just:

A Conjunctive Normal Form Boolean Satisfiability problem is a Boolean Satisfiability Problem where all the clauses in $L$ are in conjunctive normal form.

?

Although exactly what $L$ is in this context needs to be defined.

IMO all the rest of the page is doing is explaining (very poorly, by example) what CNF is, and this is completely redundant as it is explained properly on the Definition:Conjunctive Normal Form page. --prime mover (talk) 21:03, 19 April 2014 (UTC)

I think so. The confusion arises because by a common abuse of language, "CNFSAT" is also the open problem about such problems being solvable in polynomial time. — Lord_Farin (talk) 21:54, 19 April 2014 (UTC)

This page has now been completely rewritten. --prime mover (talk) 05:27, 15 June 2015 (UTC)