Search

When a circuit exhibits abnormal behaviour, a diagnosis of the circuit is a set of gates whose failure explains the abnormality. The cardinality of a diagnosis is the number of gates assumed to be failing. A diagnosis is of minimum cardinality if no other diagnosis of the circuit exists that has a smaller cardinality. In general, the number of diagnoses can be exponentially large, and often only a preferred set of minimum-cardinality diagnoses is computed. In propositional satisfiability (SAT), given a propositional circuit, the task is to check whether all gates of the circuit can be assigned values in a consistent manner. In SAT-based diagnosis approach, the given circuit is injected with additional circuitry modelling the health of gates as well as the cardinality constraint. Under an abnormal observation the SAT solver repeatedly computes consistent assignments to all gates in the augmented circuit where each such assignment corresponds to a minimum-cardinality diagnosis. However, diagnosis of large size circuits as well as diagnostic cases with large minimum cardinalities pose a challenge for SAT solvers. To scale diagnosis to larger and harder cases, we propose a novel encoding that captures the hierarchical structure of the circuit in terms of single-output self-contained sub-circuits called cones. Cones have been exploited in diagnostic reasoning in the past; however, our encoding is the first of its kind in a SAT-based approach. Previously, cones were used to take the abstraction of a circuit and simplify it, while we exploit cones to improve the speed and efficiency of the SAT solver. Experiments on 1800 diagnostic cases of ISCAS-85 benchmark circuits show that the new encoding allows faster and more scalable diagnosis solving $$1700$$ 1700 cases which is $$163$$ 163 more than the number of cases solved by the baseline approach. [ABSTRACT FROM AUTHOR]

We consider the extension of the two-variable guarded fragment logic with local Presburger quantifiers. These are quantifiers that can express properties such as "the number of incoming blue edges plus twice the number of outgoing red edges is at most three times the number of incoming green edges" and captures various description logics with counting, but without constant symbols. We show that the satisfiability problem for this logic is EXP-complete. While the lower bound already holds for the standard two-variable guarded fragment logic, the upper bound is established by a novel, yet simple deterministic graph-based algorithm. [ABSTRACT FROM AUTHOR]

Can we efficiently compute optimal solutions to instances of a hard problem from optimal solutions to neighbor instances, that is, instances with one local modification? For example, can we efficiently compute an optimal coloring for a graph from optimal colorings for all one-edge-deleted subgraphs? Studying such questions not only gives detailed insight into the structure of the problem itself, but also into the complexity of related problems, most notably, graph theory's core notion of critical graphs (e.g., graphs whose chromatic number decreases under deletion of an arbitrary edge) and the complexity-theoretic notion of minimality problems (also called criticality problems, e.g., recognizing graphs that become 3-colorable when an arbitrary edge is deleted). We focus on two prototypical graph problems, colorability and vertex cover. For example, we show that it is NP -hard to compute an optimal coloring for a graph from optimal colorings for all its one-vertex-deleted subgraphs, and that this remains true even when optimal solutions for all one-edge-deleted subgraphs are given. In contrast, computing an optimal coloring from all (or even just two) one-edge-added supergraphs is in P . We observe that vertex cover exhibits a remarkably different behavior, demonstrating the power of our model to delineate problems from each other more precisely on a structural level. Moreover, we provide a number of new complexity results for minimality and criticality problems. For example, we prove that Minimal-3-UnColorability is complete for DP (differences of NP sets), which was previously known only for the more amenable case of deleting vertices rather than edges. For vertex cover, we show that recognizing β -vertex-critical graphs is complete for Θ 2 p (parallel access to NP ), obtaining the first completeness result for a criticality problem for this class. [ABSTRACT FROM AUTHOR]

We obtain exact expressions counting the satisfiable 2-SAT formulae and describe the structure of associated implication digraphs. Our approach is based on generating function manipulations. To reflect the combinatorial specificities of the implication digraphs, we introduce a new kind of generating function, the Implication generating function, inspired by the Graphic generating function used in digraph enumeration. Using the underlying recurrences, we make accurate numerical predictions of the phase transition curve of the 2-SAT problem inside the critical window. We expect these exact formulae to be amenable to rigorous asymptotic analysis using complex analytic tools, leading to a more detailed picture of the 2-SAT phase transition in the future.Mathematics Subject Classifications: 05A15, 68Q87, 68R95Keywords: 2-CNF, exact enumeration, random graphs, phase transitions, strongly connected components, satisfiability, generating functions

