Search

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.

In this paper, we discuss the copy complexity of Horn formulas with respect to unit resolution. A Horn formula is a boolean formula in conjunctive normal form (CNF) with at most one positive literal per clause. Horn formulas find applications in a number of domains, such as program verification (abstract interpretation) and logic programming (answer set programming). Quantified Horn clauses are used extensively in temporal verification of universal properties. Resolution is one of the oldest proof systems (refutation systems) for the boolean satisfiability problem (SAT), when the input is presented in conjunctive normal form (CNF). It is both sound and complete, although inefficient, when compared to other stronger proof systems for boolean formulas. Despite its inefficiency, the simple nature of resolution makes it an integral part of several theorem provers. Unit resolution is a restricted form of resolution in which each resolution step needs to use a clause with only one literal (unit literal clause). While not complete for general CNF formulas, unit resolution is complete for Horn formulas. Read-once resolution is a form of resolution in which each clause (input or derived) may be used in at most one resolution step. As with unit resolution, read-once resolution is incomplete in general and complete for Horn clauses. This paper focuses on a combination of unit resolution and read-once resolution called unit read-once resolution. Unit read-once resolution is incomplete for Horn clauses. In this paper, we study the copy complexity problem in Horn formulas with respect to unit read-once resolution. Briefly, the copy complexity of a formula with respect to unit read-once resolution, is the smallest number k, such that replicating each clause k times guarantees the existence of a unit read-once resolution refutation (UROR). This paper focuses on two problems related to the copy complexity of Horn formulas with respect to unit read-once resolution. We first relate the copy complexity of Horn formulas with respect to unit read-once resolution to the copy complexity of the corresponding Horn constraint system with respect to the addition rule. We also examine a form of copy complexity in which we permit replication of derived clauses, in addition to the input clauses. Finally, we provide a polynomial time algorithm for the problem of checking if a 2-CNF formula has a UROR.

In this paper, we discuss algorithms for the problem of finding read-once resolution refutations of unsatisfiable 2CNF formulas within the resolution refutation system. Broadly, a read-once resolution refutation is one in which each constraint (input or derived) is used at most once. Read-once resolution refutations have been widely studied in the literature for a number of constraint system-refutation system pairs. For instance, read-once resolution has been analyzed for boolean formulas in conjunctive normal form (CNF) and read-once cutting planes have been analyzed for polyhedral systems. By definition, read-once refutations are compact, and hence valuable in applications that place a premium on visualization. The satisfiability problem (SAT) is concerned with finding a satisfying assignment for a boolean formula in CNF. While SAT is NP-complete in general, there exist some interesting subclasses of CNF formulas, for which it is decidable in polynomial time. One such subclass is the class of 2CNF formulas, i.e., CNF formulas in which each clause has at most two literals. The existence of efficient algorithms for satisfiability checking in 2CNF formulas (2SAT), makes this class useful from the perspective of modeling selected logic programs. The work in this paper is concerned with the read-once refutability problem (under resolution) in this subclass. Although 2SAT is decidable in polynomial time, the problem of finding a read-once resolution refutation of an unsatisfiable 2CNF formula is NP-complete. We design non-trivial, parameterized and exact exponential algorithms for this problem. Additionally, we study the computational complexity of finding a shortest read-once resolution refutation of a 2CNF formula.

The study of alternation in two-way finite automata ( 2 fa s) has been quite non-systematic. Since the 1970's, various authors with a variety of motivations have studied 2 fa s with various types of alternation and a variety of names, creating a fairly long list of sporadic contributions with little internal consistency. This article attempts to organize the subject into a single unifying framework. We start with a detailed account of all contributions to date, that reveals the large variety of approaches and the lack of consistency between them. We then identify and name four types of automata that these contributions have really studied over the years: general two-way Boolean finite automata ( 2 b fa s); monotone 2 b fa s; basic 2 b fa s; and (monotone basic, or) alternating 2 b fa s ( 2 a fa s). Next, we identify four different ways by which authors have described how such automata compute, each offering a distinct view onto their operation: the circuit view, where computation is modelled by a circuit of Boolean gates; the formula view, where computation is modelled by a Boolean formula over configuration-variables; the run view, where decisions are determined by the existence of appropriate trees of configuration-goal pairs, called “runs”; and the (most classic) tree view, where computation is modelled by a tree of configurations. After carefully defining each 2 b fa type and each view, we prove the following. First, that within each type, every two of the four views are equivalent to each other, in the strong sense that each of them closely mimics the other at every step of the computation. Second, that not all types of 2 b fa s are equivalent: although general 2 b fa s are as powerful as monotone 2 b fa s, and basic 2 b fa s are as powerful as 2 a fa s (up to polynomial differences in the number of states), general 2 b fa s may need exponentially fewer states than 2 a fa s.

Boolean formulas often have what are known as hidden structures. We study the complexity of whether such structures (of certain sizes) exist in a formula, the complexity of getting one’s hands on the structure’s information, and whether even when in hand the information can be efficiently exploited. In particular, backdoors and backbones of Boolean formulas are important hidden structural properties. A natural goal, already in part realized, is that solver algorithms seek better performance by exploiting these structures. However, the present paper is not intended to improve the performance of SAT solvers, but rather is a cautionary tale. The theme of this paper is that there is a potential chasm between the existence of such structures in the Boolean formula and being able to effectively exploit them. This does not mean that these structures are not useful to solvers. It does mean that one must be very careful not to assume that it is computationally easy to go from the existence of information to being able to get one’s hands on it and/or being able to exploit it. We construct backdoor- and backbone-based cases where, if $$\mathrm {P}\ne \mathrm {NP}$$ , such assumptions fail. For example, if $$\mathrm {P}\ne \mathrm {NP}$$ , then (a) there are easily recognizable families of Boolean formulas with strong backdoors that are easy to find, yet for which it is hard to determine whether the formulas are satisfiable, and (b) there are easily recognizable sets of Boolean formulas for which it is hard to determine whether they have a large backbone.

