Boolean satisfiability (SAT) is the problem of determining whether there exists an assignment of the Boolean variables to the truth values such that a given Boolean formula evaluates to true. SAT was the first example of an NP-complete problem. Only two decades ago SAT was mainly considered as of a theoretical interest. Nowadays, the picture is very different. SAT solving becomes mature and is a successful approach for tackling a large number of applications, ranging from artificial intelligence to industrial hardware design and verification. SAT solving consists of encodings and solvers. In order to benefit from the tremendous advances in the development of solvers, one must first encode the original problems into SAT instances. These encodings should not only be easily generated, but should also be efficiently processed by SAT solvers. Furthermore, an increasing number of practical applications in computer science can be expressed as constraint satisfaction problems (CSPs). However, encoding a CSP to SAT is currently regarded as more of an art than a science, and choosing an appropriate encoding is considered as important as choosing an algorithm. Moreover, it is much easier and more efficient to benefit from highly optimized state-of-the-art SAT solvers than to develop specialized tools from scratch. Hence, finding appropriate SAT encodings of CSPs is one of the most fascinating challenges for solving problems by SAT. This thesis studies SAT encodings of CSPs and aims at: 1) conducting a comprehensively profound study of SAT encodings of CSPs by separately investigating encodings of CSP domains and constraints; 2) proposing new SAT encodings of CSP domains; 3) proposing new SAT encoding of the at-most-one constraint, which is essential for encoding CSP variables; 4) introducing the redundant encoding and the hybrid encoding that aim to benefit from both two efficient and common SAT encodings (i.e., the sparse and order encodings) by using the channeling constraint (a term used in Constraint Programming) for SAT; and 5) revealing interesting guidelines on how to choose an appropriate SAT encoding in the way that one can exploit the availability of many efficient SAT solvers to solve CSPs efficiently and effectively. Experiments show that the proposed encodings and guidelines improve the state-of-the-art SAT encodings of CSPs.

Boolean networks are coarse-grained models of the regulatory dynamics that controls the survival and proliferation of a living cell. The dynamics is time- and state-discrete. This Boolean abstraction assumes that small differences in concentration levels are irrelevant; and the binary distinction of a low or a high concentration of each biomolecule is sufficient to capture the dynamics. In this work, we briefly introduce the gene regulatory models, where with the advent of system-specific Boolean models, new conceptual questions and analytical and numerical challenges arise. In particular, the response of the system to external intervention presents a novel area of research. Thus first we investigate how to quantify a node\\\''s individual impact on dynamics in a more detailed manner than an averaging against all eligible perturbations. Since each node now represents a specific biochemical entity, it is the subject of our interest. The prediction of nodes\\\'' dynamical impacts from the model may be compared to the empirical data from biological experiments. Then we develop a hybrid model that incorporates both continuous and discrete random Boolean networks to compare the reaction of the dynamics against small as well as flip perturbations in different regimes. We show that the chaotic behaviour disappears in high sensitive Boolean ensembles with respect to continuous small fluctuations in contrast to the flipping. Finally, we discuss the role of distributing delays in stabilizing of the Boolean dynamics against noise. These studies are expected to trigger additional experiments and lead to improvement of models in gene regulatory dynamics.

Information security in the present era is becoming very important in communication and data storage. Data transferred from one party to another over an insecure channel (e.g., Internet) can be protected by cryptography. The encrypting technologies of traditional and modern cryptography are usually used to avoid the message from being disclosed. Public-key cryptography usually uses complex mathematical computations to scramble the message. / A digital signature is an important public-key primitive that performs the function of conventional handwritten signatures for entity authentication, data integrity, and non-repudiation, especially within the electronic commerce environment. Currently, most conventional digital signature schemes are based on mathematical hard problems. These mathematical algorithms require computers to perform the heavy and complex computations to generate and verify the keys and signatures. In 1995, Naor and Shamir proposed a visual cryptography (VC) for binary images. VC has high security and requires simple computations. The purpose of this thesis is to provide an alternative to the current digital signature technology. We introduce a new digital signature scheme based on the concept of a non-expansion visual cryptography. A visual digital signature scheme is a method to enable visual verification of the authenticity of an image in an insecure environment without the need to perform any complex computations. We proposed scheme generates visual shares and manipulates them using the simple Boolean operations OR rather than generating and computing large and long random integer values as in the conventional digital signature schemes currently in use.

