Many industrial verification problems are solved via reduction to CircuitSAT (curcuit satisfibiliaty). It is often the case that the resulting SAT instances are very hard and require the use of parallel computing to be solved in reasonable time. The particularly relevant problem in this context is how to best plan the use of the computing resources, because SAT solvers' runtime is well known to be hard to predict. In the present paper we propose two methods that employ the knowledge about a circuit's structure to partition a CircuitSAT instance into a specific number of simpler subproblems. A distinctive feature of the proposed partitioning methods is that they make it possible to estimate the hardness (e.g. the total runtime of a SAT solver on all subproblems) of a partitioning via the Monte Carlo method. In the experimental evaluation we apply these methods to hard CircuitSAT instances and compare their performance with the well known Cube and Conquer approach. The proposed partitioning methods not only often outperform Cube and Conquer, but also show remarkably small variance in the runtime of a SAT solver on subproblems from a partitioning, thus making it possible to construct accurate estimations of time required to process all subproblems, using random samples of small size. As a consequence, we have the efficient stochastic estimation procedure which provides an additional opportunity to employ hyperparameter tuning methods to further increase the SAT solver performance on (partitioned) hard SAT instances. We demonstrate the effectiveness of the proposed constructions by applying them to some problems associated with CircuitSAT, in particular, Logical Equivalence Checking benchmarks, Automated Test Pattern Generation benchmarks and the inversion problems of some cryptographic functions.

Backdoors for SAT, proposed by Williams et al. in 2003, are the sets of variables, the instantiation of which vastly simplifies the resulting subproblem. The focus of the present paper are.-backdoors- the probabilistic generalization of Strong Backdoor Sets. Unlike most kinds of backdoors, small rho-backdoors with rho > 0 are relatively easy to find and they can be found in many formulas. In the theoretical part of the paper, we show that there exists a connection between rho-backdoors and the conflict information generated by CDCL SAT solvers. On the one hand, any set of variables appearing in some learnt clauses can be viewed as a.-backdoor (with rho> 0) with respect to the Unit Propagation (UP) rule. On the other hand, surprisingly, rho-backdoors can often be used to generate logical entailments of a formula, which can be viewed as learnt clauses, and we present several techniques and algorithms, that can be used to derive such clauses. We also show that a rho-backdoor with rho > 0 can be considered as a partial unsatisfiability certificate for a CNF formula as it proves that the formula is false for the fraction of at least rho of all possible assignments. Therefore, from the practical viewpoint, finding rho-backdoors with. close to 1 makes sense. To evaluate the proposed techniques, we implemented a proof-of-concept prototype, that interleaves the backdoor-based techniques with standard CDCL solving, and evaluated it on a variety of challenging benchmarks. The results of the experiments show that the proposed technique makes it possible to speed up the SAT solving for many hard SAT instances both from SAT Competitions and of industrial origin.

In the paper we consider the discrete variant of the well-known Influence Maximization Problem (IMP). Given some influence model, it consists in finding a so-called seed set of influential users of fixed size, that maximizes the total spread of influence over the network. We limit our study to the influence model called Deterministic Linear Threshold Model (DLTM). It is well known that IMP under DLTM is computationally hard and there are no approximate algorithms for its solving with a constant approximation ratio if $P\neq NP$. Therefore, it makes sense to apply metaheuristic algorithms to this problem. In the present research we propose new algorithms for solving IMP under DLTM, which are based on a technique that combines evolutionary and genetic strategies for pseudo-Boolean optimization with a greedy algorithm which is used to find some initial approximation. We use the proposed strategy to solve another well-known combinatorial problem for networks called Target Set Selection (TSS). We propose to solve TSS as a sequence of IMPs with gradually decreasing of target set size. In the experimental part of the paper we demonstrate that our new strategy outperforms the previous ways to solve TSS, yielding smaller target sets of good quality.