Bounded treewidth is one of the most cited combinatorial invariants, which was applied in the literature 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 (DBMS). 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 DBMS naturally allow to deal with huge tables with a limited amount of main memory (RAM), parallelization, as well as suspending computation., Comment: Under consideration in Theory and Practice of Logic Programming (TPLP)

Bounded synthesis generates a state machine satisfying given temporal specification in linear temporal logic (LTL) while bounding the number of states of the target solution. Bounded synthesis methods currently do not support finite-length behavior examples, which are often helpful when formulating the specification of the desired state machine. In this work we show how to incorporate behavior examples into bounded synthesis methods and exemplify the approach by presenting BeBoSy (Behavior Examples meet BoSy), an extension of the bounded synthesis tool BoSy based on reductions to Boolean satisfiability (SAT) and Quantified Boolean formula satisfiability (QSAT) problems. The proposed approach is to augment the encodings used in BoSy with additional constraints that ensure the compliance of the generated state machine with the given behavior examples. Experiments with openly available data from the annual reactive synthesis competition SYNTCOMP augmented with random behavior examples show that the efficiency of the proposed approach is superior to both BoSy (with naïve representation of behavior examples with LTL formulas) and a state-of-the-art counterexample-guided approach EFSM-tools.

Subject of Research. The paper considers a method for solution of the nondeterministic polynomial hard problem (NP-hard problem) of a minimal Boolean formula synthesis from a given truth table. The solution of this problem is proposed based on its reduction to the Boolean satisfiability problem (SAT). The issues of efficient and convenient software implementation are discussed for reducing nondeterministic polynomial hard problems to the satisfiability problem. Method. For a minimal Boolean formula synthesis, the constraint programming approach was used: a SAT-formula was created for a given truth table, satisfiable if and only if, there exists a Boolean formula of a given size that satisfies the given truth table. The developed method accent is the application of incremental satisfiability problem solvers. Main Results. A method is proposed for synthesis of a Boolean formula, minimal with respect to the number of operators and terminals, for a given truth table. The method is based on reducing to satisfiability problem and provides the usage of incremental satisfiability problem solvers. The kotlin-satlib framework is developed with the possibility to use the Kotlin and Java languages effectively and conveniently for the software implementation of reducing various nondeterministic polynomial-time hard problems to satisfiability problem. Native interaction with satisfiability problem solvers by Java Native Interface (JNI) technology is used. The proposed method for the minimal Boolean formula synthesis is implemented in the Kotlin programming language using the developed kotlin-satlib framework. Practical Relevance. An experimental study on the example of minimal Boolean formula synthesis has shown that the usage of incremental satisfiability problem solvers for nondeterministic polynomial hard problems is reasonable, since it reduces the total solving time in comparison with the non-incremental approach application.

In reaction systems, preimages and nth ancestors are sets of reactants leading to the production of a target set of products in either 1 or n steps, respectively. Many computational problems on preimages and ancestors, such as finding all minimum-cardinality nth ancestors, computing their size or counting them, are intractable. In this paper, we characterize all nth ancestors using a Boolean formula that can be computed in polynomial time. Once simplified, this formula can be exploited to easily solve all preimage and ancestor problems. This allows us to directly relate the difficulty of ancestor problems to the cost of the simplification so that new insights into computational complexity investigations can be achieved. In particular, we focus on two problems: (i) deciding whether a preimage/nth ancestor exists and (ii) finding a preimage/nth ancestor of minimal size. Our approach is constructive, it aims at finding classes of reactions systems for which the ancestor problems can be solved in polynomial time, in exact or approximate way.

Similar to the satisfiability (SAT) problem, which can be seen to be the archetypical problem for NP, the quantified Boolean formula problem (QBF) is the archetypical problem for PSPACE. Recently, Atserias and Oliva (2014) showed that, unlike for SAT, many of the well-known decompositional parameters (such as treewidth and pathwidth) do not allow efficient algorithms for QBF. The main reason for this seems to be the lack of awareness of these parameters towards the dependencies between variables of a QBF formula. In this paper we extend the ordinary pathwidth to the QBF-setting by introducing prefix pathwidth, which takes into account the dependencies between variables in a QBF, and show that it leads to an efficient algorithm for QBF. We hope that our approach will help to initiate the study of novel tailor-made decompositional parameters for QBF and thereby help to lift the success of these decompositional parameters from SAT to QBF.

In a work presented by Gazdag and Kolonits from 2013, it was shown that SAT can be solved in linear time in the number of variables using the clause completion method on a non-distributed P system with active membranes. A distributed P system with active membranes using the clause completion method solving SAT (denoted as k-$$\varDelta (n)$$) is presented in this work. k-$$\varDelta (n)$$ is a weak uniform solution to SAT that runs in linear time with respect only to the number of variables, n, of the Boolean formula $$\varphi$$. For the 2-component solution, 2-$$\varDelta (n)$$, we show that the communication cost is constant. But, increasing the number of components in k-$$\varDelta (n)$$, $$k \ge 3$$, would make the communication cost dependent on not just the number of components and the number of variables, but as well as the number of satisfying assignments to $$\varphi$$. We report that an exponential amount of resources (in terms of alphabet size and rules) are necessary to construct k-$$\varDelta (n)$$ solving SAT to obtain these reasonable communication costs.

