A method for counting models on grid Boolean formulas1

We present a novel algorithm based on combinatorial operations on lists for computing the number of models on two conjunctive normal form Boolean formulas whose restricted graph is represented by a grid graph Gm,n. We show that our algorithm is correct and its time complexity is O ( t · 1 . 618 t + 2 + t · 1 . 618 2 t + 4 ) , where t = n · m is the total number of vertices in the graph. For this class of formulas, we show that our proposal improves the asymptotic behavior of the time-complexity with respect of the current leader algorithm for counting models on two conjunctive form formulas of this kind.

Embedding and extraction of knowledge in tree ensemble classifiers

The embedding and extraction of knowledge is a recent trend in machine learning applications, e.g., to supplement training datasets that are small. Whilst, as the increasing use of machine learning models in security-critical applications, the embedding and extraction of malicious knowledge are equivalent to the notorious backdoor attack and defence, respectively. This paper studies the embedding and extraction of knowledge in tree ensemble classifiers, and focuses on knowledge expressible with a generic form of Boolean formulas, e.g., point-wise robustness and backdoor attacks. For the embedding, it is required to be preservative (the original performance of the classifier is preserved), verifiable (the knowledge can be attested), and stealthy (the embedding cannot be easily detected). To facilitate this, we propose two novel, and effective embedding algorithms, one of which is for black-box settings and the other for white-box settings. The embedding can be done in PTIME. Beyond the embedding, we develop an algorithm to extract the embedded knowledge, by reducing the problem to be solvable with an SMT (satisfiability modulo theories) solver. While this novel algorithm can successfully extract knowledge, the reduction leads to an NP computation. Therefore, if applying embedding as backdoor attacks and extraction as defence, our results suggest a complexity gap (P vs. NP) between the attack and defence when working with tree ensemble classifiers. We apply our algorithms to a diverse set of datasets to validate our conclusion extensively.

On Quantifying Literals in Boolean Logic and its Applications to Explainable AI

Quantified Boolean logic results from adding operators to Boolean logic for existentially and universally quantifying variables. This extends the reach of Boolean logic by enabling a variety of applications that have been explored over the decades. The existential quantification of literals (variable states) and its applications have also been studied in the literature. In this paper, we complement this by introducing and studying universal literal quantification and its applications, particularly to explainable AI. We also provide a novel semantics for quantification, discuss the interplay between variable/literal and existential/universal quantification, and identify some classes of Boolean formulas and circuits on which quantification can be done efficiently. Literal quantification is more fine-grained than variable quantification as the latter can be defined in terms of the former, leading to a refinement of quantified Boolean logic with literal quantification as its primitive.

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.

Planning with Incomplete Information in Quantified Answer Set Programming

We present a general approach to planning with incomplete information in Answer Set Programming (ASP). More precisely, we consider the problems of conformant and conditional planning with sensing actions and assumptions. We represent planning problems using a simple formalism where logic programs describe the transition function between states, the initial states and the goal states. For solving planning problems, we use Quantified Answer Set Programming (QASP), an extension of ASP with existential and universal quantifiers over atoms that is analogous to Quantified Boolean Formulas (QBFs). We define the language of quantified logic programs and use it to represent the solutions different variants of conformant and conditional planning. On the practical side, we present a translation-based QASP solver that converts quantified logic programs into QBFs and then executes a QBF solver, and we evaluate experimentally the approach on conformant and conditional planning benchmarks.

Boolean Network Learning in Vector Spaces for Genome-wide Network Analysis

Boolean networks (BNs) are one of the standard tools for modeling gene regulatory networks in biology but their learning has been limited to small networks due to computational difficulty. Aiming at unprecedented scalability, we focus on a subclass of BNs called AND/OR Boolean networks where Boolean formulas are restricted to a conjunction or a disjunction of literals. We represent an AND/OR BN with N nodes by an N x 2N binary matrix Q paired with an N dimensional integer vector theta called a threshold vector, a state of the BN by an N dimensional binary state vector s and a state transition by matrix operations on Q, theta and s. Given a list of state transitions S = s_0...s_L, we learn Q and theta in a continuous space by minimizing a cost function J(Q*,theta,S) w.r.t. a real number matrix Q* and theta while thresholding Q* into a binary matrix Q using theta so that Q represents an AND/OR BN realizing the target state transitions S. We conducted experiments with artificial and real data sets to check scalability and accuracy of our learning algorithm. First we randomly generated AND/OR BNs up to N=5,000 nodes and empirically confirmed O(N^2) learning time behavior using them. We also observed 99.8% bit-by-bit prediction accuracy (prediction accuracy = 1 - test error) with state transition data generated by AND/OR BNs. For real data, we learned genome-wide AND/OR BNs with 10,928 nodes for budding yeast from transcription profiling data sets, each containing 10,928 mRNAs and 40 transitions and achieved for instance 84.3% prediction accuracy and successfully extracted more than 6,000 small AND/ORs whose average prediction accuracy reaches much higher 94.9%.

