ນີ້ແມ່ນຄໍາສັ່ງ anldp ທີ່ສາມາດດໍາເນີນການໄດ້ໃນ OnWorks ຜູ້ໃຫ້ບໍລິການໂຮດຕິ້ງຟຣີໂດຍໃຊ້ຫນຶ່ງໃນຫຼາຍໆບ່ອນເຮັດວຽກອອນໄລນ໌ຂອງພວກເຮົາເຊັ່ນ Ubuntu Online, Fedora Online, Windows online emulator ຫຼື MAC OS online emulator
ໂຄງການ:
NAME
anldp - ການປະຕິບັດຂັ້ນຕອນຄວາມພໍໃຈຂອງຂໍ້ສະເຫນີ Davis-Putnam
ສະຫຼຸບສັງລວມ
andldp [ທາງເລືອກໃນການ] ໄຟລ໌ປ້ອນຂໍ້ມູນ > output-file
ລາຍລະອຽດ
ຫນ້າຄູ່ມືນີ້ເອກະສານສັ້ນໆກ່ຽວກັບ andldp ຄໍາສັ່ງ.
andldp ແມ່ນການປະຕິບັດຂັ້ນຕອນການ Davis - Putnam ສໍາລັບການສະເຫນີ
ບັນຫາຄວາມພໍໃຈ. andldp exposes ຂັ້ນຕອນການນໍາໃຊ້ໂດຍ ມ້າມ2(1) ກໍານົດ
ຄວາມພໍໃຈ. andldp ຍັງສາມາດໃຊ້ເວລາຄໍາຖະແຫຼງການໃນລໍາດັບທໍາອິດທີ່ມີຄວາມສະເຫມີພາບແລະ a
ຂະຫນາດໂດເມນ n ຫຼັງຈາກນັ້ນຄົ້ນຫາສໍາລັບຕົວແບບຂະຫນາດ n. ລະຫັດການຊອກຫາແບບຈໍາລອງແບບລໍາດັບທໍາອິດ
ປ່ຽນຄຳຖະແຫຼງດັ່ງກ່າວເປັນຊຸດຂອງຂໍ້ສະ ເໜີ ເຊັ່ນວ່າ ລຳດັບທຳອິດ
ຖະແຫຼງການມີຮູບແບບຂອງຂະຫນາດ n if and only if the proposal clauses ແມ່ນ
ພໍໃຈ. ຫຼັງຈາກນັ້ນ, ຊຸດການສະເຫນີແມ່ນໄດ້ຖືກມອບໃຫ້ລະຫັດ Davis-Putnam; ໃດ
ຮູບແບບການສະເໜີທີ່ພົບເຫັນສາມາດແປເປັນແບບຈໍາລອງຂອງຄໍາສັ່ງທໍາອິດ
ຖະແຫຼງການ. ໂຄງການຄົ້ນຫາແບບຈໍາລອງຄໍາສັ່ງທໍາອິດຍອມຮັບຄໍາຖະແຫຼງການພຽງແຕ່ໃນແບບແປ
ຮູບແບບຂໍ້ຄວາມກ່ຽວຂ້ອງໂດຍບໍ່ມີສັນຍາລັກຫນ້າທີ່.
OPTIONS
-s ປະຕິບັດການຍ່ອຍ. (ການຍ່ອຍສະຫຼາຍຈະຖືກປະຕິບັດສະເໝີໃນລະຫວ່າງການປະມວນຜົນໜ່ວຍກ່ອນ.)
-p ພິມແບບຈໍາລອງຕາມທີ່ເຂົາເຈົ້າພົບເຫັນ.
-m n ຢຸດເຊົາໃນເວລາທີ່ nຮູບແບບທີຖືກພົບເຫັນ.
-t n ຢຸດຫຼັງຈາກ n ວິນາທີ.
-k n ຈັດສັນຫຼາຍທີ່ສຸດ n kbytes ສໍາລັບການເກັບຮັກສາຂອງຂໍ້.
-x n ການທົດລອງກຸ່ມ n.
-B ເອກະສານ
ການມອບໝາຍສຳຮອງໃສ່ໄຟລ໌.
-b n Backup ການມອບຫມາຍທຸກໆ n ວິນາທີ.
-R ເອກະສານ
ກູ້ຄືນການມອບໝາຍຈາກໄຟລ໌. ໂດຍທົ່ວໄປແລ້ວໄຟລ໌ດັ່ງກ່າວມີພຽງແຖວສຸດທ້າຍຂອງ
ໄຟລ໌າຮອງ. ການປ້ອນຂໍ້ມູນອື່ນໆ, ໂດຍສະເພາະປະໂຫຍກ, ຕ້ອງໄດ້ຮັບການໃຫ້ແນ່ນອນຄືກັບໃນ
ການຄົ້ນຫາຕົ້ນສະບັບ.
-n n ຕົວເລືອກນີ້ຖືກນໍາໃຊ້ສໍາລັບການຄົ້ນຫາແບບຈໍາລອງຄໍາສັ່ງທໍາອິດ. ພາລາມິເຕີ n ລະບຸ
ຂະຫນາດໂດເມນ, ແລະການປະກົດຕົວຂອງມັນບອກໃຫ້ໂຄງການອ່ານຄໍາສັ່ງທໍາອິດແປ
ຂໍ້ຄວາມກ່ຽວຂ້ອງກັບການປ້ອນຂໍ້ມູນແທນທີ່ຈະເປັນ propositional clauses.
ໃຊ້ anldp ອອນໄລນ໌ໂດຍໃຊ້ບໍລິການ onworks.net