The Lovasz Local Lemma (LLL) is a probabilistic tool which has been used to show the existence of a variety of combinatorial structures with good "local" properties. The "LLL-distribution" can be used to show that the resulting structures have good global properties in expectation. The simplest, variable-based setting of the LLL was covered by the seminal algorithm of Moser & Tardos (2010). This has since been extended to other probability spaces including random permutations. One can similarly define an "MT-distribution" for these algorithms, that is, the distribution of the configuration they produce. Haeupler et al. (2011) showed bounds on the MT-distribution which essentially match the LLL-distribution for the variable-assignment setting; Harris & Srinivasan showed similar results for the permutation setting. In this work, we show new bounds on the MT-distribution which are significantly stronger than those known to hold for the LLL-distribution. In the variable-assignment setting, we show a tighter bound on the probability of a disjunctive event or singleton event. As a consequence, in $k$-SAT instances with bounded variable occurrence, the MT-distribution satisfies an $\epsilon$-approximate independence condition asymptotically stronger than the LLL-distribution. We use this to show a nearly tight bound on the minimum implicate size of a CNF boolean formula. Another noteworthy application is constructing independent transversals which avoid a given subset of vertices; this provides a constructive analogue to a result of Rabern (2014). In the permutation LLL setting, we show a new type of bound which is similar to the cluster-expansion LLL criterion of Bissacot et al. (2011), but is stronger and takes advantage of the extra structure in permutations. We illustrate with improved bounds on weighted Latin transversals and partial Latin transversals.

This paper considers the path planning problem in multirobot systems with an unknown environment. The robots’ mission is given as a Boolean formula on the final states. We assume that the robots have partial knowledge of the environment and they are able to estimate the environment using a recursive Bayes estimator. Furthermore, they communicate between them if they are at a distance smaller than a given threshold in order to improve their own estimation. Each robot will solve an optimization problem based on the Petri net model of the environment and it will move accordingly. We provide an algorithm to be iterated by each robot and we evaluate the results by simulation.

Stephen Cook and Leonard Levin independently proved that there are problems called NonPolynomial-complete (NP-complete) problems. The theorem is today referred to as Cook-Levin theorem. The theorem states that Boolean satisfiability problem is NP-complete. That is to say, any problem in NP can be reduced in polynomial time by a deterministic Turing machine to the problem of determining whether a Boolean formula is satisfiable. Therefore, if there exists a deterministic polynomial time algorithm for solving a Boolean satisfiability, then there exists a deterministic polynomial time algorithm for solving all problems in NP. Thus Cook-Levin theorem provides a proof that the problem of SAT is NP-complete via reduction technique. In this paper, we revisit Cook-Levin Theorem but using a completely different approach to prove the theorem. The approach used combines the concepts of NP-completeness and circuit-SAT. Using this technique, we showed that Boolean satisfiability problem is NP-complete through the reduction of polynomial time algorithms for NP-completeness and circuit-SAT.

A constructive logical method for the synthesis of the characteristic matrix of a linear binary dynamical system with a given set of one-point attractors and one-step dynamics of reaching this set from any state is proposed. The problem conditions are written as a quantified Boolean formula with subsequent verification of its truth using the QSAT solver. This solver provide the values of the elements of the required matrix as a certificate. The proposed method implementation is performed using automation tools for constructing and executing composite services in an applied microservices package for solving problems of qualitative research of binary dynamic systems. These tools provide cloud services for getting a quantified Boolean formula in QDIMACS format, verifying its truth, getting a constructive solution to the considered problem, and supporting synchronization of cloud and local data in a hybrid cloud infrastructure using Dew Computing.

This paper considers the path planning problem of a multi-robot system in an uncertain environment with high-level specifications. The specification that the team of robots has to satisfy is given in form of a Boolean formula over the set of regions of interest. Opposed to the majority of solutions for this type of problem, in this paper we consider that the robots do not know with precision the location of these regions, having a probability distribution over the labeling instead. We present a planning algorithm that leverages the properties of Petri net models to efficiently solve an optimization problem that maximizes the probability of satisfying the formula. In addition, the solution of the optimizer avoids regions with high probability of being obstacles and tries to reduce the chances of collisions of the team. We also discuss the application of the algorithm in a distributed scenario, where the robots have different probability distributions and even outdated locations of the rest of the team. Simulations are presented to validate the proposed methodology.

Alloy is a declarative modeling language based on a first-order relational logic. Its constraint-based analysis has enabled a wide range of applications in software engineering, including configuration synthesis, bug finding, test-case generation, and security analysis. Certain types of analysis tasks in these domains involve finding an optimal solution. For example, in a network configuration problem, instead of finding any valid configuration, it may be desirable to find one that is most permissive (i.e., it permits a maximum number of packets). Due to its dependence on SAT, however, Alloy cannot be used to specify and analyze these types of problems. We propose AlloyMax, an extension of Alloy with a capability to express and analyze problems with optimal solutions. AlloyMax introduces (1) a small addition of language constructs that can be used to specify a wide range of problems that involve optimality and (2) a new analysis engine that leverages a Maximum Satisfiability (MaxSAT) solver to generate optimal solutions. To enable this new type of analysis, we show how a specification in a first-order relational logic can be translated into an input format of MaxSAT solvers—namely, a Boolean formula in weighted conjunctive normal form (WCNF). We demonstrate the applicability and scalability of AlloyMax on a benchmark of problems. To our knowledge, AlloyMax is the first approach to enable analysis with optimality in a relational modeling language, and we believe that AlloyMax has the potential to bring a wide range of new applications to Alloy.

Vesicle traffic systems (VTSs) transport cargo among the intracellular compartments of eukaryotic cells. The compartments are viewed as nodes that are labeled by their chemical identity and the transport vesicles are similarly viewed as labeled edges between the nodes. Several interesting questions about VTSs translate to combinatorial search and synthesis problems. We present novel encodings for the problems based on Boolean satisfiability (SAT), satisfiability modulo theories and quantified Boolean formula of the properties over vesicle traffic systems. We have implemented the presented encodings in a tool that searches for the networks that satisfy properties related to transport consistency conditions using these solvers. In our numerical experiments, we show that our tool can search for networks of sizes that are relevant to real cellular systems. Our work illustrates the potential of novel biological applications of SAT solving technology.

