Маалыматтарды бийлеген жана татаал маселелерди тез чечкен алгоритм

Шилтемелер таблицасы

1 Киришүү

2 Dancing Links

3 Rust программалоо тили

4 RAC: Аппараттык камсыздоо/Программалык камсыздоо масштабда биргелешип кепилдик берүү

5 Rust жана RAR

5.1 Чектелген Алгоритмдик Rust

6 Rust менен бийлеген шилтемелер жана 6.1 аныктамалар

6.2 ACL2ге которуу

6.3 Бийлик шилтемелер теоремасы

7 Байланыштуу иштер

8 Корутунду

9 Ыраазычылык жана Шилтемелер

"Бийлөөчү шилтемелер" тизменин элементтерин тез алып салуу жана калыбына келтирүүнү камсыз кылган тегерек эки эселенген тизмек маалымат структурасын ишке ашырууга оптималдаштырууну билдирет. Dancing Links оптималдаштыруу биринчи кезекте так капкактарды табуу үчүн тез алгоритмдерде колдонулат жана Кнут тарабынан өзүнүн "Компьютердик программалоо искусствосу" сериясынын 4В томунда кеңири жайылтылган. Биз Rust программалоо тилинде Dancing Links оптималдаштыруунун ишке ашырылышын, ошондой эле ACL2 теоремасы проверинин жардамы менен аны расмий текшерүүнү сүрөттөйбүз. Rust акыркы бир нече жылда Amazon, Google жана Microsoft сыяктуу компанияларда C/C++ үчүн заманбап, эстутум боюнча коопсуз мураскер катары олуттуу жактырууга ээ болду жана Linux жана Windows операциялык тутумунун өзөктөрүнө интеграцияланууда. Rust программасына болгон кызыгуубуз анын аппараттык/программалык камсыздоо тили катары, критикалык системаларга колдонуу мүмкүнчүлүгүнөн келип чыгат. Биз Russinoffтун Чектелген алгоритмдик C (RAC) шыктандыруусу менен Rust чакан топтомун жасадык, аны биз кыялдануу менен Чектелген Алгоритмдик Rust же RAR деп атадык. Мурунку жумушта биз RAR инструменталдык чынжырын алгачкы ишке ашыруубузду сүрөттөгөнбүз, мында биз жөн гана RAR булагын RACга көчүрөбүз. Муну менен биз убакытты жана күчтү минималдуу инвестициялоо менен бир катар учурдагы аппараттык/программалык камсыздоо куралдарын колдонобуз. Бул макалада биз RAR Rust чакан топтомун сүрөттөп, жакшыртылган RAR инструменталдык чынжырыбызды сүрөттөп беребиз жана RARдагы Dancing Links оптималдаштырууну колдонгон тегерек кош байланыштуу тизме түзүмүн долбоорлоону жана текшерүүнү майда-чүйдөсүнө чейин келтиребиз. ACL2 теоремасы провер.

1 Киришүү

Так жабуу маселеси [17], эң жөнөкөй түрдө, экилик элементтери бар n × m матрица үчүн бардык мамычанын суммалары так бир болгон матрицанын саптарынын бардык бөлүмчөлөрүн табууга аракет кылат. Бул негизги түшүнүк табигый түрдө кандайдыр бир сандык диапазондо турган матрицалык элементтерге жайылтылат; Чынында эле, Судоку популярдуу баш катырма оюну 1ден 9га чейинки диапазондогу элементтин маанилери менен 9×9 матрицасы үчүн кеңейтилген так жабуу маселеси.

Так капкак маселеси NP-толук, бирок компьютер илимпоздору так капкактарды табуу үчүн рекурсивдүү, детерминисттик эмес артка кайтуу алгоритмдерин ойлоп табышты. Мындай процедуралардын бири [17] сүрөттөлгөн Knuth's Algorithm X болуп саналат. Бул алгоритмде матрицанын элементтери эки эселенген тегерек тизмелер аркылуу туташтырылат, ал эми айрым элементтер алгоритмдин жүрүшүнө жараша, артка кайтууга дуушар болуп, ж.б.у.с. өчүрүлөт же калыбына келтирилет. Анткени бул алып салуулар жана тизмеден/тизмеден калыбына келтирүү кеңири таралган. , бул операцияларды натыйжалуу кылуу мактоого татырлык максат болуп саналат. Бул жерде Knuth's "Bicing Links" пайда болот, натыйжада Knuth DLX деп атаган так капкактарды табуу үчүн оптималдаштырылган алгоритм пайда болот (X алгоритмине колдонулган бийлөө шилтемелери).

2 бий шилтемелери

Dancing Links концепциясы абдан жөнөкөй: тизменин берилген Y элементи так мукаба алгоритминде алынып салынганда, ошол эле элемент кийинчерээк калыбына келтирилет. Ошентип, тескерисинче

Y элементи менен байланышкан "мурунку" жана "кийинки" шилтемелерди "нөлгө чыгарууга" караганда, программалоонун жакшы гигиенасы адатта талап кылгандай, Dancing Links программасында программист өчүрүлгөн элемент үчүн шилтеме маанилерин калтырат. Бийлеген шилтемелер оператору ошентип, Y элементин тизмеден өчүрөт, мурунку X элементинин "кийинки" элементин кийинки Z элементине жана Z'дин "мурунку" элементин X менен байланыштырат, бирок 'ге тийбейт. Алынып салынган Y элементинин кийинки' жана 'мурунку' шилтемелери. Кийинчерээк, Y калыбына келтирилиши керек болсо, ал жөнөкөй калыбына келтирүү операторунун жардамы менен тизмеге кайра кошулат. Кнуттун сөзү менен айтканда, эгер кимдир бирөө DLX алгоритминин жүрүшү менен тизмедеги шилтемелерди көзөмөлдөп турса, шилтемелер "бийлеп" көрүнөт, демек, аты. Knuth's Dancing Links функционалдуулугу 1-сүрөттө кыскача келтирилген.