Constraint Satisfaction Problems (CSPs) are NP-complete in general, however, there are many tractable subclasses that rely on the restriction of the structure of their underlying hypergraphs. It is a well-known fact, for instance, that CSPs whose underlying hypergraph is acyclic are tractable. Trying to define “nearly acyclic” hypergraphs led to the definition of various hypergraph decomposition methods. An important member in this class is the hypertree decomposition method, introduced by Gottlob et al. It possesses the property that CSPs falling into this class can be solved efficiently, and that hypergraphs in this class can be recognized efficiently as well. Apart from polynomial tractability, complexity analysis has shown, that both afore-mentioned problems lie in the low complexity class LOGCFL and are thus moreover efficiently parallelizable. A parallel algorithm has been proposed for the “evaluation problem”, however all algorithms for the “recognition problem” presented to date are sequential. The main contribution of this dissertation is the creation of an object oriented programming library including a task scheduler which allows the parallelization of a whole range of computational problems, fulfilling certain complexity-theoretic restrictions. This library merely requires the programmer to provide the implementation of several classes and methods, representing a general alternating algorithm, while the mechanics of the task scheduler remain hidden. In particular, we use this library to create an efficient parallel algorithm, which computes hypertree decompositions of a fixed width. Another result of a more theoretical nature is the definition of a new type of decomposition method, called Balanced Decompositions. Solving CSPs of bounded balanced width and recognizing such hypergraphs is only quasi-polynomial, however still parallelizable to a certain extent. A complexity-theoretic analysis leads to the definition of a new complexity class hierarchy, called the DC-hierarchy, with the first class in this hierarchy, DC1 , precisely capturing the complexity of solving CSPs of bounded balanced width.

This research compares three approaches to land suitability evaluation, Boolean, Fuzzy AHP and Ideal Point, for barley, wheat and maize crops in the north-western region of Jeffara Plain in Libya. A number of soil and landscape criteria were identified to accommodate the three cash crops under irrigation conditions and their weights specified as a result of discussions with local experts. The findings emphasised that soil factors represented the most sensitive criteria affecting all the crops considered. In contrast, erosion and slope were found to be less important in the study area. Using Boolean logic the results indicated only four suitability classes (highly suitable, moderately suitable, marginally suitable and currently not suitable) for all crops. In contrast, the results obtained by adopting the Fuzzy AHP and Ideal Point approaches revealed that the area of study has a greater degree of subdivision in land suitability classes. Overall, the results of the three approaches indicated that the area under consideration has a good potential to produce barley, wheat and maize under irrigation provided that the water and drainage requirements are met. Comparing the three models showed that each suitability class derived from the Boolean approach is associated with low and high values for joint membership functions when derived from Fuzzy AHP and Ideal Point approaches respectively. In other words, the two fuzzy approaches have shown their ability to explore the uncertainties associated with describing the land properties. The richer overall picture provides an alternative type of land suitability evaluation to Boolean approaches and allows subtle variations in land suitability to be explored. The Fuzzy AHP approach was found to be better than the Ideal Point approach; the latter was biased towards positive and negative ideal values. In the future, field trial plots will be needed to evaluate and validate the results further.