Modal logic S5, which isan important knowledge representation and reasoning paradigm, has been successfully applied in various artificial-intelligence-related domains. Similar to the random propositional theories in conjunctive clause form, the phase transition plays an important role in designing efficient algorithms for computing models of propositional S5 theories. In this paper, a new form of S5 formula is proposed, which fixes the number of modal operators and literals in the clauses of the formula. This form consists of reduced 3-3-S5 clauses of the form l 1 ∨ l 2 ∨ ξ , where ξ takes the form □ (l 3 ∨ l 4 ∨ l 5 ), ◊ (l 3 ∧ l 4 ∧ l 5) , or a propositional literal, and l i (1 ≤ i ≤ 5) is a classical literal. Moreover, it is demonstrated that any S5 formula can be translated into a set of reduced 3-3-S5 clauses while preserving its satisfiability. This work further investigates the probability of a random 3-c-S5 formula with c = 1 , 2 , 3 being satisfied by random assignment. In particular, we show that the satisfiability threshold of random 3-1-S5 clauses is − ln 2 (1 − P d − P s) ln 7 8 + P s · ln 3 4 , where P s and P d denote the probabilities of different modal operators appearing in a clause. Preliminary experimental results on random 3-1-S5 formulas confirm this theoretical threshold. [ABSTRACT FROM AUTHOR]

Search/optimization problems are plentiful in scientific and engineering domains. Artificial intelligence has long contributed to the development of search algorithms and declarative programming languages geared toward solving and modeling search/optimization problems. Automated reasoning and knowledge representation are the subfields of AI that are particularly vested in these developments. Many popular automated reasoning paradigms provide users with languages supporting optimization statements: answer set programming or MaxSAT or min-one, to name a few. These paradigms vary significantly in their languages and in the ways they express quality conditions on computed solutions. Here we propose a unifying framework of so-called weight systems that eliminates syntactic distinctions between paradigms and allows us to see essential similarities and differences between optimization statements provided by paradigms. This unifying outlook has significant simplifying and explanatory potential in the studies of optimization and modularity in automated reasoning and knowledge representation. It also supplies researchers with a convenient tool for proving the formal properties of distinct frameworks; bridging these frameworks; and facilitating the development of translational solvers. [ABSTRACT FROM AUTHOR]

In this paper we study a variation of the random $k$ -SAT problem, called polarised random $k$ -SAT, which contains both the classical random $k$ -SAT model and the random version of monotone $k$ -SAT another well-known NP-complete version of SAT. In this model there is a polarisation parameter $p$ , and in half of the clauses each variable occurs negated with probability $p$ and pure otherwise, while in the other half the probabilities are interchanged. For $p=1/2$ we get the classical random $k$ -SAT model, and at the other extreme we have the fully polarised model where $p=0$ , or 1. Here there are only two types of clauses: clauses where all $k$ variables occur pure, and clauses where all $k$ variables occur negated. That is, for $p=0$ , and $p=1$ , we get an instance of random monotone $k$ -SAT. We show that the threshold of satisfiability does not decrease as $p$ moves away from $\frac{1}{2}$ and thus that the satisfiability threshold for polarised random $k$ -SAT with $p\neq \frac{1}{2}$ is an upper bound on the threshold for random $k$ -SAT. Hence the satisfiability threshold for random monotone $k$ -SAT is at least as large as for random $k$ -SAT, and we conjecture that asymptotically, for a fixed $k$ , the two thresholds coincide. [ABSTRACT FROM AUTHOR]

