ABSTRACT. SAT and SAT Modulo Theories (SMT) are well known as workhorses for formal verification applications.  But SAT- and SMT-like techniques are also highly effective for AI applications such as constraint solving and optimization.  Here we explain how this idea has been validated at Barcelogic.com and elsewhere.  We shorty introduce SAT/SMT as well as our new IntSat method for Integer Linear Programming (ILP) and 0-1 ILP. 

Some demos on real-world industrial problems will illustrate easy logic-based modeling and cases where our solvers outperform the best-known commercial ones.

ABSTRACT. We study two modal logics of trust that interconnect the trust modality with the individual belief modalities of agents. One logic includes an axiom stating that if agent i trusts agent j with respect to a statement p then i believes that j does not disbelieve p. In the second logic, if i trusts j concerning p then i believes that j believes p. These extensions of the logic of trust help to solve some unintuitive consequences that arise when the semantics of trust and belief are independent. As a main technical result we prove the soundness and completeness of these logics.

ABSTRACT. Metis is an automated theorem prover based on ordered paramodulation. It is widely employed in the interactive theorem provers Isabelle/HOL and HOL4 to automate proofs as well as reconstruct proofs found by automated provers. For both these purposes, the tableaux-based MESON tactic is frequently used in HOL Light. However, paramodulation-based provers such as Metis perform better on many problems involving equality. We created a Metis-based tactic in HOL Light which translates HOL problems to Metis, runs an OCaml version of Metis, and reconstructs proofs in Metis' paramodulation calculus as HOL proofs. We evaluate the performance of Metis as proof reconstruction method in HOL Light.

ABSTRACT. The aim of this work is to define a resolution method for the modal logic S5. We first propose a conjunctive normal form (S5-CNF) which is mainly based on using labels referring to semantic worlds. In a sense, S5-CNF can be seen as a generalization of the conjunctive normal form in propositional logic by using in the clause structure the modal connective of necessity and labels. We show that every S5 formula can be transformed into an S5-CNF formula using a linear encoding. Then, in order to show the suitability of our normal form, we describe a modeling of the problem of graph coloring. Finally, we introduce a simple resolution method for S5, composed of three deductive rules, and we show that it is sound and complete. Our deductive rules can be seen as adaptations of Robinson’s resolution rule to the possible-worlds semantics.

ABSTRACT. The application of e-mail is the most widespread communication method. The increased email number includes permanently increased amount of unwanted notifications (spam). The statistics claims that 80% of the traffic is spam that lags the internet traffic, consumes space on hard disc, and reduces the capacity of the network, not to mention time spent for email’s classification. The advanced E-mail service packs contain spam filtration program. Nevertheless, to classify the e-mails as spam fully depends on the consumers, as information acceptable (or vital) for one consumer, may be a spam for other. Hence, it is crucial to have automatic spam filtration system for every individual consumer. The paper discuss the solution, a learning system that filters emails through consumers’ parameters and gradually learn how to filter them accordingly. The system based on multi-layer neural network, which uses logistic activation function, learns via tutor and counter-spread algorithm of mistakes

ABSTRACT. Energy optimization problem in Wireless Sensor Networks (WSN) is a backbone of efficient performance of sensor network consisting of small devices with limited and non-recovering battery. WSN lifetime maximization problem under assumption of that the coverage is main task of the network is known as Maximal lifetime coverage problem (MLCP).

This problem belongs to a class of NP-hard problems. In this paper we propose a novel simulated annealing (SA) algorithm to solve MLCP. The proposed algorithm is studied for high dense WSN instances under different parameter setup.

ABSTRACT. Organic Synthesis is a computationally challenging practical problem concerned with constructing  a target molecule from a set of initially available molecules via  chemical reactions. This paper demonstrates how organic synthesis  can be formulated as a planning problem in Artificial Intelligence, and how it can be explored using the state-of-the-art domain independent planners. To this end, we develop a methodology to represent chemical molecules and generic reactions in PDDL 2.2, a version of the standardized Planning Domain  Definition Language popular in AI. In our model, derived predicates define  common functional groups and chemical classes in chemistry, and actions  correspond to generic chemical reactions.  We develop a set of benchmark problems. Since PDDL is supported as an input language by many modern planners, our benchmark can be subsequently useful for  empirical assessment of the performance of various state-of-the-art planners.

