Thesis (Ph.D)-Cairo University, 2022.

Bibliography: pages 86-102.

The 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

مسألة التحقق (SAT) هي تقرير ما اذا كان يوجد حل يحقق الصيغة البوليانية المعطاه. هذه المسألة هي واحدة من أكثر المسائل محل الدراسة في علوم الحاسب نظرا لأهميتها من الناحية النظرية و العملية. مسألة أقصى تحقق ممكن (MaxSAT) هي إيجاد الحل الذي يحقق أكبر عدد من الجمل المكونة للصيغة المعطاه. لم تلقى كلاً من SAT و MaxSAT اهتماماً كافياً في المنطق الضبابي. الهدف من هذه الأطروحة هو مناقشة SAT و MaxSAT في المنطق الضبابي، وعلى وجه الخصوص، الصيغ الإقتراحية في منطق Łukasiewicz. وتقدم الرسالة اثبات أن التعقيد الحسابي لـ MaxSAT من نوع NP-complete. ثم نقدم نموذج مولد الصيغ يُستخدم لإنتاج الصيغ الاقتراحية لأشكال Ł-clausal بقيم مختلفة لـ k ودرجة غياب المصطلحات (الاطراف) المنفية (l1⊕•••⊕ lm)¬ في كل جملة. ايضاً نقوم بدراسة تجريبيه للعلاقة بين معامل التكلفة و المعاملات الأخرى لمولد الصيغ. ثم ندرس ملاءمة أشكال Ł-clausal من خلال تدريب نماذح مختلفة لتعليم الاله وحصلنا على متوسط درجة تحقق متقاطع 95.2٪ وأخيراً، نقدم تطبيقاً جديدًا لـ SAT و الذى يتضمن ترميز مسألة k-coloring كصيغة مقترحة في منطق Łukasiewicz لـ k قيمة ثم تقديم حل أكثر سهولة وصغراً من نظيره الأساسي في المنطق البوليانى.

Issued also as CD

Text in English and abstract in Arabic & English.