Un modello proposizionale indica quali atomi sono veri. Nella circoscrizione si minimizzano alcuni atomi: si scarta un modello se ne esiste uno ammissibile con un insieme strettamente più piccolo di atomi minimizzati veri, rispettando gli eventuali atomi fissati.
Esempio: KB=p∨q e minimizziamo entrambi gli atomi. I modelli sono {p}, {q} e {p,q}. I primi due sono minimali; l’ultimo non lo è, perché contiene un modello più piccolo. La domanda «p è vera in almeno un modello minimale?» ha risposta sì grazie a {p}. «p è vera in tutti?» ha invece risposta no, per {q}.
CIRC SAT usa la prima domanda: ∃ un modello che soddisfa KB e φ, e ∀ candidati strettamente minori nessuno soddisfa i vincoli. La minimalità riguarda l’inclusione degli atomi minimizzati, non semplicemente il loro numero.
Complemento e collegamenti
Nessun complemento associato.
- nomi simili, classi diverse: NP contro Σ2P
- CIRC SAT e QSAT2 sono entrambi Σ2P-completi
Teorema (CIRC SAT e CIRC VALIDITY)