Come creare un algoritmo per determinare le Tautologie Booleane

3

Quindi ora sto esplorando alcuni argomenti in un corso di prova e mi è venuto in mente di provare a creare un risolutore di tautologia booleana. Vorrei un algoritmo più efficiente della forza bruta.

Dichiarazione di problemi:

data una stringa di '(', ')', '[e]', '[o]',! e parti di testo che denotano nomi di variabili (che per definizione non possono includere marchi parentesi segni di parentesi o contrassegni!) che devono essere circondati da una coppia di parentesi

Anche le parole "VERO" e "FALSO" sono riservate

determina se la stringa booleana è ben formata e, in tal caso, è una tautologia

ex: (alpha)[and](beta)

è ben formato e non una tautologia perché se: alpha = false e beta = true è un esempio di contatore

ex: (alpha)[or]!(alpha) è ben formato e una tautologia perché ((X)[or]!(X)) è per definizione una tautologia

ex: ((alpha)[or]((beta)[or]!(beta))) è ben formato poiché (beta)[or]!(beta) è true e ((alpha)[or](TRUE)) è sempre true

ex: ((alpha[and](beta)) non è ben formato

Alcune idee che avevo per questo consistevano nel formare un albero genealogico. Poiché ogni istruzione sarà incapsulata da parentesi prima che possa essere applicata a un operatore [o], [e] o [!], Ciò che posso fare è dividere la stringa nei suoi blocchi di livello più alto racchiusi tra parentesi (clausola 1) (clausola 2 ) per generare 2 nodi di un albero che punta al nodo di livello superiore

Ogni nodo contiene informazioni sul fatto che abbia un! collegato al suo fronte, e se ha nodi sotto, quale operatore è usato per unificare questi due nodi

Questo albero può essere generato rapidamente per ridurre l'enunciazione ai singoli letterali e verificare facilmente se l'istruzione è ben strutturata (ci sono un numero uguale di (as) e ogni [o] e [e] hanno due dichiarazioni che circondano e una coppia di parentesi incapsulanti attorno a queste due affermazioni.

Ora il mio piano consisteva nel sottoporre a scansione sistematica i nodi che hanno un valore (!) e che non distribuiscono le leggi di DeMorgan. Se sono costretto a fare qualcosa sulla falsariga (xe! X), ho immediatamente trovato una contraddizione e posso abortire.

Non sono ancora perfettamente chiaro cosa deve accadere in questa fase, tuttavia

    
posta frogeyedpeas 22.07.2014 - 06:05
fonte

1 risposta

7

Il problema di rilevare una tautologia equivale al problema alla soddisfazione booleana che purtroppo np-complete per istanze generali. Puoi convertire facilmente il rilevamento tautologia in SAT con annullando l'equazione booleana e verificarne la soddisfacibilità, se l'equazione negata è insoddisfacente , quindi l'equazione originale deve essere una tautologia .

Che cosa puoi fare: -

  1. Use lex & yacc parser tools to generate a grammer to parse a equation.
  2. Evaluate the negation of the equation using de-morgan's law.
  3. Give the negated eqaution to a standard SAT solvers.

Nota: se la tua equazione è riducibile a 2-SAT allora c'è algoritmo di tempo lineare.

    
risposta data 22.07.2014 - 06:41
fonte

Leggi altre domande sui tag