Ants Colony Optimization Algorithm in the Hopfield Neural Network for Agricultural Soil Fertility Reverse Analysis

The Boolean Satisfiability Problem (BSAT) is one of the most important decision problems in mathematical logic and computational sciences for determining whether or not a solution to a Boolean formula.. Hopfield neural network (HNN) is one of the major type artificial neural network (NN) popularly known for it used in solving various optimization and decision problems based on its energy minimization machinism. The existing models that incorporate standalone network projected non-versatile framework as fundamental Hopfield type of neural network (HNN) employs random search in its training stages and sometimes get trapped at local optimal solution. In this study, Ants Colony Optimzation Algorithm (ACO) as a novel variant of probabilistic metaheuristic algorithm (MA) inspired by the behavior of real Ants, has been incorporated in the training phase of Hopfield types of the neural network (HNN) to accelerate the training process for Random Boolean kSatisfiability reverse analysis (RANkSATRA) based for logic mining. The proposed hybrid model has been evaluated according to robustness and accuracy of the induced logic obtained based on the agricultural soil fertility data set (ASFDS). Based on the experimental simulation results, it reveals that the ACO can effectively work with the Hopfield type of neural network (HNN) for Random 3 Satisfiability Reverse Analysis with 87.5 % classification accuracy

On the Representation of Boolean and Real Functions as Hamiltonians for Quantum Computing

Mapping functions on bits to Hamiltonians acting on qubits has many applications in quantum computing. In particular, Hamiltonians representing Boolean functions are required for applications of quantum annealing or the quantum approximate optimization algorithm to combinatorial optimization problems. We show how such functions are naturally represented by Hamiltonians given as sums of Pauli Z operators (Ising spin operators) with the terms of the sum corresponding to the function’s Fourier expansion. For many classes of Boolean functions which are given by a compact description, such as a Boolean formula in conjunctive normal form that gives an instance of the satisfiability problem, it is #P-hard to compute its Hamiltonian representation, i.e., as hard as computing its number of satisfying assignments. On the other hand, no such difficulty exists generally for constructing Hamiltonians representing a real function such as a sum of local Boolean clauses each acting on a fixed number of bits as is common in constraint satisfaction problems. We show composition rules for explicitly constructing Hamiltonians representing a wide variety of Boolean and real functions by combining Hamiltonians representing simpler clauses as building blocks, which are particularly suitable for direct implementation as classical software. We further apply our results to the construction of controlled-unitary operators, and to the special case of operators that compute function values in an ancilla qubit register. Finally, we outline several additional applications and extensions of our results to quantum algorithms for optimization. A goal of this work is to provide a design toolkit for quantum optimization which may be utilized by experts and practitioners alike in the construction and analysis of new quantum algorithms, and at the same time to provide a unified framework for the various constructions appearing in the literature.

The Model Counting Competition 2020

Many computational problems in modern society account to probabilistic reasoning, statistics, and combinatorics. A variety of these real-world questions can be solved by representing the question in (Boolean) formulas and associating the number of models of the formula directly with the answer to the question. Since there has been an increasing interest in practical problem solving for model counting over the past years, the Model Counting Competition was conceived in fall 2019. The competition aims to foster applications, identify new challenging benchmarks, and promote new solvers and improve established solvers for the model counting problem and versions thereof. We hope that the results can be a good indicator of the current feasibility of model counting and spark many new applications. In this article, we report on details of the Model Counting Competition 2020, about carrying out the competition, and the results. The competition encompassed three versions of the model counting problem, which we evaluated in separate tracks. The first track featured the model counting problem, which asks for the number of models of a given Boolean formula. On the second track, we challenged developers to submit programs that solve the weighted model counting problem. The last track was dedicated to projected model counting. In total, we received a surprising number of nine solvers in 34 versions from eight groups.

Investigation of observability property of controlled binary dynamical systems: a logical approach