Hitting formulas, introduced by Iwama, are an unusual class of propositional CNF formulas. Not only is their satisfiability decidable in polynomial time, but even their models can be counted in closed form. This stands in stark contrast with other polynomial-time decidable classes, which usually have algorithms based on backtracking and resolution and for which model counting remains hard, like 2-SAT and Horn-SAT. However, those resolution-based algorithms usually easily imply an upper bound on resolution complexity, which is missing for hitting formulas. Are hitting formulas hard for resolution? In this paper we take the first steps towards answering this question. We show that the resolution complexity of hitting formulas is dominated by so-called irreducible hitting formulas, first studied by Kullmann and Zhao, that cannot be composed of smaller hitting formulas. However, by definition, large irreducible unsatisfiable hitting formulas are difficult to construct; it is not even known whether infinitely many exist. Building upon our theoretical results, we implement an efficient algorithm on top of the Nauty software package to enumerate all irreducible unsatisfiable hitting formulas with up to 14 clauses. We also determine the exact resolution complexity of the generated hitting formulas with up to 13 clauses by extending a known SAT encoding for our purposes. Our experimental results suggest that hitting formulas are indeed hard for resolution. [ABSTRACT FROM AUTHOR]

Many types of decision problems can be solved using mathematical modeling and analysis. Such techniques are also developed on the border of mathematical logic and computer science. A good example is the translation of the issues examined into the Satisfiability Problem (SAT) of a logical propositional formula. Unfortunately, this method is not always practical, considering the high computational complexity of solving the SAT problem. It often happens that in the studied cases, the encoding formulas contain even hundreds of thousands of clauses and propositional variables. However, even in these cases, modern SAT solvers can sometimes successfully solve these problems. This approach can be used to cryptanalyze some symmetric ciphers or parts/modifications. In this case, the encryption algorithm is first translated into a boolean formula. Then additional formulas are created to encode randomly selected plaintext and the key bits. Using the SAT solver; we can count the values of the ciphertext bits. Then, using the SAT solver again, we proceed to the cryptanalysis of the cipher with the selected plaintext and proper ciphertext, looking for the bits of the encryption key. In this paper, we will present the new results of how SAT techniques behave against representative fragments of the AES cipher, the current standard for symmetric encryption. We also compare the results obtained in this case by several SAT solvers. In addition, we present the results of the SAT-solver CryptoMiniSat obtained during the attack on the 1st round of the AES-128 cipher. [ABSTRACT FROM AUTHOR]

Modal logic S5, which isan important knowledge representation and reasoning paradigm, has been successfully applied in various artificial-intelligence-related domains. Similar to the random propositional theories in conjunctive clause form, the phase transition plays an important role in designing efficient algorithms for computing models of propositional S5 theories. In this paper, a new form of S5 formula is proposed, which fixes the number of modal operators and literals in the clauses of the formula. This form consists of reduced 3-3-S5 clauses of the form l1∨l2∨ξ, where ξ takes the form □(l3∨l4∨l5), ◊(l3∧l4∧l5), or a propositional literal, and li(1≤i≤5) is a classical literal. Moreover, it is demonstrated that any S5 formula can be translated into a set of reduced 3-3-S5 clauses while preserving its satisfiability. This work further investigates the probability of a random 3-c-S5 formula with c=1,2,3 being satisfied by random assignment. In particular, we show that the satisfiability threshold of random 3-1-S5 clauses is −ln2(1−Pd−Ps)ln78+Ps·ln34, where Ps and Pd denote the probabilities of different modal operators appearing in a clause. Preliminary experimental results on random 3-1-S5 formulas confirm this theoretical threshold.