ABSTRACT. Genetic algorithms have been applied to various optimization problems in the past. Our library GeneiAL implements a framework for genetic algorithms specially targeted to the area of hybrid electric vehicles. In a parallel hybrid electric vehicle (PHEV), an internal combustion engine and an electrical motor are coupled on the same axis in parallel. In the area of PHEVs, genetic algorithms have been extensively used for the optimization of parameter tuning of control strategies. We use GeneiAL to control the torque distribution between the engines directly. The objective function of this control strategy minimizes the weighted sum of functions that evaluate the fuel consumption, the battery state of charge, and drivability aspects over a prediction horizon of fixed finite length.

We analyze the influence of these weights and different configurations for the genetic algorithm on the computation time, the convergence, and the quality of the optimization result. For promising configurations, we compare the results of our control strategy with common control strategies.

ABSTRACT. First-order theorem provers have to search for proofs in an infinite space of possible derivations. Proof search heuristics play a vital role for the practical performance of these systems. In the current generation of saturation-based theorem provers like SPASS, E, Vampire or Prover~9, one of the most important decisions is the selection of the next clause to process with the given clause algorithms. Provers offer a wide variety of basic clause evaluation functions, which can often be parameterized and combined in many different ways. Finding good strategies is usually left to the users or developers, often backed by large-scale experimental evaluations. We describe a way to automatize this process using genetic algorithms, evaluating a population of different strategies on a test set, and applying mutation and crossover operators to good strategies to create the next generation. We describe the design and experimental set-up, and report on first promising results.

ABSTRACT. The Countdown game is one of the oldest TV show in the world. It started broadcasting in 1972 on the french television and in 1982 on British channel 4, and it has been running since in both countries. The game, while extremely popular, never received any serious scientific attention, probably because it seems too simple at first sight. We present in this article an in-depth analysis of the numbers round of the countdown game. This includes a complexity analysis of the game, an analysis of existing algorithms and the presentation of a new algorithm that increases resolution speed by a large factor. It also includes some leads on how to turn the game into a more difficult one, both for a human player and for a computer, and even to transform it into a possibly undecidable problem.

ABSTRACT. In recent years it was proposed to encode bounded model checking (BMC) into the effectively propositional fragment of first-order logic (EPR). The EPR fragment can provide for a succinct representation of the problem and facilitate reasoning at a higher level. In this paper we present an extension of the EPR-based bounded model checking with k-induction which can be used to prove safety properties of systems over unbounded runs. We present a novel abstraction-refinement approach based on unsatisfiable cores and models (UCM) for BMC and k-induction in the EPR setting. We have implemented UCM refinements for EPR-based BMC and k-induction in a first-order automated theorem prover iProver. We also extended iProver with the AIGER format and evaluated it over the HWMCC'14 competition benchmarks. The experimental results are encouraging. We show that a number of AIG problems can be verified until deeper bounds with the EPR-based model checking.

ABSTRACT. We introduce the notion of strongly distributed structures and present a uniform approach to incremental automated reasoning on them. The approach is based on systematic use of two logical reduction techniques: Feferman-Vaught reductions and syntactically defined translation schemes. The distributed systems are presented as logical structures $\fA$'s. We propose a uniform template for methods, which allow for certain cost evaluation of formulae of logic $\mcL$ over $\fA$ from values of formulae over its components and values of formulae over the index structure $\cI$. Given logic $\cL$, structure $\fA$ as a composition of structures $\fA_i, i \in I$, index structure $\cI$ and formula $\phi$ of the logic to be evaluated on $\fA$, the question is: what is the reduction sequence for $\phi$ if any. We show that if we may prove preservation theorems for $\cL$ as well as if $\fA$ is a strongly distributed composition of its components then the corresponding reduction sequence for $\fA$ may be effectively computed. We show that the approach works for lots of extensions of $FOL$ but not all. The considered extensions of $FOL$ are suitable candidates for modeling languages for components and services, used in incremental automated reasoning, data mining, decision making, planning and scheduling. A short complexity analysis of the method is also provided.