Creating industrial-like SAT instances by clustering and reconstruction (Poster presentation)

Abstract

For the optimization of SAT solvers, it is crucial that a solver can be trained on a preferably large number of instances for general or domain specific problems. Especially for domain specific problems the set of available instances can be insufficiently small. In our approach we built large sets of instances by recombining several small snippets of different instances of a particular domain. Also the fuzzer utility [3] builds industrial-like SAT instances by combining smaller pieces. However, these pieces are a combination of randomly created circuits and are not derived from an existing pool of instances. In Ansotegui [1] random pseudo-industrial instances are created in a more formal way. © 2012 Springer-Verlag.