One way of solving 3sat instances on a quantum computer is to transform the 3sat instances into instances of Quadratic Unconstrained Binary Optimizations (QUBOs), which can be used as an input for the QAOA algorithm on quantum gate systems or as an input for quantum annealers. This mapping is performed by a 3sat-to-QUBO transformation. Recently, it has been shown that the choice of the 3sat-to-QUBO transformation can significantly impact the solution quality of quantum annealing. It has been shown that the solution quality can vary up to an order of magnitude difference in the number of correct solutions received, depending solely on the 3sat-to-QUBO transformation. An open question is: what causes these differences in the solution quality when solving 3sat-instances with different 3sat-to-QUBO transformations? To be able to conduct meaningful studies that assess the reasons for the differences in the performance, a larger number of different 3sat-to-QUBO transformations would be needed. However, currently, there are only a few known 3sat-to-QUBO transformations, and all of them were created manually by experts, who used time and clever reasoning to create these transformations. In this paper, we will solve this problem by proposing an algorithmic method that is able to create thousands of new and different 3sat-to-QUBO transformations, and thus enables researchers to systematically study the reasons for the significant difference in the performance of different 3sat-to-QUBO transformations. Our algorithmic method is an exhaustive search procedure that exploits properties of 4 × 4 dimensional pattern QUBOs, a concept which has been used implicitly in the creation of 3sat-to-QUBO transformations before, but was never described explicitly. We will thus also formally and explicitly introduce the concept of pattern QUBOs in this paper. [ABSTRACT FROM AUTHOR]

It is well-known that the satisfiability problem of feature diagrams (FDs) is computationally hard. This paper examines the complexities of the satisfiability problems of sixteen FD sublanguages, i.e., languages that only permit a subset of the syntactic modeling elements of general FDs. Previous work neglected a detailed examination of the complexities of the satisfiability problems of FD sublanguages, although results in this area could lead to the development of efficient satisfiability checking procedures for the FDs of specific sublanguages. This paper contributes to fill this gap by analyzing the complexities of the satisfiability problems of sixteen FD sublanguages that differ in whether they allow or-groups, xor-groups, excludes constraints, and requires constraints. The results of this paper show that the satisfiability problem is NP-complete for eight of these sublanguages, is solvable in linear time for two of these sublanguages, and is trivial for the remaining six sublanguages in the sense that every FD of these sublanguages is satisfiable. The results are extended to feature model sublanguages with complex cross-tree constraints by extending FD sublanguages that have satisfiability problems, which are solvable in polynomial time. The feature model sublanguages also have satisfiability problems that are solvable in polynomial time. [ABSTRACT FROM AUTHOR]

Due to its excellent diffusion avalanche performance, MDS linear transformation based on rotational-XOR shift operation is frequently employed in the construction of block cipher diffusion layer. In existing studies, the search for the best linear transformation on the small finite field (F2n)~4 is almost complete, however when the number of XOR terms is between 9 and 11, there is no best linear transformation on the huge finite field (F2n)~8. For the actual use of the 64-bit environment, it is crucial to investigate the most recent optimum linear transformation of the huge finite field (F2~8)~8. This work chooses a huge finite field (F2n)~8 as its research object based on the findings of earlier studies. The branch number test problem is converted into a Boolean Satisfiability problem (SAT) by examining the structural properties of the rotational-XOR diffusion layer. The issue is solved using the Satisfiability Modulo Theories (SMT) solver Boolector, and the final linear transformation group of the huge finite field (F2n)~8 is investigated. The experimental findings demonstrate the existence of a suboptimal linear transformation in the huge finite field (F2~8)~8 with up to 8 branches. Along with the test, a particular rotational-XOR form is provided, and a different approach is suggested for determining the true requirement for the ideal diffusion layer. Future research will focus on the theoretical properties and broadened applications of the suboptimal linear transformation of the huge finite field (F2n)~8. [ABSTRACT FROM AUTHOR]

Model abstraction for finite state automata is beneficial to reduce the complexity of discrete-event systems (DES), enhance the readability and facilitate the control synthesis and verification of DES. Supremal quasi-congruence computation is an effective way for reducing the state space of DES. Effective algorithms on the supremal quasi-congruence relation have been developed based on the graph theory. This paper proposes a new approach to translate the supremal quasi-congruence computation into a satisfiability (SAT) problem that determines whether there exists an assignment for Boolean variables in the state-to-coset allocation matrix. If the result is satisfied, then the supremal quasi-congruence relation exists and the minimum equivalence classes is obtained. Otherwise, it indicates that there is no such supremal quasi-congruence relation, and a new set of observable events needs to be modified or reselected for the original system model. The satisfiability problem on the computation of supremal quasi-congruence relation is solved by different methods, which are respectively implemented by mixed integer linear programming (MILP) in MATLAB, binary linear programming (BLP) in CPLEX, and a SAT-based solver (Z3Py). Compared with the MILP and BLP methods, the SAT method is more efficient and stable. The computation time of model abstraction for large-scale systems by Z3Py solver is significantly reduced.