Denote by SWE the satisfiability problem for word equations. Consider the problem of computability of the maximal exponent of periodicity for word equations MaxExpProblem ( e , k ) in which given positive integer k and a word equation e one is to check whether maximal exponent of periodicity of a solution of a word equation is at least k. We present both a deterministic polynomial time reduction of the MaxExpProblem ( e , k ) problem to the satisfiability problem for word equations and a deterministic polynomial time reduction in the opposite direction. Consequently, if the satisfiability problem is in NP then the other problem is NP-complete. As a simple consequence we get that computation of maximal exponent of periodicity of a solution set for a word equation is in P SWE (SWE is an oracle) and, consequently in PSPACE. Let ϕ be an existential boolean formula built on word equations expressing a relation on words by means of its unknowns. Consider the problem of checking the maximal exponent of periodicity of a component of a relation CMaxExpProblem ( ϕ , k ) in which given positive integer k and a formula ϕ one is to check whether maximal exponent of periodicity of a component of the relation is at least k. We give nondeterministic polynomial time reduction of the described above CMaxExpProblem ( ϕ , k ) problem to the satisfiability problem for word equations and deterministic polynomial time reduction in the other direction. Consequently, if the satisfiability problem is in NP then the other problem is NP-complete. Denote by SAT ( WE ) the satisfiability problem of closed existential formula built on word equations. As a simple consequence of our considerations we get that computation of maximal exponent of periodicity of a component of expressible relation is in P SAT ( WE ) ( SAT ( WE ) is an oracle), and, consequently, in PSPACE. Another consequence of that is that if SWE is in NP, then the computability problem is in P N P . The above results hold also for semigroups with involution. If the expressible relation is defined by a formula using word equations and regular constraints we prove that the problem is PSPACE-complete. The same holds for free semigroups with involution and free groups.

Abstract Dialectical Frameworks ( adf s) are generalizations of Dung's abstract argumentation frameworks ( af s) where each argument has an associated acceptance condition expressed by a boolean formula. The resulting extension is robust enough not only to model the attack relation original to af s, but also others types of dependencies and interactions between arguments. A recent development in adf s proposed an alternative formalization involving three-valued acceptance conditions, connecting the original definitions of adf s to the concept of three-valued argument labellings, a core concept in computational argumentation literature. In this paper, we revise some of the main semantics defined under this three-valued approach and prove our definitions hold equivalence to well-known semantics of af s.

Given a Boolean formula φ, the problem of model counting, also referred to as #SAT is to compute the number of solutions of φ. Model counting is a fundamental problem in artificial intelligence with a wide range of applications including probabilistic reasoning, decision making under uncertainty, quantified information flow, and the like. Motivated by the success of SAT solvers, there has been surge of interest in the design of hashing-based techniques for approximate model counting for the past decade. We profiled the state of the art approximate model counter ApproxMC2 and observed that over 99.99% of time is consumed by the underlying SAT solver, CryptoMiniSat. This observation motivated us to ask: Can we design an efficient underlying CNF-XOR SAT solver that can take advantage of the structure of hashing-based algorithms and would this lead to an efficient approximate model counter? The primary contribution of this paper is an affirmative answer to the above question. We present a novel architecture, called BIRD, to handle CNF-XOR formulas arising from hashingbased techniques. The resulting hashing-based approximate model counter, called ApproxMC3, employs the BIRD framework in its underlying SAT solver, CryptoMiniSat. To the best of our knowledge, we conducted the most comprehensive study of evaluation performance of counting algorithms involving 1896 benchmarks with computational effort totaling 86400 computational hours. Our experimental evaluation demonstrates significant runtime performance improvement for ApproxMC3 over ApproxMC2. In particular, we solve 648 benchmarks more than ApproxMC2, the state of the art approximate model counter and for all the formulas where both ApproxMC2 and ApproxMC3 did not timeout and took more than 1 seconds, the mean speedup is 284.40 – more than two orders of magnitude. Erratum: This research is supported in part by the National Research Foundation Singapore under its AI Singapore Programme (Award Number: [AISG-RP-2018-005])

Fault tree analysis is still widely practiced in high-hazard industries. We propose in this article an algorithm for the reduction of fault tree expressions that are generated from automata representations of failure behaviors. Automata formalisms are increasingly being used to describe systems exhibiting sequence-dependent failures—i.e., the overall outcome like a total failure of the system can depend on the order in which events occur. A set of paths leading to a safety-relevant state is encoded as a standard sum of product canonical form, and without any loss of the significance of the sequencing of events. That is, the corresponding fault tree expression is basically a Boolean formula which is extended with the necessary temporal features (event occurrence priority). Such expressions can then be reduced into minimal canonical forms by using the Boolean methods together with the required temporal logic calculus. Since minimal failure sequences can be determined from the obtained reduced models, the proposed approach can improve the analysis of the dynamic effects of the sequencing of faults and propagated errors in such models. As a consequence, it can have a positive impact on the design of failure prevention measures. A fault tolerant example system exhibiting dynamic behavior is used to highlight the benefits of the approach.

International audience; We investigate the complexity of four decision problems dealing with the uniqueness of a solution in a graph: “Uniqueness of an r-Locating–Dominating Code with bounded size” (U-LDCr), “Uniqueness of an Optimal r-Locating–Dominating Code” (U-OLDCr), “Uniqueness of an r-Identifying Code with bounded size” (U-IdCr), “Uniqueness of an Optimal r-Identifying Code” (U-OIdCr), for any fixed integer r ≥ 1In particular, we describe a polynomial reduction from “Unique Satisfiability of a Boolean formula” (U-SAT) to U-OLDCr, and from U-SAT to U-OIdCr; for U-LDCr and U-IdCr, we can do even better and prove that their complexity is the same as that of U-SAT, up to polynomials. Consequently, all these problems are NP-hard, and U-LDCr and U-IdCr belong to the class DP.

