SAT
Un problema SAT è costituito da un insieme di clausole booleane.
Ciascuna clausola è l'OR di un insieme di letterali.
Ogni letterale può essere un atomo o un atomo negato.
Ad esempio, il seguente è un problema SAT:
- X1 \/ not(X2) \/ not(X3)
- not(X1) \/ X2 \/ not(X3)
Una soluzione è un assegnamento alle variabili per cui tutte le clausole sono soddisfatte (tutti gli OR sono veri), ad es X1=1, X2=1, X3=0.
Di solito i problemi SAT vengono dati in formato CNF DIMACS.
Per leggere il formato DIMACS, si può usare il predicato read_cnf(NomeFile) dal file read_cnf.ecl
read_cnf(NomeFile) salva l'istanza con un insieme di fatti. Il nome del file può essere dato come stringa (fra doppie virgolette) o come atomo (fra apici singoli).
È presente un fatto cnf(NumeroVariabili,NumeroClausole) e poi un insieme di NumeroClausole fatti clausola(Lista) che rappresentano le varie clausole.
Ciascuna clausola è rappresentata con una lista di numeri interi. Un valore positivo i rappresenta l'i-esima variabile, mentre un valore negativo rappresenta l'i-esima variabile negata.
Il problema sopra è quindi rappresentato come:
cnf(3,2).
clausola([1,-2,-3]).
clausola([-1,2,-3]).Si scriva un programma ECLiPSe che risolve un problema SAT. Lo si provi poi con queste istanze:
Altre istanze si possono trovare su
