Quelle est la complexité de déterminer la satisfabilité d'un CNF contenant à la fois des clauses de corne et de corne double?

Question

Si un CNF contient à la fois des clauses de corne et de corne double et ne contient pas de clauses d'autres types, alors sa satisfabilité peut-elle toujours être déterminée en temps polynomial?

Si la réponse au problème ci-dessus est oui, supposons que nous ne faisons que des clauses XOR en plus des clauses de corne et de corne double, la satisfaction de ce type de CNF peut-elle être déterminée en temps polynomial?