This research revisits the fundamental problem of processing privacy-preserving Boolean queries over outsourced databases on untrusted public clouds. Much current searchable encryption (SE) schemes try to seek an appropriate trade-off between security and efficiency, yet most of them suffer from an unacceptable query leakage due to their conjunctive/disjunctive terms that are processed individually. We show, however, this trade-off still can be deeply optimized for more security. We consider a Boolean formula as a set of deterministic finite automatons (DFAs) and propose a novel approach to running an encrypted DFA, which can be effectively and efficiently processed by the cloud. We give three constructions for conjunctive, disjunctive, and Boolean queries, respectively. Their notable advantages are single-round, highly-efficient, adaptively-secure, and leakage-minimized. A lot of experiments are made to evaluate overall efficiency. Testing results show that the schemes achieve enhanced security almost without sacrificing anything of search efficiency.

For sequential circuits, it is well known that the sets of reachable states may be much smaller than the entire state space, and computing the supersets of reachable states is practically useful due to the less computational complexity than the exact set of the reachable states. Inductive invariant is the one of the methods to compute such supersets. We first show a way to prove the property of the sequential circuits with inductive invariants. For inductive invariants, it is important to select the subset of flipflops in order to find a small and/or useful superset of reachable states or prove the property. Unknown value X based analysis is used to find the subset of flipflops. In some HWMCC2017 benchmark circuits, the proposed method can find the subset of flipflops to prove the correctness of the property. The calculation of inductive invariants is formulated with Quantified Boolean Formula. The QBF problem can be solved by repeatedly applying SAT solvers. We also show a way to reduce the number of variables in QBF problems. In the method, we start with smaller inputs LUT and gradually increase the number of inputs in order to reduce variables. This method has reduced calculation time by up to around 80% when solving large QBF problem.

Boolean satisfiability (SAT) has played a key role in diverse areas spanning planning, inferencing, data mining, testing and optimization. Apart from the classical problem of checking Boolean satisfiability, generating random satisfying assignments has attracted significant theoretical and practical interests over the years. For practical applications, a large number of satisfying assignments for a given Boolean formula are needed, the generation of which turns out to be a hard problem in both theory and practice. In this work, we propose a novel approach to derive a large set of satisfying assignments from a given one in an efficient way. Our approach is orthogonal to the previous techniques for generating satisfying assignments and could be integrated into the existing SAT samplers. We implement our approach as an open-source tool ESampler and conduct extensive experiments on real-world benchmarks. Experimental results show that ESampler performs better than three state-of-the-art samplers on a large portion of the benchmarks, and is at least comparable on the others, showcasing the efficacy of our approach.

Recent developments in the propositional representation of achievement games have renewed interest in applying the latest advances in Quantified Boolean Formula technologies to solving these games. However, the number of quantifier alternations necessary to explore the solution space still impairs and limits the applicability of these methods. In this paper, we show that one can encode blocking strategies for the second player and express the last moves of the play with a single string of existential quantifiers, instead of the usual alternations of universal and existential quantifiers. We experimentally show that our method improves the performance of state-of-the-art Quantified Boolean Formula solvers on Harary’s Tic-Tac-Toe, a well-known achievement game.

Given an unsatisfiable Boolean formulaFin CNF, an unsatisfiable subset of clauses U ofFis called Minimal Unsatisfiable Subset (MUS) if every proper subset ofUis satisfiable. Since MUSes serve as explanations for the unsatisfiability ofF, 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}$$AMUSICby designing the first exact MUS counter,$$\mathsf {CountMUST}$$CountMUST, that does not rely on exhaustive enumeration.$$\mathsf {CountMUST}$$CountMUSTcircumvents 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}$$CountMUSTsuccessfully returns MUS count for 1500 instances while$$\mathsf {AMUSIC}$$AMUSICand enumeration-based techniques could only handle up to 833 instances.

The analysis of input conditions that may cause a short-circuit in a logic circuit has recently become a critical issue, due to the potential presence of parasitic circuit elements after layout. This analysis is strongly related to the problem of determining paths in a graph whose edges are defined by related logic functions. Logic circuits can be modeled as a generic graph, where edges are a logic function of static input variable combinations, representing transistors that act like logic switches. The solution to this problem must address a complex SAT-problem involving an extensive inspection of all possible paths between two nodes, the power supply and ground. We describe an efficient method, based on a Quantified Boolean Formula (QBF) model, that solves this problem in an incremental way. We propose a parallel implementation for multi-core shared-memory machines. The Espresso logic minimization tool was critical to keep the size of the intermediate logic functions manageable. In order to be able to use this tool in parallel, we developed a thread-safe version of Espresso and have made it available to the community. The proposed solution was validated against a set of benchmarks that show the effectiveness of our parallel implementation, allowing to address instances of transistor-level circuits for a wide range of inputs and internal nodes efficiently.

Token swapping (TSWAP) represents a challenging problem underlying in many practical applications ranging from item relocation to quantum program compilation. In TSWAP, we are given an undirected graph with colored vertices. A colored token is placed in each vertex. A pair of tokens can be swapped between a pair of adjacent vertices. The goal is to perform a sequence of swaps so that token and vertex colors agree across the graph. The total number of swaps is usually required to be small. We study bounded sub-optimal algorithms for solving the TSWAP problem. We introduce a SAT-based algorithm based on lazy compilation of the problem to a Boolean formula and an alternative search-based algorithm using conflict based search. We analyze both algorithms experimentally on a number of benchmarks.