The property of observability of controlled binary dynamical systems is investigated. A formal definition of the property is given in the language of applied logic of predicates with bounded quantifiers of existence and universality. A Boolean model of the property is built in the form of a quantified Boolean formula accordingly to the Boolean constraints method developed by the authors. This formula satisfies both the logical specification of the property and the equations of the binary system dynamics. Aspects of the proposed approach implementation for the study of the observability property are considered. The technology of checking the feasibility of the property using an applied microservice package is demonstrated in several examples.

A logical method for the synthesis of periodic trajectory in a binary dynamical system

A logic method for structural-parametric synthesis of a binary dynamical system with a given periodic trajectory is proposed. This method provides a constructive solution for the considered problem. The attraction region of such a trajectory must coincide with a given subset of the state space. An additional constraint sets the acceptable time for reaching this trajectory from its attraction region. As admissible structures for dynamical models of the synthesis, we consider the following systems: linear systems, systems with the disjunctive and conjunctive right sides. All conditions of the problem are written in the form of a quantified Boolean formula with subsequent verification of its truth using a specialized solver, which gives values of the required parameters of the dynamical model. The software implementation of the proposed method in the form of a composite service is presented. All stages of the parametric synthesis of a Boolean network based on the proposed method are demonstrated in the example of a one-step linear system.

Automatic Test Pattern Generation using Grover’s Algorithm

Quantum computing is an exciting new field in the intersection of computer science, physics and mathematics. It refines the central concepts from Quantum mechanics into its least difficult structures, peeling away the complications from the physical world. Any combinational circuit that has only one stuck at fault can be tested by applying a set of inputs that drive the circuit to verify the output response. The outputs of that circuit will be different from the one desired if the faults exist. This project describes a method of generating test patterns using the Boolean satisfaction method. First, the Boolean formula is constructed to express the Boolean difference between a fault-free circuit and a faulty circuit. Second, the Boolean satisfaction algorithm is applied to the formula in the previous step. The Grover algorithm is used to solve the Boolean satisfaction problem. The Boolean Satisfiability problem for Automatic Test Pattern Generation(ATPG) is implemented on IBM Quantum Experience. The Python program initially generates the boolean expression from the file and converts it into Conjunctive Normal Form(CNF) which is passed on to Grover Oracle and runs on IBM simulator and produces excellent results on combinational circuits for test pattern generation with a quadratic speedup. Grover’s Algorithm on this problem has a run time of O(√N).

Using Eight-Variable Karnaugh Maps to Unravel Hidden Technicalities in Qualitative Comparative Analysis

We use a regular and modular eight-variable Karnaugh map to reveal some technical details of Boolean minimization usually employed in solving problems of Qualitative Comparative Analysis (QCA). We utilize as a large running example a prominent eight-variable political-science problem of sparse diversity (involving a partially-defined Boolean function (PDBF), that is dominantly unspecified). We recover the published solution of this problem, showing that it is merely one candidate solution among a set of many equally-likely competitive solutions. We immediately obtain one of these rival solutions, that looks better than the published solution in two aspects, namely: (a) it is based on a smaller minimal set of supporting variables, and (b) it provides a more compact Boolean formula. However, we refrain from labelling our solution as a better one, but instead we stress that it is simply un-comparable with the published solution. The comparison between any two rival solutions should be context-specific and not tool-specific. In fact, the Boolean minimization technique, borrowed from the area of digital design, cannot be used as is in QCA context. A more suitable paradigm for QCA problems is to identify all minimal sets of supporting variables (possibly via integer programming), and then obtain all irredundant disjunctive forms (IDFs) for each of these sets. Such a paradigm stresses inherent ambiguity, and does not seem appealing as the QCA one, which usually provides a decisive answer (irrespective of whether it is justified or not).The problem studied herein is shown to have at least four distinct minimal sets of supporting variables with various cardinalities. Each of the corresponding functions does not have any non-essential prime implicants, and hence each enjoys the desirable feature of having a single IDF that is both a unique minimal sum and the complete sum. Moreover, each of them is unate as it is expressible in terms of un-complemented literals only. Political scientists are invited to investigate the meanings of the (so far) abstract formulas we obtained, and to devise some context-specific tool to assess and compare them.

