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...
| প্রধান লেখক: | , , |
|---|---|
| অন্যান্য লেখক: | |
| বিন্যাস: | Conference item |
| প্রকাশিত: |
ACM
2013
|