Boolean satisfiability is a propositional logic problem of interest in multiple fields, e.g., physics, mathematics, and computer science. Beyond a field of research, instances of the SAT problem, as it is known, require efficient solution methods in a variety of applications. It is the decision problem of determining whether a Boolean formula has a satisfying assignment, believed to require exponentially growing time for an algorithm to solve for the worst-case instances. Yet, the efficient solution of many classes of Boolean formulae eludes even the most successful algorithms, not only for the worst-case scenarios, but also for typical-case instances. Here, we introduce a memory-assisted physical system (a digital memcomputing machine) that, when its non-linear ordinary differential equations are integrated numerically, shows evidence for polynomially-bounded scalability while solving “hard” planted-solution instances of SAT, known to require exponential time to solve in the typical case for both complete and incomplete algorithms. Furthermore, we analytically demonstrate that the physical system can efficiently solve the SAT problem in continuous time, without the need to introduce chaos or an exponentially growing energy. The efficiency of the simulations is related to the collective dynamical properties of the original physical system that persist in the numerical integration to robustly guide the solution search even in the presence of numerical errors. We anticipate our results to broaden research directions in physics-inspired computing paradigms ranging from theory to application, from simulation to hardware implementation.

Boolean satisfiability logical representation is a programming paradigm that has its foundations in mathematical logic. It has been classified as an NP-complete problem that difficult practical combinatorial optimization and search problems can be easily converted into it. Random Maximum kSatisfiability (MAX-RkSAT) composed of the most consistent mapping in a Boolean formula that generates a maximum number of random satisfied clauses. Many optimization and search problems can be easily expressed by mapping the problem into a Hopfield neural network (HNN) to minimize the optimal configuration of the corresponding Lyapunov energy function. In this paper, a hybrid computational model hs been proposed that incorporates the Random Maximum kSatisfiability (MAX-RkSAT) into the Hopfield neural network (HNN) for optimal Random Maximum kSatisfiability representation (HNN-MAX-RkSAT). Hopfield neural network learning will be integrated with the random maximum satisfiability to enhance the correct neural state of the network model representation. The computer simulation using C++ has been used to demonstrate the ability of MAX-RkSAT to be embedded optimally in Hopfield neural network to serve as Neuro-symbolic integration. The performance of the proposed hybrid HNN-MAXRkSAT model has been explored and compared with the existing model. The proposed HNN-MAXRkSAT demonstrates good agreement with the existing models measured in terms of Global minimum Ratio (Gm), Hamming Distance (HD), Mean Absolute Error (MAE) and network computation Time CPU time). The proposed framework explored that MAX-RkSAT can be optimally represented in HNN and subsequently provides an additional platform for neural-symbolic integration, representing the various types of satisfiability logic.

International audience; We introduce a new algorithm that takes a Transition-based Emerson-Lei Automaton (TELA), that is, an ω-automaton whose acceptance condition is an arbitrary Boolean formula on sets of transitions to be seen infinitely or finitely often, and converts it into a Transition-based Parity Automaton (TPA). To reduce the size of the output TPA, the algorithm combines and optimizes two procedures based on a latest appearance record principle, and introduces a partial degeneralization. Our motivation is to use this algorithm to improve our LTL synthesis tool, where producing deterministic parity automata is an intermediate step.

Reaction systems, introduced by Ehrenfeucht and Rozenberg, are a theoretical model of computation based on the two main features of biochemical reactions: facilitation and inhibition, which are captured by the individual reactions of the system. All reactions, acting together, determine the global behavior or the result function, res, of the system. In this paper, we study decomposing of a given result function to find a functionally equivalent set of reactions. We propose several approaches, based on identifying reaction systems with Boolean functions, Boolean formulas, and logic circuits. We show how to minimize the number of reactions and their resources for each single output individually, as a group, and when only a subset of the states are considered. These approaches work both when the reactions of the given res function are known and not known. We characterize the minimal number of reactions through the minimal number of logical terms of the Boolean formula representation of the reaction system. Finally, we make applications recommendations for our findings.

Feature Models are a mechanism to organize the configuration space and facilitate the construction of software variants by describing configuration options using features, i.e., a name representing a functionality. The development of Feature Models is an error prone activity and detecting their anomalies is a challenging and important task needed to promote their usage. Feature Models have been extended with context to capture the correlation of configuration options with contextual influences and user customizations. Unfortunately, this extension makes the task of detecting anomalies harder. In this paper, we formalize the anomaly analysis in Context-aware Feature Models and we show how Quantified Boolean Formula (QBF) solvers can be used to detect anomalies without relying on iterative calls to a SAT solver. By extending the reconfigurator engine HyVarRec, we present findings evidencing that QBF solvers can outperform the common techniques for anomaly analysis on some instances.

SMT solving is often a major source of cost in a broad range of techniques such as symbolic program analysis. Thus, speeding up SMT solving is still an urgent requirement. A dominant approach, which is known as eager SMT solving, is to reduce a first-order formula to a pure Boolean formula, which is handed to an expensive SAT solver to determine the satisfiability. We observe that the SAT solver can utilize the knowledge in the first-order formula to boost its solving efficiency. Unfortunately, despite much progress, it is still not clear how to make use of the knowledge in an eager SMT solver. This paper addresses the problem by introducing a new and fast method, which utilizes the interval and data-dependence information learned from the first-order formulas. We have implemented the approach as a tool called Trident and evaluated it on three symbolic analyzers (Angr, Qsym, and Pinpoint). The experimental results, based on seven million SMT solving instances generated for thirty real-world software systems, show that Trident significantly reduces the total solving time from 2.9X to 7.9X over three state-of-the-art SMT solvers (Z3, CVC4, and Boolector), without sacrificing the number of solved instances. We also demonstrate that Trident achieves end-to-end speedups for three program analysis clients by 1.9X, 1.6X, and 2.4X, respectively.