Behaviour examples for synthesizing automaton models by temporal formulas

The paper deals with researching and developing the methods that make it possible to account behaviour examples when synthesizing automaton models by temporal formulas. Definitions of the terms and concepts used in work are given; the problem of synthesizing automaton systems according to the specification in the form of temporal formulas and behaviour examples is formulated; a promising algorithm for reducing the problem of synthesizing automaton systems to the Boolean formula satisfiability problem is described; an analysis of the domain and other approaches is carried out. New methods of taking into account behaviour examples in the synthesis of automaton systems according to a specification given in the form of temporal formulas are proposed. Algorithms for constructing graphs of scripts and methods for dividing graphs into clusters are described; they are designed to increase the efficiency of representing behaviour examples used for coding the behaviour examples in the form of Boolean formulas. An experimental study of the proposed methods of accounting for behaviour examples and basic approaches to the presentation of behaviour examples is carried out. The experimental results showed the superiority of the newly developed methods regarding the presentation of scripts in the form of temporal formulas. In summary, the main conclusions of the work carried out are presented.

Exploiting Database Management Systems and Treewidth for Counting

Bounded treewidth is one of the most cited combinatorial invariants in the literature. It was also applied for solving several counting problems efficiently. A canonical counting problem is #Sat, which asks to count the satisfying assignments of a Boolean formula. Recent work shows that benchmarking instances for #Sat often have reasonably small treewidth. This paper deals with counting problems for instances of small treewidth. We introduce a general framework to solve counting questions based on state-of-the-art database management systems (DBMSs). Our framework takes explicitly advantage of small treewidth by solving instances using dynamic programming (DP) on tree decompositions (TD). Therefore, we implement the concept of DP into a DBMS (PostgreSQL), since DP algorithms are already often given in terms of table manipulations in theory. This allows for elegant specifications of DP algorithms and the use of SQL to manipulate records and tables, which gives us a natural approach to bring DP algorithms into practice. To the best of our knowledge, we present the first approach to employ a DBMS for algorithms on TDs. A key advantage of our approach is that DBMSs naturally allow for dealing with huge tables with a limited amount of main memory (RAM).

Counting Minimal Unsatisfiable Subsets

Given an unsatisfiable Boolean formula F in CNF, an unsatisfiable subset of clauses U of F is called Minimal Unsatisfiable Subset (MUS) if every proper subset of U is satisfiable. Since MUSes serve as explanations for the unsatisfiability of F, MUSes find applications in a wide variety of domains. The availability of efficient SAT solvers has aided the development of scalable techniques for finding and enumerating MUSes in the past two decades. Building on the recent developments in the design of scalable model counting techniques for SAT, Bendík and Meel initiated the study of MUS counting techniques. They succeeded in designing the first approximate MUS counter, $$\mathsf {AMUSIC}$$ AMUSIC , that does not rely on exhaustive MUS enumeration. $$\mathsf {AMUSIC}$$ AMUSIC , however, suffers from two shortcomings: the lack of exact estimates and limited scalability due to its reliance on 3-QBF solvers.In this work, we address the two shortcomings of $$\mathsf {AMUSIC}$$ AMUSIC by designing the first exact MUS counter, $$\mathsf {CountMUST}$$ CountMUST , that does not rely on exhaustive enumeration. $$\mathsf {CountMUST}$$ CountMUST circumvents the need for 3-QBF solvers by reducing the problem of MUS counting to projected model counting. While projected model counting is #NP-hard, the past few years have witnessed the development of scalable projected model counters. An extensive empirical evaluation demonstrates that $$\mathsf {CountMUST}$$ CountMUST successfully returns MUS count for 1500 instances while $$\mathsf {AMUSIC}$$ AMUSIC and enumeration-based techniques could only handle up to 833 instances.