Conflict Driven Clause Belajar menelusuri kembali klarifikasi

Pada halaman wikipedia di sini dijelaskan dengan sangat baik algoritma CDCL (dan tampaknya gambar diambil dari slide yang dibuat oleh Sharad Malik di Princeton). Namun ketika menggambarkan bagaimana untuk mundur semua yang dikatakannya adalah "ke titik yang tepat". MiniSAT juga menggunakan varian dari algoritma CDCL jadi saya membaca makalah ini. Apa yang mereka katakan adalah bahwa Anda harus mundur sampai klausa yang dipelajari adalah klausa unit. Itu jelas klarifikasi tetapi tidak masuk akal bagi saya. Tugas terakhir pasti akan menjadi bagian dari klausa konflik yang dipelajari sejauh yang saya tahu (mungkin saya salah di sini?) Jadi ketika Anda mundur satu langkah Anda akan segera membuat unit klausa yang dipelajari, nilai yang ditugaskan terakhir akan terbalik, dan algoritme akan berjalan persis seperti DPLL tanpa pernah mundur jauh. Selain itu halaman wikipedia tidak mengikuti aturan ini, ia mundur lebih jauh seperti yang diinginkan.

Seberapa jauh seseorang harus mundur?

Inilah paragraf yang relevan dari makalah MiniSAT:

$False$

Poin yang sepertinya Anda lewatkan adalah bahwa begitu klausa yang dipelajari menjadi unit karena penugasan dibatalkan (mundur), pemecah masalah tidak berhenti di situ. Mungkin ada tugas lain sebelum ini yang tidak ada hubungannya dengan konflik saat ini dan secara eksperimental telah ditunjukkan bahwa lebih baik untuk membatalkan tugas yang tidak berhubungan ini juga. Jadi pemecah terus membatalkan tugas sampai membatalkan berikutnya akan membuat klausa yang dipelajari non-unit, yaitu itu akan berisi lebih dari satu variabel yang belum ditetapkan. Solver berhenti di sini, menjalankan propagasi unit untuk memenuhi klausa unit dan kemudian melanjutkan pencarian, menugaskan variabel secara normal.

Perhatikan juga bahwa variabel keputusan saat ini mungkin tidak ada dalam klausa yang dipelajari. Strategi umum untuk pemecah CDCL adalah menemukan titik implikasi unik pertama dan menggunakan variabel itu dalam klausa yang dipelajari. Dalam beberapa kasus, UIP pertama adalah variabel keputusan, tetapi seringkali tidak.