Two SAT solvers for solving quantified Boolean formulas with an arbitrary number of quantifier alternations

In recent years, expansion-based techniques have been shown to be very powerful in theory and practice for solving quantified Boolean formulas (QBF), the extension of propositional formulas with existential and universal quantifiers over Boolean variables. Such approaches partially expand one type of variable (either existential or universal) for obtaining a propositional abstraction of the QBF. If this formula is false, the truth value of the QBF is decided, otherwise further refinement steps are necessary. Classically, expansion-based solvers process the given formula quantifier-block wise and use one SAT solver per quantifier block. In this paper, we present a novel algorithm for expansion-based QBF solving that deals with the whole quantifier prefix at once. Hence recursive applications of the expansion principle are avoided and only two incremental SAT solvers are required. While our algorithm is naturally based on the $$\forall $$ ∀ Exp+Res calculus that is the formal foundation of expansion-based solving, it is conceptually simpler than present recursive approaches. Experiments indicate that the performance of our simple approach is comparable with the state of the art of QBF solving, especially in combination with other solving techniques.

Computational Complexity and ILP Models for Pattern Problems in the Logical Analysis of Data

Logical Analysis of Data is a procedure aimed at identifying relevant features in data sets with both positive and negative samples. The goal is to build Boolean formulas, represented by strings over {0,1,-} called patterns, which can be used to classify new samples as positive or negative. Since a data set can be explained in alternative ways, many computational problems arise related to the choice of a particular set of patterns. In this paper we study the computational complexity of several of these pattern problems (showing that they are, in general, computationally hard) and we propose some integer programming models that appear to be effective. We describe an ILP model for finding the minimum-size set of patterns explaining a given set of samples and another one for the problem of determining whether two sets of patterns are equivalent, i.e., they explain exactly the same samples. We base our first model on a polynomial procedure that computes all patterns compatible with a given set of samples. Computational experiments substantiate the effectiveness of our models on fairly large instances. Finally, we conjecture that the existence of an effective ILP model for finding a minimum-size set of patterns equivalent to a given set of patterns is unlikely, due to the problem being NP-hard and co-NP-hard at the same time.

Program Synthesis as Dependency Quantified Formula Modulo Theory

Given a specification φ(X, Y ) over inputs X and output Y and defined over a background theory T, the problem of program synthesis is to design a program f such that Y = f (X), satisfies the specification φ. Over the past decade, syntax-guided synthesis (SyGuS) has emerged as a dominant approach to program synthesis where in addition to the specification φ, the end-user also specifies a grammar L to aid the underlying synthesis engine. This paper investigates the feasibility of synthesis techniques without grammar, a sub-class defined as T constrained synthesis. We show that T-constrained synthesis can be reduced to DQF(T),i.e., to the problem of finding a witness of a dependency quantified formula modulo theory. When the underlying theory is the theory of bitvectors, the corresponding DQF problem can be further reduced to Dependency Quantified Boolean Formulas (DQBF). We rely on the progress in DQBF solving to design DQBF-based synthesizers that outperform the domain-specific program synthesis techniques; thereby positioning DQBF as a core representation language for program synthesis. Our empirical analysis shows that T-constrained synthesis can achieve significantly better performance than syntax-guided approaches. Furthermore, the general-purpose DQBF solvers perform on par with domain-specific synthesis techniques.

Constraint Satisfaction Problems and Their Reduction to Directed Graphs

Constraint satisfaction problems present a general framework for studying a large class of algorithmic problems such as satisfaction of Boolean formulas, solving systems of equations over finite fields, graph colourings, as well as various applied problems in artificial intelligence (scheduling, allocation of cell phone frequencies, among others.) CSP (Constraint Satisfaction Problems) bring together graph theory, complexity theory and universal algebra. It is a well known result, due to Feder and Vardi, that any constraint satisfaction problem over a finite relational structure can be reduced to the homomorphism problem for a finite oriented graph. Until recently, it was not known whether this reduction preserves the type of the algorithm which solves the original constraint satisfaction problem, so that the same algorithm solves the corresponding digraph homomorphism problem. We look at how a recent construction due to Bulin, Deli´c, Jackson, and Niven can be used to show that the polynomial solvability of a constraint satisfaction problem using Datalog, a programming language which is a weaker version of Prolog, translates from arbitrary relational structures to digraphs.