Abstract conflict driven learning.

Modern satisfiability solvers implement an algorithm, called Conflict Driven Clause Learning, which combines search for a model with analysis of conflicts. We show that this algorithm can be generalised to solve the lattice-theoretic problem of determining if an additive transformer on a Boolean lat...

Cur síos iomlán

Sonraí bibleagrafaíochta
Príomhchruthaitheoirí: D'Silva, V, Haller, L, Kroening, D
Rannpháirtithe: Giacobazzi, R
Formáid: Conference item
Foilsithe / Cruthaithe: ACM 2013