Existing Byzantine fault-tolerant (BFT) consensus protocols address only threshold failures, where the participating nodes fail independently of each other, each one fails equally likely, and the protocol's guarantees follow from a simple bound on the number of faulty nodes. With the widespread deployment of Byzantine consensus in blockchains and distributed ledgers today, however, more sophisticated trust assumptions are needed. This paper presents the first implementation of BFT consensus with generalized quorums. It starts from a number of generalized trust structures motivated by practice and explores methods to specify and implement them efficiently. In particular, it expresses the trust assumption by a monotone Boolean formula (MBF) with threshold operators and by a monotone span program (MSP), a linear-algebraic model for computation. An implementation of HotStuff BFT consensus using these quorum systems is described as well and compared to the existing threshold model. Benchmarks with HotStuff running on up to 40 replicas demonstrate that the MBF specification incurs no significant slowdown, whereas the MSP expression affects latency and throughput noticeably due to the involved computations., To appear in the proceedings of SRDS 2020

Given an unsatisfiable Boolean Formula F in CNF, i.e., a set of clauses, one is often interested in identifying Maximal Satisfiable Subsets (MSSes) of F or, equivalently, the complements of MSSes called Minimal Correction Subsets (MCSes). Since MSSes (MC- Ses) find applications in many domains, e.g. diagnosis, ontologies debugging, or axiom pinpointing, several MSS enumeration algorithms have been proposed. Unfortunately, finding even a single MSS is often very hard since it naturally subsumes repeatedly solving the satisfiability problem. Moreover, there can be up to exponentially many MSSes, thus their complete enumeration is often practically intractable. Therefore, the algorithms tend to identify as many MSSes as possible within a given time limit. In this work, we present a novel MSS enumeration algorithm called RIME. Compared to existing algorithms, RIME is much more frugal in the number of performed satisfiability checks which we witness via an experimental comparison. Moreover, RIME is several times faster than existing tools.

International audience; In this paper we consider the path planning problem for a team of identical mobile robots that should fulfill a given global specification. This specification is given as a Boolean formula over some regions of interest and should be satisfied on the final state (when the robots stop) and on the trajectories. The main novelty of this paper is the automatic computation of collision-free trajectories. The approach is based on a Petri net model and on solving two Mixed Integer Linear Programming problems. Based on the solutions of these problems, intermediate synchronization points are introduced in order to avoid possible collisions. Additionally, the algorithm in this paper is implemented in an open-source Matlab toolbox, called RMTool.

In this work, we present: the first adaptively secure ABE for DFA from the k-Lin assumption in prime-order bilinear groups; this resolves one of open problems posed by Waters [CRYPTO’12]; the first ABE for NFA from the k-Lin assumption, provided the number of accepting paths is smaller than the order of the underlying group; the scheme achieves selective security; the first compact adaptively secure ABE (supporting unbounded multi-use of attributes) for branching programs from the k-Lin assumption, which generalizes and simplifies the recent result of Kowalczyk and Wee for boolean formula (NC1) [EUROCRYPT’19].

The physics-based simulation game Angry Birds has been heavily researched by the AI community over the past five years, and has been the subject of a popular AI competition that is currently held annually as part of a leading AI conference. Developing intelligent agents that can play this game effectively has been an incredibly complex and challenging problem for traditional AI techniques to solve, even though the game is simple enough that any human player could learn and master it within a short time. In this paper we analyse how hard the problem really is, presenting several proofs for the computational complexity of Angry Birds. By using a combination of several gadgets within this game's environment, we are able to demonstrate that the decision problem of solving general levels for different versions of Angry Birds is either NP-hard, PSPACE-hard, PSPACE-complete or EXPTIME-hard. Proof of NP-hardness is by reduction from 3-SAT, whilst proof of PSPACE-hardness is by reduction from True Quantified Boolean Formula (TQBF). Proof of EXPTIME-hardness is by reduction from G2, a known EXPTIME-complete problem similar to that used for many previous games such as Chess, Go and Checkers. To the best of our knowledge, this is the first time that a single-player game has been proven EXPTIME-hard. This is achieved by using stochastic game engine dynamics to effectively model the real world, or in our case the physics simulator, as the opponent against which we are playing. These proofs can also be extended to other physics-based games with similar mechanics., Comment: 55 Pages, 39 Figures

In this paper, we discuss the copy complexity of unit resolution with respect to Horn formulas. A Horn formula is a boolean formula in conjunctive normal form (CNF) with at most one positive literal per clause. Horn formulas find applications in a number of domains such as program verification and logic programming. Resolution as a proof system for boolean formulas is both sound and complete. However, resolution is considered an inefficient proof system when compared to other stronger proof systems for boolean formulas. Despite this inefficiency, the simple nature of resolution makes it an integral part of several theorem provers. Unit resolution is a restricted form of resolution in which each resolution step needs to use a clause with only one literal (unit literal clause). While not complete for general CNF formulas, unit resolution is complete for Horn formulas. A read-once resolution (ROR) refutation is a refutation in which each clause (input or derived) may be used at most once in the derivation of a refutation. As with unit resolution, ROR refutation is incomplete in general and complete for Horn clauses. This paper focuses on a combination of unit resolution and read-once resolution called Unit read-once resolution (UROR). UROR is incomplete for Horn clauses. In this paper, we study the copy complexity problem in Horn formulas under UROR. Briefly, the copy complexity of a formula under UROR is the smallest number k such that replicating each clause k times guarantees the existence of a UROR refutation. This paper focuses on two problems related to the copy complexity of unit resolution. We first relate the copy complexity of unit resolution for Horn formulas to the copy complexity of the addition rule in the corresponding Horn constraint system. We also examine a form of copy complexity where we permit replication of derived clauses, in addition to the input clauses. Finally, we provide a polynomial time algorithm for the problem of checking if a 2-CNF formula has a UROR refutation.

