# These sample CNF formulas in DIMACS files are in P? (Schaefer's dichotomy theorem)

Here is my earlier question. But there was no full answer.

I've decided to include specific DIMACS files:

Are these CNF formulas fulfilling a condition of Schaefer's theorem dichotomy?

If so, what kind?

Schaefer's theorem dichotomy conditions:

all relations which are not constantly false are true when all its arguments are true;

all relations which are not constantly false are true when all its arguments are false;

all relations are equivalent to a conjunction of binary clauses;

all relations are equivalent to a conjunction of Horn clauses;

all relations are equivalent to a conjunction of dual-Horn clauses;

all relations are equivalent to a conjunction of affine formulae.

• Formulas are not in P. Only languages can be in P. For any formula, we can construct a polytime algorithm which handles that formula correctly. – Yuval Filmus Jul 13 '17 at 6:58
• It is likely that the formulas do not belong to any of the classes listed in the dichotomy theorem, and this is something that you can check directly on your own, using your programming skills. This only means that the general algorithms implied by Schaefer's dichotomy theorem do not apply here. – Yuval Filmus Jul 13 '17 at 7:01
• If they do not belong to $P$, it doesn't mean that particularly these instances can't be solved efficiently. – rus9384 Jul 13 '17 at 10:05
• I have an algorithm that can build infinitely many such CNF logical formulas (in terms of size). It may be that these infinitely many logical formulas in NPC but they can be solved in polynomial time even if P! = NP? – Aurelio Jul 13 '17 at 14:56
• Schaefer's dichotomy theorem is not about instances, it's about worst cases. – rus9384 Jul 13 '17 at 16:46