000			05462namaa22004211i 4500
003			OSt
005			20250223033237.0
008			240423s2022 |||a|||fr|m|| 000 0 eng d
040			_aEG-GICUC _beng _cEG-GICUC _dEG-GICUC _erda
041	0		_aeng _beng _dara
049			_aDeposit
082	0	4	_a511.3
092			_a511.3 _221
097			_aPh.D
099			_aCai01.12.17.Ph.D.2022.Mo.F
100	0		_aMohamed Hesham Mohamed Emam El Halaby, _epreparation.
245	1	0	_aFuzzy Satisfiability Problems and Applications / _cPresented by Mohamed Hesham Mohamed Emam El Halaby ; Supervisors Prof. Dr. Laila Abd Elal, Dr. Areeg Abdalla
246	1	5	_aمسائل التحقق في المنطق الضبابي وتطبيقاتهم /
264		0	_c2022.
300			_a102 pages : _billustrations ; _c25 cm. + _eCD.
336			_atext _2rda content
337			_aUnmediated _2rdamedia
338			_avolume _2rdacarrier
502			_aThesis (Ph.D)-Cairo University, 2022.
504			_aBibliography: pages 86-102.
520			_aThe Satisfiability problem (SAT) is deciding whether the given CNF formula has a satisfying assignment or not. SAT is one of the most studied problems in computer science for its importance from both a theoretical and practical perspectives. The Maximum Satisfiability problem (MaxSAT) is finding an assignment that maximizes the number of satisfied clauses in the given CNF formula. Both SAT and MaxSAT have received less attention in non-classical logics, such as fuzzy logics and the objective of this thesis is to fill in the gap. The major contributions of this thesis are as follows. Firstly, we show that MaxSAT is N P-complete for Ł-clausal forms. Secondly, we provide an instance generation model that is used to produce Ł-clausal forms with different values of k and degree of absence of negated terms ¬(l1 ⊕ · · · ⊕ lm) in each clause. Thirdly, we conduct an empirical investigation to identify the relationship between the cost and other parameters of the instance generator. Using our generation model, we can construct instances with different costs but having the same clauses-to-variables ratio. Fourthly, we investigate the prediction the satisfiability of Ł-clausal forms by training different classifiers (Neural Network, Linear SVC, Logistic Regression, Random Forest and Decision Tree). We used our instance generator to construct 3-valued and 7-valued Ł-clausal forms in the phase transition area from which we extract numeric and graph features. Using a neural network classifier, we obtained a mean cross- validation score of 95.2%. Finally, we present a new application to SAT that involves encoding the k-coloring problem as a propositional formula in Łukasiewicz logic with k truth values then solving its satisfiability with SMT technology. The new encoding is more intuitive and compact than its basic counterpart in Boolean logic. Through experimental results, we show that our new technique is superior than its Boolean counterpart in performance specially on unsatisfiable instances
520			_aمسألة التحقق (SAT) هي تقرير ما اذا كان يوجد حل يحقق الصيغة البوليانية المعطاه. هذه المسألة هي واحدة من أكثر المسائل محل الدراسة في علوم الحاسب نظرا لأهميتها من الناحية النظرية و العملية. مسألة أقصى تحقق ممكن (MaxSAT) هي إيجاد الحل الذي يحقق أكبر عدد من الجمل المكونة للصيغة المعطاه. لم تلقى كلاً من SAT و MaxSAT اهتماماً كافياً في المنطق الضبابي. الهدف من هذه الأطروحة هو مناقشة SAT و MaxSAT في المنطق الضبابي، وعلى وجه الخصوص، الصيغ الإقتراحية في منطق Łukasiewicz. وتقدم الرسالة اثبات أن التعقيد الحسابي لـ MaxSAT من نوع NP-complete. ثم نقدم نموذج مولد الصيغ يُستخدم لإنتاج الصيغ الاقتراحية لأشكال Ł-clausal بقيم مختلفة لـ k ودرجة غياب المصطلحات (الاطراف) المنفية (l1⊕•••⊕ lm)¬ في كل جملة. ايضاً نقوم بدراسة تجريبيه للعلاقة بين معامل التكلفة و المعاملات الأخرى لمولد الصيغ. ثم ندرس ملاءمة أشكال Ł-clausal من خلال تدريب نماذح مختلفة لتعليم الاله وحصلنا على متوسط درجة تحقق متقاطع 95.2٪ وأخيراً، نقدم تطبيقاً جديدًا لـ SAT و الذى يتضمن ترميز مسألة k-coloring كصيغة مقترحة في منطق Łukasiewicz لـ k قيمة ثم تقديم حل أكثر سهولة وصغراً من نظيره الأساسي في المنطق البوليانى.
530			_aIssued also as CD
546			_aText in English and abstract in Arabic & English.
650		7	_aMathematics _2qrmark
653		0	_aSAT _aŁ-clausal forms _aŁukasiewicz logic _aMaxSAT _aMachine learning
700	0		_aLaila Abd Elal _ethesis advisor.
700	0		_aAreeg Abdalla _ethesis advisor.
900			_b01-01-2022 _cLaila Abd Elal _cAreeg Abdalla _UCairo University _FFaculty of Science _DDepartment of Mathematics
905			_aEman _eHuda
942			_2ddc _cTH _e21 _n0
999			_c166784