We construct simple, explicit matrices with columns having unit ℓ² norm and discrepancy approaching 1 + yz2 - 2.414. This number gives a lower bound, the strongest known as far as we are aware, on the constant appearing in the Komlos conjecture. The Unsatisfiable matrices giving this bound are built by scaling the entries of clause-variable matrices of certain Unsatisfiable Boolean formulas. We show that, for a given formula, such a scaling maximizing a lower bound on the discrepancy may be computed with a convex second-order cone program. Using a dual certificate for this program, we show that our lower bound is optimal among those using Unsatisfiable matrices built from formulas admitting read-once resolution proofs of unsatisfiability. We also conjecture that a generalization of this certificate shows that our bound is optimal among all bounds using Unsatisfiable matrices. [ABSTRACT FROM AUTHOR]

The most representative interval temporal logic, called HS, was introduced by Halpern and Shoham in the nineties. Recently, HS has been proposed as a suitable formalism for modern artificial intelligence applications; however, when dealing with real-life data one is not always able to express temporal relations and propositional labels in a definite, crisp way. In this paper, following the seminal ideas of Fitting and Zadeh, we present a fuzzy generalization of HS, called FHS, that partially solves such problems of expressive power. We study FHS from both a theoretical and an application standpoint: first, we discuss its syntax, semantics, expressive power, and satisfiability problem; then, we define and solve the time series FHS finite model checking problem, to serve as the basis of future applications. [ABSTRACT FROM AUTHOR]

The decoupling between the representation of a certain problem, that is, its knowledge model, and the reasoning side is one of main strong points of model-based artificial intelligence (AI). This allows, for example, to focus on improving the reasoning side by having advantages on the whole solving process. Further, it is also well known that many solvers are very sensitive to even syntactic changes in the input. In this paper, we focus on improving the reasoning side by taking advantages of such sensitivity. We consider two well-known model-based AI methodologies, SAT and ASP, define a number of syntactic features that may characterise their inputs, and use automated configuration tools to reformulate the input formula or program. Results of a wide experimental analysis involving SAT and ASP domains, taken from respective competitions, show the different advantages that can be obtained by using input reformulation and configuration. [ABSTRACT FROM AUTHOR]

We give a new general approach for designing exact exponential-time algorithms for subset problems. In a subset problem the input implicitly describes a family of sets over a universe of size n and the task is to determine whether the family contains at least one set. A typical example of a subset problem is Weighted d-SAT. Here, the input is a CNF-formula with clauses of size at most d, and an integer W. The universe is the set of variables and the variables have integer weights. The family contains all the subsets S of variables such that the total weight of the variables in S does not exceed W and setting the variables in S to 1 and the remaining variables to 0 satisfies the formula. Our approach is based on "monotone local search," where the goal is to extend a partial solution to a solution by adding as few elements as possible. More formally, in the extension problem, we are also given as input a subset X of the universe and an integer k. The task is to determine whether one can add at most k elements to X to obtain a set in the (implicitly defined) family. Our main result is that a cknO(1) time algorithm for the extension problem immediately yields a randomized algorithm for finding a solution of any size with running time O((2 - 1/c)n). In many cases, the extension problem can be reduced to simply finding a solution of size at most k. Furthermore, efficient algorithms for finding small solutions have been extensively studied in the field of parameterized algorithms. Directly applying these algorithms, our theorem yields in one stroke significant improvements over the best known exponential-time algorithms for several well-studied problems, including d-HITTING SET, FEEDBACK VERTEX SET, NODE UNIQE LABEL COVER, and WEIGHTED d-SAT. Our results demonstrate an interesting and very concrete connection between parameterized algorithms and exact exponential-time algorithms. We also show how to derandomize our algorithms at the cost of a subexponential multiplicative factor in the running time. Our derandomization is based on an efficient construction of a new pseudo-random object that might be of independent interest. Finally, we extend our methods to establish new combinatorial upper bounds and develop enumeration algorithms. [ABSTRACT FROM AUTHOR]

