Quel est l'exemple d'une formule 3-CNF insatisfaisante?

15

J'essaie d'envelopper ma tête autour d'une preuve d'exhaustivité NP qui semble tourner autour de SAT / 3CNF-SAT.

C'est peut-être l'heure tardive, mais je crains de ne pas pouvoir penser à une formule 3CNF qui ne puisse être satisfaite (il me manque probablement quelque chose d'évident).

Pouvez-vous me donner un exemple pour une telle formule?

user11171
la source

Réponses:

29

X¬X(XXX)(¬X¬X¬X)

23=8

(Xyz)(Xy¬z)(X¬yz)(X¬y¬z)(¬Xyz)(¬Xy¬z)(¬X¬yz)(¬X¬y¬z)
Shaull
la source
2vvn(n-1)2
@BenCrossley - vous ne savez pas ce que vous voulez dire. Pouvez-vous donner un exemple?
Shaull
8

Si vous voulez des exemples plus complexes de telles formules, jetez un œil à quelques problèmes de référence de SATLIB . ToughSAT est également un bel outil pour créer des instances 3-SAT; il est facile de créer des instances satisfaisantes et insatisfaisantes.

Juho
la source