Formal concept analysis (FCA) is largely applied in different areas. However, in some FCA applications the volume of information that needs to be processed can become unfeasible. Thus, the demand for new approaches and algorithms that enable processing large amounts of information is increasing substantially. This article presents a new algorithm for extracting proper implications from high-dimensional contexts. The proposed algorithm, called ImplicPBDD, was based on the PropIm algorithm, and uses a data structure called binary decision diagram (BDD) to simplify the representation of the formal context and enhance the extraction of proper implications. In order to analyze the performance of the ImplicPBDD algorithm, we performed tests using synthetic contexts varying the number of objects, attributes and context density. The experiments show that ImplicPBDD has a better performance—up to 80% faster—than its original algorithm, regardless of the number of attributes, objects and densities.

Formal Concept Analysis (FCA) is an applied mathematical technique for data analysis, in which the relations between objects and attributes are identified. It introduces the notion of concepts and their hierarchical structure, from which we can obtain a set of implications between attributes that characterize a knowledge domain. The volume of information to be processed makes the use of FCA difficult in domains with a high number of dimensions, creating a demand for new solutions and algorithms for FCA applications. This article explores different approaches to extract proper implications from high dimensional contexts based on constraints to obtain the set of implications rules. We propose algorithms that use a data structure called Binary Decision Diagram (BDD) to represent the formal context, which reduces its size and, due to this, operates more efficiently. We also propose a heuristic to obtain proper implications by reducing the unnecessary generation of premises. In addition, we implemented a parallel computing model for generating and obtaining different implications. To analyze the proposed algorithms, we used different synthetic contexts with a varying number of objects, attributes, and density. The results obtained presented speed gains of up to 22 times when compared to the solutions proposed in the literature such as Impec and PropIm.

Triadic Concept Analysis (TCA) is an applied mathematical technique for data analysis which the relations between objects, attributes and conditions are identified. However, the volume of information to be processed could make TCA impracticable. For example, with the increasing of social network for personal (Facebook) and professional (LinkedIn) usage, more and more applications of data analysis on environments with high dimensionality (Big Data) have been discussed in the literature. This paper has as an objective to evaluate the behavior of the TRIAS algorithm in order to extract triadic concepts in high dimensional contexts. The experiments shows that our approach has a better performance - up to 33% faster - than its original algorithm.

In recent years new and efficient symbolic model checking algorithms have been developed. One technique, bounded model checking or BMC, has been particularly promising. BMC models the system being verified as a boolean formula whose satisfying assignments provide counterexamples for properties verified. BMC unrolls the system in its multiple iterations. Because of this the structure of the formula representing the system is very symmetric, since all iterations are similar in structure. This work explores this symmetry in a distributed algorithm by postponing the unrolling of the formulas until they are used. This minimizes communication among processors since the formulas transmitted are shorter. Moreover, avoiding the unrolling of conflict clauses has a more pronounced effect, because due to the symmetric nature of the formula, a conflict clause for one instant in the execution can be applied to time multiple instants. As a consequence, short conflict clauses can be unrolled into much more effective clauses, cutting back on the search space significantly. In our experiments we have obtained gains of up to 35% in verification time in some examples.