First introduced by Forman in 1998, discrete Morse theory has become a standard tool in topological combinatorics. The main idea of discrete Morse theory is to pair cells in a cellular complex in a manner that permits cancellation via elementary collapses, reducing the complex under consideration to a homotopy equivalent complex with fewer cells. In chapter 1, we introduce the relevant background for discrete Morse theory. In chapter 2, we define a discrete Morse matching for a family of independence complexes that generalize the matching complexes of suitable "small" grid graphs. Using this matching, we determine the dimensions of the chain spaces for the resulting Morse complexes and derive bounds on the location of non-trivial homology groups. Furthermore, we determine the Euler characteristic for these complexes and prove that several of their homology groups are non-zero. In chapter 3, we introduce the notion of a homomorphism complex for partially ordered sets, placing particular emphasis on maps between chain posets and the Boolean algebras. We extend the notion of folding from general graph homomorphism complexes to the poset case, and we define an iterative discrete Morse matching for these Boolean complexes. We provide formulas for enumerating the number of critical cells arising from this matching as well as for the Euler characteristic. We end with a conjecture on the optimality of our matching derived from connections to 3-equal manifolds

When we interpret the input vector of a Boolean function as a binary number, we define interval Boolean function fn [a,b] so that fn [a,b](x) = 1 if and only if a ≤ x ≤ b. Disjunctive normal form is a common way of representing Boolean functions. Minimization of DNF representation of an interval Boolean function can be per- formed in linear time. The natural generalization to k-interval functions seems to be significantly harder to tackle. In this thesis, we discuss the difficulties with finding an optimal solution and introduce a 2k-approximation algorithm.

Boolean function f is k-interval if - input vector viewed as n-bit number - f is true for and only for inputs from given (at most) k intervals. Recognition of k-interval fuction given its DNF representation is coNP-hard problem. This thesis shows that for DNFs from a given solvable class (class C of DNFs is solvable if we can for any DNF F ∈ C decide F ≡ 1 in polynomial time and C is closed under partial assignment) and fixed k we can decide whether F represents k-interval function in polynomial time. 1

In the present work we study first-order theories and their Lindenbaum alge- bras by analyzing the properties of the chain BnT n<ω, called B-chain, where BnT is the subalgebra of the Lindenbaum algebra given by formulas with up to n free variables. We enrich the structure of Lindenbaum algebra in order to cap- ture some differences between theories with term-by-term isomorphic B-chains. Several examples of theories and calculations of their B-chains are given. We also construct a model of Robinson arithmetic, whose n-th algebras of definable sets are isomorphic to the Cartesian product of the countable atomic saturated Boolean algebra and the countable atomless Boolean algebra. 1

Functional decomposition aims at finding efficient representations for Boolean functions. It is used in many applications, including multi-level logic synthesis, formal verification, and testing. This dissertation presents novel heuristic algorithms for functional decomposition. These algorithms take advantage of suitable representations of the Boolean functions in order to be efficient. The first two algorithms compute simple-disjoint and disjoint-support decompositions. They are based on representing the target function by a Reduced Ordered Binary Decision Diagram (BDD). Unlike other BDD-based algorithms, the presented ones can deal with larger target functions and produce more decompositions without requiring expensive manipulations of the representation, particularly BDD reordering. The third algorithm also finds disjoint-support decompositions, but it is based on a technique which integrates circuit graph analysis and BDD-based decomposition. The combination of the two approaches results in an algorithm which is more robust than a purely BDD-based one, and that improves both the quality of the results and the running time. The fourth algorithm uses circuit graph analysis to obtain non-disjoint decompositions. We show that the problem of computing non-disjoint decompositions can be reduced to the problem of computing multiple-vertex dominators. We also prove that multiple-vertex dominators can be found in polynomial time. This result is important because there is no known polynomial time algorithm for computing all non-disjoint decompositions of a Boolean function. The fifth algorithm provides an efficient means to decompose a function at the circuit graph level, by using information derived from a BDD representation. This is done without the expensive circuit re-synthesis normally associated with BDD-based decomposition approaches. Finally we present two publications that resulted from the many detours we have taken along the winding path of our research.