Thesis (M.S.)--State University of New York at Binghamton, Thomas J. Watson School of Engineering and Applied Science, Department of Systems Science and Industrial Engineering, 2009. / Includes bibliographical references.

Este trabalho apresenta a composição funcional (CF) como um novo paradigma para realização da síntese lógica de blocos combinacionais. CF usa uma abordagem ascendente para sintetizar funções Booleanas, sendo capaz de avaliar os custos das funções intermediárias e explorando dessa forma um grande número de combinações diferentes de funções candidatas. Há vantagens interessantes quando comparado à abordagem descendente da decomposição funcional. CF apresenta grande flexibilidade para criar algoritmos com resultados ótimos ou subótimos para diferentes aplicações. A estratégia proposta apresenta bons resultados para síntese de funções Booleanas visando diferentes tecnologias. CF é baseado nos seguintes princípios: (1) representação de funções lógicas como um par ligado com representações funcional e estrutural; (2) o algoritmo começa de um conjunto de funções iniciais; (3) funções mais simples são associadas para criar funções mais complexas; (4) existe uma ordem parcial que permite o uso da programação dinâmica; (5) um conjunto de funções permitidas pode ser mantido para reduzir o tempo de execução/consumo de memória. Este trabalho apresenta algoritmos de composição funcional para fatoração Booleana, incluindo fatoração ótima, fatoração considerando o operador OU-exclusivo, computação de cadeias mínimas de decisão e síntese de funções considerando somente portas lógicas majoritárias e inversores. / This work presents functional composition (FC) as a new paradigm for combinational logic synthesis. FC is a bottom-up approach to synthesize Boolean functions, being able to evaluate the cost of intermediate sub-functions, exploring a larger number of different candidate combinations. These are interesting advantages when compared to the top-down behavior of functional decomposition. FC presents great flexibility to implement algorithms with optimal or suboptimal results for different applications. The proposed strategy presents good results for the synthesis of Boolean functions targeting different technologies. FC is based on the following principles: (1) the representation of logic functions is done by a bonded pair of functional and structural representations; (2) the algorithm starts from a set of initial functions; (3) simpler functions are associated to create more complex ones; (4) there is a partial order, enabling dynamic programming; (5) a set of allowed functions can be used in order to reduce execution time/memory consumption. This work presents functional composition algorithms for Boolean factoring, including optimal factoring, Boolean factoring considering the exclusive-OR operator, minimum decision chain computation and synthesis of functions considering only majority and inverter logic gates.

Este trabalho apresenta a composição funcional (CF) como um novo paradigma para realização da síntese lógica de blocos combinacionais. CF usa uma abordagem ascendente para sintetizar funções Booleanas, sendo capaz de avaliar os custos das funções intermediárias e explorando dessa forma um grande número de combinações diferentes de funções candidatas. Há vantagens interessantes quando comparado à abordagem descendente da decomposição funcional. CF apresenta grande flexibilidade para criar algoritmos com resultados ótimos ou subótimos para diferentes aplicações. A estratégia proposta apresenta bons resultados para síntese de funções Booleanas visando diferentes tecnologias. CF é baseado nos seguintes princípios: (1) representação de funções lógicas como um par ligado com representações funcional e estrutural; (2) o algoritmo começa de um conjunto de funções iniciais; (3) funções mais simples são associadas para criar funções mais complexas; (4) existe uma ordem parcial que permite o uso da programação dinâmica; (5) um conjunto de funções permitidas pode ser mantido para reduzir o tempo de execução/consumo de memória. Este trabalho apresenta algoritmos de composição funcional para fatoração Booleana, incluindo fatoração ótima, fatoração considerando o operador OU-exclusivo, computação de cadeias mínimas de decisão e síntese de funções considerando somente portas lógicas majoritárias e inversores. / This work presents functional composition (FC) as a new paradigm for combinational logic synthesis. FC is a bottom-up approach to synthesize Boolean functions, being able to evaluate the cost of intermediate sub-functions, exploring a larger number of different candidate combinations. These are interesting advantages when compared to the top-down behavior of functional decomposition. FC presents great flexibility to implement algorithms with optimal or suboptimal results for different applications. The proposed strategy presents good results for the synthesis of Boolean functions targeting different technologies. FC is based on the following principles: (1) the representation of logic functions is done by a bonded pair of functional and structural representations; (2) the algorithm starts from a set of initial functions; (3) simpler functions are associated to create more complex ones; (4) there is a partial order, enabling dynamic programming; (5) a set of allowed functions can be used in order to reduce execution time/memory consumption. This work presents functional composition algorithms for Boolean factoring, including optimal factoring, Boolean factoring considering the exclusive-OR operator, minimum decision chain computation and synthesis of functions considering only majority and inverter logic gates.

