Risoluzione SAT con più di 2^32 clausole

Question

Sto cercando di risolvere una grande formula CNF utilizzando un SAT solver. La formula (in formato DIMACS) ha 4,697,898,048 = 2^32 + 402,930,752 clausole, e tutti i solutori SAT che ho trovato sono problemi con esso:

• (P)lingeling rapporti che ci sono "troppe clausole" (vale a dire più clausole che la riga di intestazione specifica, ma questo non è il caso)
• CryptoMiniSat4 & picosat pretesa di leggere la riga di intestazione come dicendo 402,930,752 clausole che sono 2^32 troppo pochi
• Glucose sembra analizzare 98,916,961 clausole e poi reports to have solved the formula as UNSAT utilizzando semplificazione, ma t il suo è improbabile che sia corretto (un segmento iniziale della formula questo breve è molto probabile che sia SAT).

Qualcuno è a conoscenza di un solutore SAT in grado di gestire file così grandi? O c'è qualcosa come un interruttore del compilatore che può aggirare questo tipo di comportamento? Credo che tutti i solutori siano compilati per 64bit linux. (Sono un po 'un noob quando si tratta di gestire numeri così grandi, mi dispiace.)

Answer 1

Sono lo sviluppatore di CryptoMiniSat. Nella maggior parte dei casi in cui il CNF è così grande, il problema non è il solutore SAT, ma la traduzione del problema originale in CNF non è stata eseguita con sufficiente attenzione. Presumo che tu non abbia scritto questo CNF a mano - hai avuto un problema che hai tradotto in CNF usando uno strumento automatico.

L'atto di tradurre un problema in CNF è chiamato codifica e ha un'enorme letteratura nel mondo accademico. È un argomento intero per se stesso, o più appropriatamente, interi argomenti a se stessi. Si prega di consultare i documenti di ricerca su Constraint Programming (CP), Pseudo-boolean constraints (PB), tecniche di traduzione ANF-a-CNF (vedi workshop/conferenze di cripto) e codifica dei circuiti elettronici (ricerca di AIG, codifica di Tseitin e sue varianti e aspetto ai riferimenti). Questi sono i grandi argomenti, ma ce ne sono molti altri. Dare una sbirciatina a questi ridurrà il tuo CNF di almeno 3 ordini di grandezza, probabilmente di più.