Abstrakt. I detta dokument föreslår vi en ny dynamisk förvaltningspolitik för databasen "inlärda klausuler" i moderna SAT-lösare. Den bygger på en dynamisk frysnings- och aktiveringsprincip för de inlärda klausulerna. Vid en given sökstat, med hjälp av en relevant urvalsfunktion, aktiverar den de mest lovande inlärda klausulerna samtidigt som de fryser irrelevanta. På så sätt kan klausuler som man lärt sig i tidigare steg frysas i det aktuella steget och aktiveras igen i framtida steg i sökprocessen. Vår strategi försöker utnyttja delar av information som samlats in från det förflutna för att härleda relevansen av en viss klausul för de återstående sökstegen. Denna politik står i kontrast till alla välkända raderingsstrategier, där en viss inlärd klausul definitivt elimineras. Experiment på SAT-fall tagna från de senaste tävlingarna visar effektiviteten i vår föreslagna teknik.
En annan dynamisk förvaltningspolitik i databasen över inlärda klausuler föreslås i REF.
On freezing and reactivating learnt clauses
{'venue': 'eds, Lecture Notes in Computer Science', 'journal': None, 'mag_field_of_study': ['Computer Science']}