No description available.

When trying to apply recently developed approaches for updating Description Logic ABoxes in the context of an action programming language, one encounters two problems. First, updates generate so-called Boolean ABoxes, which cannot be handled by traditional Description Logic reasoners. Second, iterated update operations result in very large Boolean ABoxes, which, however, contain a huge amount of redundant information. In this paper, we address both issues from a practical point of view.

Tableau-based decision procedures have been successfully used for solving a wide variety of problems. For some applications, nonetheless, it is desirable not only to obtain a Boolean answer, but also to detect the causes for such a result. In this report, a method for finding explanations on tableau-based procedures is explored, generalizing previous results on the field. The importance and use of the method is shown by means of examples.

Cette thèse aborde le problème de la décomposition booléenne des tableaux multidimensionnels de données binaires par modèle de mélange post non-linéaire. Dans la première partie, nous introduisons une nouvelle approche pour la factorisation booléenne en matrices binaires (FBMB) fondée sur un modèle de mélange post non-linéaire. Contrairement aux autres méthodes de factorisation de matrices binaires existantes, fondées sur le produit matriciel classique, le modèle proposé est équivalent au modèle booléen de factorisation matricielle lorsque les entrées des facteurs sont exactement binaires et donne des résultats plus interprétables dans le cas de sources binaires corrélées, et des rangs d'approximation matricielle plus faibles. Une condition nécessaire et suffisante d'unicité pour la FBMB est également fournie. Deux algorithmes s'appuyant sur une mise à jour multiplicative sont proposés et illustrés dans des simulations numériques ainsi que sur un jeu de données réelles. La généralisation de cette approche au cas de tableaux multidimensionnels (tenseurs) binaires conduit à la factorisation booléenne de tenseurs binaires (FBTB). La démonstration de la condition nécessaire et suffisante d’unicité de la décomposition booléenne de tenseurs binaires repose sur la notion d'indépendance booléenne d'une famille de vecteurs. L'algorithme multiplicatif fondé sur le modèle de mélange post non-linéaire est étendu au cas multidimensionnel. Nous proposons également un nouvel algorithme, plus efficace, s'appuyant sur une stratégie de type AO-ADMM (Alternating Optimization -ADMM). Ces algorithmes sont comparés à ceux de l'état de l'art sur des données simulées et sur un jeu de données réelles / This work is dedicated to the study of boolean decompositions of binary multidimensional arrays using a post nonlinear mixture model. In the first part, we introduce a new approach for the boolean factorization of binary matrices (BFBM) based on a post nonlinear mixture model. Unlike the existing binary matrix factorization methods, the proposed method is equivalent to the boolean factorization model when the matrices are strictly binary and give thus more interpretable results in the case of correlated sources and lower rank matrix approximations compared to other state-of-the-art algorithms. A necessary and suffi-cient condition for the uniqueness of the BFBM is also provided. Two algorithms based on multiplicative update rules are proposed and tested in numerical simulations, as well as on a real dataset. The gener-alization of this approach to the case of binary multidimensional arrays (tensors) leads to the boolean factorisation of binary tensors (BFBT). The proof of the necessary and sufficient condition for the boolean decomposition of binary tensors is based on a notion of boolean independence of binary vectors. The multiplicative algorithm based on the post nonlinear mixture model is extended to the multidimensional case. We also propose a new algorithm based on an AO-ADMM (Alternating Optimization-ADMM) strategy. These algorithms are compared to state-of-the-art algorithms on simulated and on real data

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.

In this thesis we study Boolean functions from three different perspectives. First, we study the complex- ity of Boolean minimization for several classes of formulas with polynomially solvable SAT, and formulate sufficient conditions for a class which cause the minimization problem to drop at least one level in the polyno- mial hierarchy. Second, we study a class of matched CNFs for which SAT is trivial but minimization remains Σp 2 complete. We prove that every matched CNF has at least one equivalent prime and irredundant CNF that is also matched. We use this fact to prove the main result of this part, namely that for every matched CNF all clause minimal equivalent CNFs are also matched. Third, we look at propagation completeness - the property of a CNF that says that for every partial assignment all entailed literals can be discovered by unit propagation. We can extend every CNF to be propagation complete by adding empowering impli- cates to it. The main result of this section is a the proof of coNP completeness of the recognition problem for propagation complete CNFs. We also show that there exist CNFs to which an exponential number of empowering implicates have to be added to make them propagation complete.

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.