Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

If I understand correctly what "conflicting" means, that process can't possibly result in an empty clause, as in Resolution refutation proofs, correct?

What would be the gold standard reference for CDCL? Something that would be taught at an undergraduate class, say?

Edit: after reading a bit on the net it seems like clause learning in CDCL is basically Resolution-derivation by input Resolution. Cool beans.



Consider applying for YC's Fall 2026 batch! Applications are open till July 27.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: