In this paper we present the Transalg system, designed to produce SAT encodings for discrete functions, written as programs in a specific language. Translation of such programs to SAT is based on propositional encoding methods for formal computing models and on the concept of symbolic execution. We used the Transalg system to make SAT encodings for a number of cryptographic functions.

Discovering causal relationships from data is the ultimate goal of many research areas. Constraint based causal exploration algorithms, such as PC, FCI, RFCI, PC-simple, IDA and Joint-IDA have achieved significant progress and have many applications. A common problem with these methods is the high computational complexity, which hinders their applications in real world high dimensional datasets, e.g gene expression datasets. In this paper, we present an R package, ParallelPC, that includes the parallelised versions of these causal exploration algorithms. The parallelised algorithms help speed up the procedure of experimenting big datasets and reduce the memory used when running the algorithms. The package is not only suitable for super-computers or clusters, but also convenient for researchers using personal computers with multi core CPUs. Our experiment results on real world datasets show that using the parallelised algorithms it is now practical to explore causal relationships in high dimensional datasets with thousands of variables in a single multicore computer. ParallelPC is available in CRAN repository at https://cran.rproject.org/web/packages/ParallelPC/index.html.

We look at dynamic programming algorithms for propositional model counting, also called #SAT, and MaxSAT. Tools from graph structure theory, in particular treewidth, have been used to successfully identify tractable cases in many subfields of AI, including SAT, Constraint Satisfaction Problems (CSP), Bayesian reasoning, and planning. In this paper we attack #SAT and MaxSAT using similar, but more modern, graph structure tools. The tractable cases will include formulas whose class of incidence graphs have not only unbounded treewidth but also unbounded clique-width. We show that our algorithms extend all previous results for MaxSAT and #SAT achieved by dynamic programming along structural decompositions of the incidence graph of the input formula. We present some limited experimental results, comparing implementations of our algorithms to state-of-the-art #SAT and MaxSAT solvers, as a proof of concept that warrants further research.

Floating-point computations are quickly finding their way in the design of safety- and mission-critical systems, despite the fact that designing floating-point algorithms is significantly more difficult than designing integer algorithms. For this reason, verification and validation of floating-point computations is a hot research topic. An important verification technique, especially in some industrial sectors, is testing. However, generating test data for floating-point intensive programs proved to be a challenging problem. Existing approaches usually resort to random or search-based test data generation, but without symbolic reasoning it is almost impossible to generate test inputs that execute complex paths controlled by floating-point computations. Moreover, as constraint solvers over the reals or the rationals do not natively support the handling of rounding errors, the need arises for efficient constraint solvers over floating-point domains. In this paper, we present and fully justify improved algorithms for the propagation of arithmetic IEEE 754 binary floating-point constraints. The key point of these algorithms is a generalization of an idea by B. Marre and C. Michel that exploits a property of the representation of floating-point numbers.

Pseudo-Boolean constraints, also known as 0-1 Integer Linear Constraints, are used to model many real-world problems. A common approach to solve these constraints is to encode them into a SAT formula. The runtime of the SAT solver on such formula is sensitive to the manner in which the given pseudo-Boolean constraints are encoded. In this paper, we propose generalized Totalizer encoding (GTE), which is an arc-consistency preserving extension of the Totalizer encoding to pseudo-Boolean constraints. Unlike some other encodings, the number of auxiliary variables required for GTE does not depend on the magnitudes of the coefficients. Instead, it depends on the number of distinct combinations of these coefficients. We show the superiority of GTE with respect to other encodings when large pseudo-Boolean constraints have low number of distinct coefficients. Our experimental results also show that GTE remains competitive even when the pseudo-Boolean constraints do not have this characteristic.

Conditional Simple Temporal Network (CSTN) is a constraint-based graph-formalism for conditional temporal planning. It offers a more flexible formalism than the equivalent CSTP model of Tsamardinos, Vidal and Pollack, from which it was derived mainly as a sound formalization. Three notions of consistency arise for CSTNs and CSTPs: weak, strong, and dynamic. Dynamic consistency is the most interesting notion, but it is also the most challenging and it was conjectured to be hard to assess. Tsamardinos, Vidal and Pollack gave a doubly-exponential time algorithm for deciding whether a CSTN is dynamically-consistent and to produce, in the positive case, a dynamic execution strategy of exponential size. In the present work we offer a proof that deciding whether a CSTN is dynamically-consistent is coNP-hard and provide the first singly-exponential time algorithm for this problem, also producing a dynamic execution strategy whenever the input CSTN is dynamically-consistent. The algorithm is based on a novel connection with Mean Payoff Games, a family of two-player combinatorial games on graphs well known for having applications in model-checking and formal verification. The presentation of such connection is mediated by the Hyper Temporal Network model, a tractable generalization of Simple Temporal Networks whose consistency checking is equivalent to determining Mean Payoff Games. In order to analyze the algorithm we introduce a refined notion of dynamic-consistency, named \epsilon-dynamic-consistency, and present a sharp lower bounding analysis on the critical value of the reaction time \hat{\varepsilon} where the CSTN transits from being, to not being, dynamically-consistent. The proof technique introduced in this analysis of \hat{\varepsilon} is applicable more in general when dealing with linear difference constraints which include strict inequalities.

For instance, within the time relations, one can say that an interval A meets another interval B at a coarse granularity In this paper, we propose a qualitative formalism (i.e., looking at it with a general point of view), but for representing and reasoning about time at different that A is before B at a fine granularity (i.e., with a closer point scales. It extends the algebra of Euzenat [2001] of view). The usual algebras cannot process this knowledge and overcomes its major limitations, allowing one without leading to an inconsistency. To solve this problem, to reason about relations between points and intervals. Euzenat has proposed a granular extension of the point algebra Our approach is more expressive than of Vilain et al. and one of Allen's interval algebra [Euzenat, the other algebras of temporal relations: for instance, 2001], each one providing a table describing how relations some relations are more relaxed than those change when considered at a finer granularity (downward in Allen's [1983] algebra, while others are stricter.

Symmetries are common in many constraint problems. They can be broken statically or dynamically. The focus of this paper is the symmetry breaking during search (SBDS) method that adds conditional symmetry breaking constraints upon each backtracking during search. To trade completeness for efficiency, partial SBDS (ParSBDS) is proposed by posting only a subset of symmetries. We propose an adaptation method recursive SBDS (ReSBDS) of ParSBDS which extends ParSBDS to break more symmetry compositions. We observe that the symmetry breaking constraints added for each symmetry at a search node are nogoods and increasing. A global constraint (incNGs), which is logically equivalent to a set of increasing nogoods, is derived. To further trade pruning power for efficiency, we propose weak-nogood consistency (WNC) for nogoods and a lazy propagator for SBDS (and its variants) using watched literal technology. We further define generalized weak-incNGs consistency (GWIC) for a conjunction of increasing nogoods, and give a lazy propagator for incNGs.

As part of the ongoing effort of designing secure DCOP algorithms, we propose P-Max-Sum, the first private algorithm that is based on Max-Sum. The proposed algorithm has multiple agents preforming the role of each node in the factor graph, on which the Max-Sum algorithm operates. P-Max-Sum preserves three types of privacy: topology privacy, constraint privacy, and assignment/decision privacy.By allowing a single call to a trusted coordinator, P-Max-Sum also preserves agent privacy. The two main cryptographic means that enable this privacy preservation are secret sharing and homomorphic encryption. Our experiments on structured and realistic problems show that the overhead of privacy preservation in terms of runtime is reasonable.

Raven’s Progressive Matrices (RPMs) are a popular family of general intelligence tests, and provide a non-verbal measure of a test subject’s reasoning abilities. Traditionally RPMs have been manually designed. To make them readily available for both practice and examination, we tackle the problem of automatically synthesizing RPMs. Our goal is to efficiently generate a large number of RPMs that are authentic (i.e. similar to manually written problems), interesting (i.e. diverse in terms of difficulty), and well-formed (i.e unambiguous). The main technical challenges are: How to formalize RPMs to accommodate their seemingly enormous diversity, and how to define and enforce their validity? To this end, we (1) introduce an abstract representation of RPMs using first-order logic, and (2) restrict instantiations to only valid RPMs. We have realized our approach and evaluated its efficiency and effectiveness. We show that our system can generate hundreds of valid problems per second with varying levels of difficulty. More importantly, we show, via a user study with 24 participants, that the generated problems are statistically indistinguishable from actual problems. This work is an exciting instance of how logic and reasoning may aid general learning.