Come un risolutore SMT / SAT genera valutazioni per questo esempio

Question

Innanzitutto, un esempio di una serie di vincoli che si sono rivelati non essere risolvibili (non credo):

b < 3 && c + a > 5 && a - b > 2 && c > 1 && b - c > 3

La mia procedura per risolvere questo è all'incirca: ok b è inferiore a 3 e c> 1. 1 + a> 5, quindi a> 4 in quel caso. Prova 4 - 2> 2, no che non funziona, quindi forse a è 5, 5 - 2> 2. quindi b - c> 3. 2 - 2> 3. no, quindi b deve b maggiore di 3, ma Sappiamo che B è inferiore a 3, quindi non può essere risolto.

Quindi un esempio più semplice che può essere risolto.

b < 3 && c + a > 5 && a - b > 2

Quindi dire B è 2. Quindi a - 2> 2, quindi dire a è 5. Quindi C + 5> 5, quindi dire che C è anche 1. Quindi a = 5, b = 2, c = 1 risolve il problema.

In questo esempio, ho scelto numeri che erano vicino al confine, in quanto erano "appena sopra" il limite inferiore nella parte>. Ma si potrebbe dire che A è 100 e C è 100. Questo è anche un esempio particolarmente semplice.

La mia domanda è: come un solutore di vincoli risolve questo problema. Ho letto di SAT e SMT e devo ancora leggere il libro sulle procedure decisionali. Tuttavia, capisco che i risolutori SAT risolvono i sistemi di equazioni booleane in due modi: (1) restituendo sì/no che il sistema può essere risolto o (2) assegnando valutazioni a ciascuna variabile nel sistema in modo che soddisfi i vincoli. Non so come lo facciano però. Capisco anche che i solutori SMT sono fondamentalmente uno strato leggero sopra i solutori SAT. Ti permettono di avere formule booleane più ricche usando diverse "teorie" (come la teoria dell'uguaglianza, la teoria dei reali, gli interi, le liste, ecc.). Quindi è possibile definire facoltativamente come unire queste teorie in modo da poter applicare il solutore SAT su un'espressione complicata che coinvolge, ad esempio i reali, i numeri interi, l'uguaglianza, i booleani ed elenchi o array tutti in una volta. Per me questo sembra ovvio, perché il solutore di vincoli non dovrebbe funzionare su funzioni e variabili arbitrarie, ma probabilmente mi manca qualcosa.

Vorrei sapere come implementare qualcosa di simile Z3. Presumo che ogni teoria specifica (come il teoria delle corde) è piuttosto complicato, quindi non volevo chiedere come risolvere genericamente tutti i diversi tipi di vincoli. Invece volevo porre una domanda semplificata usando vincoli interi di base in modo da poter imparare i fondamenti di come funziona un risolutore SMT / SAT.

In quanto tale, la domanda è fondamentalmente proprio, come un solutore di vincoli risolve il secondo esempio sopra. Uno o due degli algoritmi che potrebbe usare per farlo. In particolare, vorrei sapere come dare a qualche funzione un insieme di vincoli e farmi restituire valutazioni per tutte le variabili. A tale proposito, la domanda prevede anche come il risolutore di vincoli scelga o decida sull'insieme dei valori. Ho visto che diceva che è casuale, ma vorrei evitare quell'approccio se possibile. Ma in entrambi i casi, quando sceglie un valore, chiedendosi come sa che ne abbia ottenuto uno valido. Se deve ricompensare tutti i vincoli ogni volta che fa un'ipotesi o può fare una sorta di ottimizzazione. Fondamentalmente, proprio come funziona il risolutore SAT / SMT.

Per mantenerlo semplice, non sto cercando una spiegazione completa di come funzionano tutti gli aspetti della risoluzione del problema. Solo più un'introduzione di alto livello agli algoritmi e su come selezionano i valori e restituiscono la valutazione. Una volta capito che allora immagino che capire le teorie più complicate come la teoria delle stringhe avranno più senso.

Lo chiedo perché non posso dirlo in base alla mia lettura finora se tutto si riduce davvero per applicare vincoli in un risolutore SAT, e forse ci sono algoritmi di risoluzione di 1 o 2 SAT (DPLL e CDCL con cui sto acquisendo familiarità) Per vincoli booleani (più forse qualche altro per generare i dati di test per risolvere i vincoli). O mi sbaglio lì, e c'è un intero livello di ricerca al di là di questo (sui risolutori SMT) in cui le procedure di decisione personalizzate sono gli algoritmi che si desidera utilizzare, e ce ne sono centinaia e non esiste un modello standard. In tal caso, continuo ad avere difficoltà a imaging come è possibile risolvere un sistema di vincoli come quello sopra, o qualcosa di più complicato con i vincoli di stringa (abbina Regex) e altri vincoli che richiedono funzioni complesse (come qualcosa è la versione inversa o ordinata qualcos'altro). Se c'è tanta variabilità, allora l'idea di risolvere eventuali vincoli sembra difficile.

Fondamentalmente quello che sto cercando è una descrizione di un implementazione. Finora ho letto molti documenti, ma sono stati per lo più di livello troppo alto per applicarlo.