Retrophylogenomics makes use of genome-wide retrotransposon presence/absence insertion patterns to resolve questions in phylogeny and population genetics. In the genomics era, evaluating high-throughput data requires the associated development of appropriately powerful statistical tools. The currently used KKSC 3-lineage statistical test for estimating the significance of retrophylogenomic data is limited by the number of possible tree topologies it can assess in one step. To improve on this, we have extended the analysis to simultaneously compare four lineages, enabling us to evaluate ten distinct presence/absence insertion patterns for 26 possible tree topologies plus 129 trees with different incidences of hybridization or introgression. The new tool provides statistics for cases involving multiple ancestral hybridizations/introgressions, ancestral incomplete lineage sorting, bifurcation, and polytomy. The test is embedded in a user-friendly web R application (http://retrogenomics.uni-muenster.de:3838/hammlet/) and is available for use by the scientific community. [ancestral hybridization/introgression; ancestral incomplete lineage sorting (ILS); empirical distribution; KKSC-statistics; 4-lineage (4-LIN) insertion polymorphism; polytomy; retrophylogenomics.].

In this paper we investigate how to estimate the hardness of Boolean satisfiability (SAT) encodings for the Logical Equivalence Checking problem (LEC). Meaningful estimates of hardness are important in cases when a conventional SAT solver cannot solve a SAT instance in a reasonable time. We show that the hardness of SAT encodings for LEC instances can be estimated \textit{w.r.t.} some SAT partitioning. We also demonstrate the dependence of the accuracy of the resulting estimates on the probabilistic characteristics of a specially defined random variable associated with the considered partitioning. The paper proposes several methods for constructing partitionings, which, when used in practice, allow one to estimate the hardness of SAT encodings for LEC with good accuracy. In the experimental part we propose a class of scalable LEC tests that give extremely complex instances with a relatively small input size $n$ of the considered circuits. For example, for $n = 40$, none of the state-of-the-art SAT solvers can cope with the considered tests in a reasonable time. However, these tests can be solved in parallel using the proposed partitioning methods.

Finite-state models are widely used in software engineering, especially in the development of control systems. In control applications, such models are often developed manually, which can make it difficult to keep them up to date. To simplify the maintenance process, an automatic approach can be used to infer models from behavior examples and temporal specification. As an example of a specific control systems development application, we focus on inferring finite-state models of function blocks (FBs) defined by the IEC 61499 international standard for distributed automation systems. In this paper, we propose a method for inferring FB models from behavior examples based on reduction to the Boolean satisfiability problem (SAT). Additionally, we take into account linear temporal properties using counterexample-guided synthesis. The developed tool, fbSAT, implementing the proposed method is evaluated in three case studies: inferring a finite-state controller for a Pick-and-Place manipulator, reconstructing randomly generated automata, and minimizing transition systems. In contrast to existing approaches, the suggested method is more efficient and produces finite-state models that are minimal in terms of both the number of states and the complexity of guard conditions.

This article proposes a new method for automatic synthesis of distributed discrete-state controllers from given temporal specification and behavior examples. The proposed method develops known synthesis methods to the distributed case, which is a fundamental extension. This method can be applied for automatic generation of correct-by-design distributed control software for industrial automation. The proposed approach is based on reduction to the Boolean satisfiability problem (SAT) and has Counterexample-Guided Inductive Synthesis (CEGIS) at its core. We evaluate the proposed approach using the classical distributed alternating bit protocol.

Nowadays an increasing number of industries are considering moving toward being Industry 4.0 compliant. But this transition is not straightforward: transfer to new system can lead to significant production downtime, resulting in delays and cost overruns. The best way is systematic seamless transition to newer and advanced technologies that Industry 4.0 offers. This article proposes a framework based on automatic synthesis methods that learns the behavior of an existing legacy programmable logic controller (PLC) and generates state machines that can be incorporated into IEC 61499 function blocks. Proposed algorithms are based on Boolean satisfiability (SAT) solvers. The first algorithm accepts a set of noisy PLC traces and produces a set of candidate state machines that satisfy the traces. The second algorithm accepts error-free traces and synthesizes a modular controller that may be distributed across several physical devices. The toolchain architecture is exemplified on a laboratory scale Festo mechatronic system.