The growing scale of industrial applications encoded to Boolean Satisfiability (SAT) problems imposed the researchers to practice SAT simplification as an imperative requirement for any SAT solver. In this talk, I will discuss how GPU can be utilized to perform variable and subsumption eliminations in parallel. Benchmarks show that our proposed simplifier (SIGmA) achieved an …continue reading

An algorithm for deciding strong probabilistic bisimulation, referred to as BEM, was proposed in 2000 by Baier, Engelen, and Majster-Cederbaum claiming O(m n log n) complexity for the construction of the bisimulation equivalence classes of a probabilistic automaton. Besides so-called Ordered Balanced Trees, the BEM algorithm uses straightforward datastructures. More recently, Groote and Rivera Verduzco …continue reading