Limiti di risolutori SMT

Question

Tradizionalmente la maggior parte del lavoro con la logica computazionale era proposizionale, nel qual caso si utilizzava un solutore SAT (soddisfacibilità booleana) o di primo ordine, nel qual caso si utilizzava un rilevatore del teorema del primo ordine.

Negli ultimi anni, sono stati fatti molti progressi sui solutori SMT (teoria modulo soddisfacente), che fondamentalmente aumentano la logica proposizionale con le teorie dell'aritmetica ecc .; John Rushby di SRI International arriva addirittura a definirli una tecnologia dirompente.

Quali sono gli esempi pratici più importanti di problemi che possono essere gestiti nella logica del primo ordine ma che non possono ancora essere gestiti da SMT? In particolare, quali sono i problemi che non possono essere gestiti da SMT nell'ambito della verifica del software?

Answer 1

I risolutori SMT non sono più potenti dei solutori SAT. Funzioneranno ancora in tempo esponenziale o saranno incompleti per gli stessi problemi in SAT. Il vantaggio di SMT è che molte cose che sono ovvie in SMT possono richiedere molto tempo prima che un risolutore di satelliti equivalente possa riscoprire.

Quindi, con la verifica del software come esempio, se si utilizza un risolutore SMT QF BV (quantificatore-libera teoria dei bit-bit), il solutore SMT sarà consapevole che (a + b = b + a) su una parola livello invece, mentre può impiegare un risolutore SAT per un tempo veramente lungo per dimostrare che si utilizzano i singoli valori booleani.

Quindi, per la verifica del software, è possibile creare facilmente problemi nella verifica del software che sarebbe difficile per qualsiasi risolutore SMT o SAT.

Per prima cosa, i loop devono essere srotolati in QF BV, il che significa che in pratica è necessario limitare ciò che il risolutore verifica. Se i quantificatori sono stati autorizzati, diventa un problema completo di PSPACE, non solo NP-completo.

In secondo luogo, i problemi che sono considerati difficili in generale sono facili da codificare in QF BV. Ad esempio, è possibile scrivere un programma come segue:

void run(int64_t a,int64_t b) 
{ 
    a * b == <some large semiprime>; 

    assert (false); 
} 

Ora, naturalmente, il risolutore SMT sarà facile dimostrare che assert (false) si verificherà, ma dovrà fornire un controesempio, che vi darà la ingressi a,b. Se imposti <some large number> in un semiprime RSA, hai appena invertito la moltiplicazione ... altrimenti noto come fattorizzazione di interi! Quindi questo sarà probabilmente difficile per qualsiasi solutore SMT e dimostrerà che la verifica del software è un problema difficile in generale (a meno che P = NP, o almeno la fattorizzazione di interi sia facile). Tali solutori SMT sono solo un vantaggio per i solutori del SAT, vestendo le cose in un linguaggio più facile da scrivere e più facile da ragionare.

I risolutori SMT che risolvono teorie più avanzate sono necessariamente incompleti o sono ancora più lenti dei solutori SAT, perché stanno tentando di risolvere i problemi più difficili.

Consulta anche:

• interessante notare che il Beaver SMT solver traduce QF BV al CNF e possono utilizzare un solutore SAT come back-end.
• Klee che può richiedere un programma compilato a LLVM IR (rappresentazione intermedia), controlla i bachi e trova esempi di controprestazioni alle asserzioni ecc. Se trova un bug, può dare un controesempio alla correttezza (verrà darti un input che riprodurrà il bug).