Clause Learning is one of the most important components of a conflict driven clause learning (CDCL) SAT solver that is effective on industrial SAT instances. Since the number of learned clauses is proved to be exponential in the worst case, it is necessary to identify the most relevant clauses to maintain and delete the irrelevant ones. As reported in the literature, several learned clauses deletion strategies have been proposed. However the diversity in both the number of clauses to be removed at each step of reduction and the results obtained with each strategy increase the difficulty to determine which criterion is better. Thus, the problem to select which learned clauses are to be removed during the search step remains very challenging. In this paper, we propose a novel approach to identify the most relevant learned clauses without favoring or excluding any of the proposed measures, but by adopting the notion of dominance relationship among those measures. Our approach bypasses the problem of difference in the results obtained with different measures and reaches a compromise between the measures assessments. Furthermore, the proposed approach also reduces the non-trivial problem of choosing the number of clauses to delete at each reduction of the learned clause database. [ABSTRACT FROM AUTHOR]

We continue the program of proving circuit lower bounds via circuit satisfiability algorithms. So far, this program has yielded several concrete results, proving that functions in Quasi - NP = NTIME [ n (log n) O (1) ] and other complexity classes do not have small circuits (in the worst case and/or on average) from various circuit classes C , by showing that C admits non-trivial satisfiability and/or # SAT algorithms which beat exhaustive search by a minor amount. In this paper, we present a new strong lower bound consequence of having a non-trivial # SAT algorithm for a circuit class C . Say that a symmetric Boolean function f(x1,...,xn) is sparse if it outputs 1 on O(1) values of ∑ i x i . We show that for every sparse f, and for all "typical" C , faster # SAT algorithms for C circuits imply lower bounds against the circuit class f ∘ C , which may be stronger than C itself. In particular: # SAT algorithms for nk-size C -circuits running in 2n/nk time (for all k) imply NEXP does not have (f ∘ C) -circuits of polynomial size. # SAT algorithms for 2 n ε -size C -circuits running in 2 n − n ε time (for some ε > 0) imply Quasi-NP does not have (f ∘ C) -circuits of polynomial size. Applying # SAT algorithms from the literature, one immediate corollary of our results is that Quasi-NP does not have EMAJ ∘ ACC0 ∘ THR circuits of polynomial size, where EMAJ is the "exact majority" function, improving previous lower bounds against ACC0 [Williams JACM'14] and ACC0 ∘THR [Williams STOC'14], [Murray-Williams STOC'18]. This is the first nontrivial lower bound against such a circuit class. [ABSTRACT FROM AUTHOR]

Numerous fundamental database and reasoning problems are known to be NP -hard in general but tractable on instances where the underlying hypergraph structure is β -acyclic. Despite the importance of many of these problems, there has been little success in generalizing these results beyond acyclicity. In this paper, we take on this challenge and propose nest-set width , a novel generalization of hypergraph β -acyclicity. We demonstrate that nest-set width has desirable properties and algorithmic significance. In particular, evaluation of boolean conjunctive queries with negation (CQ¬) is tractable for classes with bounded nest-set width. Furthermore, propositional satisfiability (SAT) is fixed-parameter tractable when parameterized by nest-set width. [ABSTRACT FROM AUTHOR]

In this paper we consider general continuous propositional logics and prove some basic properties about them. First, we characterize full systems of continuous connectives of the form { ¬ , ∸ , f } where f is a unary connective. We also show that, in contrast to the classical propositional logic, a full system of continuous propositional logic cannot contain only one continuous connective. We then construct a closed full system of continuous connectives without any constants. Such a system does not have any tautologies. For the rest of the paper we consider the standard continuous propositional logic as defined by Yaacov, I.B and Usvyatsov, A. We show that Strong Compactness and Craig Interpolation fail for this logic, but approximated versions of Strong Compactness and Craig Interpolation hold true. In the last part of the paper, we introduce various notions of satisfiability, falsifiability, tautology, and fallacy, and show that they are either NP-complete or co-NP-complete. [ABSTRACT FROM AUTHOR]