Est-ce que le cas SAT suivant dans $ mathsf {p} $?

Question

f[1](2, 3, 20) : 10011010
f[2](4, 20, 21) : 10101001
f[3](4, 20, 22) : 10010110
f[4](2, 4, 23) : 10011010
f[5](5, 23, 24) : 10101001
f[6](5, 21, 23) : 01101001
f[7](2, 5, 26) : 10011010
f[8](2, 3, 33) : 10101001
f[9](3, 22, 33) : 10000110
f[10](3, 21, 40) : 10100110
f[11](3, 21, 41) : 01101001
f[12](21, 41, 42) : 10101001
f[13](40, 42, 44) : 10010110
f[14](3, 4, 45) : 10101001
f[15](26, 45, 46) : 10101001
f[16](26, 45, 47) : 10010110
f[17](24, 46, 47) : 11001001
f[18](24, 44, 47) : 01101001

Chaque f[i](a, b, c) : truth-table signifie une formule booléenne de 3 variables $ x_a, x_b, x_c $. La formule principale est la conjonction de tous (je viens de convertir CNF pour 53 Circuit de factorisation à une telle forme et a réussi à le réduire à l'instance donnée).

$$ phi = f_1 land f_2 land ... land f_n $$

Ce que je pense, c'est que maintenant je n'ai besoin que de la quantité logarithmique (ou même constante) de toutes les affectations possibles pour voir si elle est satisfaisante.

Par exemple, je peux prendre $ x_2 = 1 $ et cela entraînera automatiquement $ x_ {20} = 0, x_ {21} = 0, x_4 neq x_ {22}, x_ {23} = 0, $ etc . Il semble que la moitié de toutes les variables soient automatiquement attribuées, si je vais en mettre une.

Alors, est-ce dans $ mathsf {p} $?