Satisfiability in big Boolean algebras via Boolean-equation solving
Other Title(s)
دراسة المشبعية في أنواع الجبر البولاني الكبير بواسطة حل المعادلات البولانية
Joint Authors
Ahmad, Walid
Rushdi, Ali Muhammad Ali
Source
Journal of King Abdulaziz University : Engineering Sciences
Issue
Vol. 28, Issue 1 (30 Jun. 2017), pp.3-18, 16 p.
Publisher
King Abdulaziz University Scientific Publishing Center
Publication Date
2017-06-30
Country of Publication
Saudi Arabia
No. of Pages
16
Main Subjects
Abstract EN
This paper studies Satisfiability (SAT) in finite atomic Boolean algebras larger than the two-valued one B2, which are named big Boolean algebras.
Unlike the formula g(X) in the SAT problem over B2, which is either satisfiable or unsatisfiable, this formula for the SAT problem over a big Boolean algebra could be unconditionally satisfiable, conditionally satisfiable, or unsatisfiable depending on the nature of the consistency condition of the Boolean equation {g(X)=1}, since this condition could be an identity, a genuine equation, or a contradiction.
The paper handles this latter SAT problem by using a conventional method and a novel one for deriving parametric general solutions, and subsequently utilizing expansion trees for generating all particular solutions of the aforementioned Boolean equation.
Each of these two methods could be cast in pure algebraic form, but becomes much easier to visualize and comprehend when presented via the natural map of a big Boolean algebra, which (for historical reasons) is called the variable-entered Karnaugh map (VEKM).
In the classical method, the number of parameters used is minimized and compact solutions are obtained.
However, the parameters belong to the underlying big Boolean algebra.
By contrast, the novel method does not attempt to minimize the number of parameters used, as it uses independent parameters belonging to the two-valued Boolean algebra B2 for each asserted atom in the Boole-Shannon expansion of the formula g(X).
Though the method produces non-compact expressions, it is much quicker in generating particular solutions.
The two methods are demonstrated via two detailed examples.
American Psychological Association (APA)
Rushdi, Ali Muhammad Ali& Ahmad, Walid. 2017. Satisfiability in big Boolean algebras via Boolean-equation solving. Journal of King Abdulaziz University : Engineering Sciences،Vol. 28, no. 1, pp.3-18.
https://search.emarefa.net/detail/BIM-926490
Modern Language Association (MLA)
Rushdi, Ali Muhammad Ali& Ahmad, Walid. Satisfiability in big Boolean algebras via Boolean-equation solving. Journal of King Abdulaziz University : Engineering Sciences Vol. 28, no. 1 (2017), pp.3-18.
https://search.emarefa.net/detail/BIM-926490
American Medical Association (AMA)
Rushdi, Ali Muhammad Ali& Ahmad, Walid. Satisfiability in big Boolean algebras via Boolean-equation solving. Journal of King Abdulaziz University : Engineering Sciences. 2017. Vol. 28, no. 1, pp.3-18.
https://search.emarefa.net/detail/BIM-926490
Data Type
Journal Articles
Language
English
Notes
Includes bibliographical references : p. 17
Record ID
BIM-926490