Given a Boolean formula \(\varphi \), the problem of model counting, also referred to as #SAT, is to compute the number of solutions of \(\varphi \). The hashing-based techniques for approximate counting have emerged as a dominant approach, promising achievement of both scalability and rigorous theoretical guarantees. The standard construction of strongly 2-universal hash functions employs dense XORs (i.e., involving half of the variables in expectation), which is widely known to cause degradation in the runtime performance of state of the art \(\mathsf {SAT}\) solvers. Consequently, the past few years have witnessed an intense activity in the design of sparse XORs as hash functions. Such constructions have been proposed with beliefs to provide runtime performance improvement along with theoretical guarantees similar to that of dense XORs.

The random satisfiability (RAN-SAT) is a problem that decides whether there exists a mapping of truth values to variables that makes a given random Boolean formula satisfiable. This paper gives a brief discussion on artificial neural network, Hopfield neural networks and logic programming integration. It proposed a method of optimizing random satisfiability in Hopfield neural networks based on the model energy minimization scheme. Computer simulation is carried out to demonstrate and verify the feasibility to carrying out random satisfiability in the Hopfield network.

In many areas of computer science, we are given an unsatisfiable Boolean formula F in CNF, i.e. a set of clauses, with the goal to identify minimal unsatisfiable subsets (MUSes) of F. The more MUSes are identified, the better insight into F’s unsatisfiability is obtained. Unfortunately, finding even a single MUS can be very time consuming since it naturally subsumes repeatedly solving the satisfiability problem, and thus a complete MUS enumeration is often practically intractable. Therefore, contemporary MUS enumeration algorithms tend to identify as many MUSes as possible within a given time limit. In this work, we present a novel MUS enumeration algorithm. Compared to existing algorithms, our algorithm is much more frugal in the number of performed satisfiability checks. Consequently, our algorithm is often able to find substantially more MUSes than contemporary algorithms.

In order to leverage the capacities of non-linear constraint solvers, we propose a reformulation of SAT into a box-constrained optimization problem where the objective function is polynomial. We prove that any optimal solution of the numerical problem corresponds to a solution of the Boolean formula, and demonstrate a stopping criterion that can be used with a numerical solver.

The Propositional Logic plays a central role in Artificial Intelligence. Extremely simple, this logic already addresses some of the most important problems in computer theory. It allows an incredible panel of pragmatic solutions to be successfully applied on a large number of (theoretically) hard problems. Its apparent simplicity allows one to design very efficient and compact algorithms to tackle, in practice, problems lying at the first levels of the complexity classes. In this chapter, we first present the kind of A.I. problems that can typically be addressed by this formalism. Then, we present an historical view of the impressive progresses observed in the practical solving of the Satisfiability (SAT) problem. Then, we introduce the concept of Knowledge Compilation, another important field of A.I. often build upon Propositional Logic. We also introduce Quantified Boolean Formula (QBF), a natural extension of SAT to quantifiers.

Attribute-based encryption (ABE) is an advanced form of encryption scheme allowing for access policies to be embedded within the secret keys and ciphertexts. By now, we have ABEs supporting numerous types of policies based on hardness assumptions over bilinear maps and lattices. However, one of the distinguishing differences between ABEs based on these two breeds of assumptions is that the former can achieve adaptive security for quite expressible policies (e.g., inner-products, boolean formula) while the latter can not. Recently, two adaptively secure lattice-based ABEs have appeared and changed the state of affairs: a non-zero inner-product (NIPE) encryption by Katsumata and Yamada (PKC’19) and an ABE for t-CNF policies by Tsabary (CRYPTO’19). However, the policies supported by these ABEs are still quite limited and do not embrace the more interesting policies that have been studied in the literature. Notably, constructing an adaptively secure inner-product encryption (IPE) based on lattices still remains open.

At Eurocrypt’19, Attrapadung presented several transformations that dynamically compose a set of attribute-based encryption (ABE) schemes for simpler predicates into a new ABE scheme for more expressive predicates. Due to the powerful unbounded and modular nature of his compositions, many new ABE schemes can be obtained in a systematic manner. However, his approach heavily relies on q-type assumptions, which are not standard. Devising such powerful compositions from standard assumptions was left as an important open problem. In this paper, we present a new framework for constructing ABE schemes that allow unbounded and dynamic predicate compositions among them, and show that the adaptive security of these composed ABE will be preserved by relying only on the standard matrix Diffie-Hellman (MDDH) assumption. This thus resolves the open problem posed by Attrapadung. As for applications, we obtain various ABEs that are the first such instantiations of their kinds from standard assumptions. These include the following adaptively secure large-universe ABEs for Boolean formulae under MDDH: The first completely unbounded monotone key-policy (KP)/ciphertext-policy (CP) ABE. Such ABE was recently proposed, but only for the KP and small-universe flavor (Kowalczyk and Wee, Eurocrypt’19). The first completely unbounded non-monotone KP/CP-ABE. Especially, our ABEs support a new type of non-monotonicity that subsumes previous two types of non-monotonicity, namely, by Ostrovsky et al. (CCS’07) and by Okamoto and Takashima (CRYPTO’10). The first (non-monotone) KP and CP-ABE with constant-size ciphertexts and secret keys, respectively. The first KP and CP-ABE with constant-size secret keys and ciphertexts, respectively.

Given a Boolean formula, the problem of counting seeks to estimate the number of solutions of F while the problem of uniform sampling seeks to sample solutions uniformly at random. Counting and uniform sampling are fundamental problems in computer science with a wide range of applications ranging from constrained random simulation, probabilistic inference to network reliability and beyond. The past few years have witnessed the rise of hashing-based approaches that use XOR-based hashing and employ SAT solvers to solve the resulting CNF formulas conjuncted with XOR constraints. Since over 99% of the runtime of hashing-based techniques is spent inside the SAT queries, improving CNF-XOR solvers has emerged as a key challenge.