In interdependent systems, such as electric power systems, entities or components mutually depend on each other. Due to these interdependencies, a small number of initial failures can propagate throughout the system, resulting in catastrophic system failures. This paper addresses the problem of finding the set of entities whose failures will have the worst effects on the system. To this end, a two-phase algorithm is developed. In the first phase, the tight bound on failure propagation steps is computed using a Boolean Satisfiablility (SAT) solver. In the second phase, the problem is formulated as an Integer Linear Programming (ILP) problem using the obtained step bound and solved with an ILP solver. Experimental results show that the algorithm scales to large problem instances and outperforms a single-phase algorithm that uses a loose step bound.

Majority operation has been paid attention as a basic element of beyond-Moore devices on which logic functions are constructed from Majority elements and inverters. Several optimization methods are developed to reduce the number of elements on Majority-Inverter Graphs (MIGs) but more area and power reduction are required. The paper proposes a new exact synthesis method for MIG based on a new topological constraint using node levels. Possible graph structures are clustered by the levels of input nodes, and all possible structures can be enumerated efficiently in the exact synthesis compared with previous methods. Experimental results show that our method decreases the runtime up to 25.33% compared with the fence-based method, and up to 6.95% with the partial-DAG-based method. Furthermore, our implementation can achieve better performance in size optimization for benchmark suites.

A branching program is a well-studied model of computation and a representation for Boolean functions. It is a directed acyclic graph with a unique root node, some accepting nodes, and some rejecting nodes. Except for the accepting and rejecting nodes, each node has a label with a variable and each outgoing edge of the node has a label with a 0/1 assignment of the variable. The satisfiability problem for branching programs is, given a branching program with n variables and m nodes, to determine if there exists some assignment that activates a consistent path from the root to an accepting node. The width of a branching program is the maximum number of nodes at any level. The satisfiability problem for width-2 branching programs is known to be NP-complete. In this paper, we present a satisfiability algorithm for width-2 branching programs with n variables and cn nodes, and show that its running time is poly(n)·2(1-µ(c))n, where µ(c)=1/2O(c log c). Our algorithm consists of two phases. First, we transform a given width-2 branching program to a set of some structured formulas that consist of AND and Exclusive-OR gates. Then, we check the satisfiability of these formulas by a greedy restriction method depending on the frequency of the occurrence of variables.

Cascading Style Sheets (CSS) is a popular language for describing the styles of XML documents as well as HTML documents. To resolve conflicts among CSS rules, CSS has a mechanism called specificity. For a DTD D and a CSS code R, due to specificity R may contain “unsatisfiable” rules under D, e.g., rules that are not applied to any element of any document valid for D. In this paper, we consider the problem of detecting unsatisfiable CSS rules under DTDs. We focus on CSS fragments in which descendant, child, adjacent sibling, and general sibling combinators are allowed. We show that the problem is coNP-hard in most cases, even if only one of the four combinators is allowed and under very restricted DTDs. We also show that the problem is in coNP or PSPACE depending on restrictions on DTDs and CSS. Finally, we present four conditions under which the problem can be solved in polynomial time.

The circuit satisfiability problem has been intensively studied since Ryan Williams showed a connection between the problem and lower bounds for circuit complexity. In this letter, we present a #SAT algorithm for synchronous Boolean circuits of n inputs and s gates in time $2^{nleft(1 - rac{1}{2^{O(s/n)}} ight)}$ if s=o(n log n).

In a real-time system, tasks are required to be completed before their deadlines. Under normal workload conditions, a scheduler with a proper scheduling policy can make all the tasks meet their deadlines. However, in practical environment, system workload may vary widely. Once system workload becomes too heavy, so that there does not exist a feasible schedule can make all the tasks meet their deadlines, we say the system is overloaded under which some tasks will miss their deadlines. To alleviate the degrees of system performance degradation caused by the missed deadline tasks, the design of scheduling is crucial. Many design objectives can be considered. In this paper, we first focus on maximizing the total number of tasks that can be completed before their deadlines. A scheduling method based on satisfiability modulo theories (SMT) is proposed. In the method, the problem of scheduling is treated as a satisfiability problem. The key work is to formalize the satisfiability problem using first-order language. After the formalization, a SMT solver (e.g., Z3, Yices) is employed to solve this satisfiability problem. An optimal schedule can be generated based on the solution model returned by the SMT solver. The correctness of this method and the optimality of the generated schedule can be verified in a straightforward manner. The time efficiency of the proposed method is demonstrated through various simulations. Moreover, in the proposed SMT-based scheduling method, we define the scheduling constraints as system constraints and target constraints. This means if we want to design scheduling to achieve other objectives, only the target constraints need to be modified. To demonstrate this advantage, we adapt the SMT-based scheduling method to other design objectives: maximizing effective processor utilization and maximizing obtained values of completed tasks. Only very little changes are needed in the adaption procedure, which means the proposed SMT-based scheduling method is flexible and sufficiently general.

We propose an exact algorithm to determine the satisfiability of oblivious read-twice branching programs. Our algorithm runs in $2^{left(1 - Omega(rac{1}{log c}) ight)n}$ time for instances with n variables and cn nodes.

Cold boot attack is a side channel attack that recovers data from memory, which persists for a short period after power is lost. In the course of this attack, the memory gradually degrades over time and only a corrupted version of the data may be available to the attacker. Recently, great efforts have been made to reconstruct the original data from a corrupted version of AES key schedules, based on the assumption that all bits in the charged states tend to decay to the ground states while no bit in the ground state ever inverts. However, in practice, there is a small number of bits flipping in the opposite direction, called reverse flipping errors. In this paper, motivated by the latest work that formulates the relations of AES key bits as a Boolean Satisfiability problem, we move one step further by taking the reverse flipping errors into consideration and employing off-the-shelf SAT and MaxSAT solvers to accomplish the recovery of AES-128 key schedules from decayed memory images. Experimental results show that, in the presence of reverse flipping errors, the MaxSAT approach enables reliable recovery of key schedules with significantly less time, compared with the SAT approach that relies on brute force search to find out the target errors. Moreover, in order to further enhance the efficiency of key recovery, we simplify the original problem by removing variables and formulas that have relatively weak relations to the whole key schedule. Experimental results demonstrate that the improved MaxSAT approach reduces the scale of the problem and recover AES key schedules more efficiently when the decay factor is relatively large.

Recently, Impagliazzo et al. constructed a nontrivial algorithm for the satisfiability problem for sparse threshold circuits of depth two which is a class of circuits with cn wires. We construct a nontrivial algorithm for a larger class of circuits. Two gates in the bottom level of depth two threshold circuits are dependent, if the output of the one is always greater than or equal to the output of the other one. We give a nontrivial circuit satisfiability algorithm for a class of circuits which may not be sparse in gates with dependency. One of our motivations is to consider the relationship between the various circuit classes and the complexity of the corresponding circuit satisfiability problem of these classes. Another background is proving strong lower bounds for TC0 circuits, exploiting the connection which is initiated by Ryan Williams between circuit satisfiability algorithms and lower bounds.

Many fatal accidents involving safety-critical reactive systems have occurred in unexpected situations, which were not considered during the design and test phases of system development. To prevent such accidents, reactive systems should be designed to respond appropriately to any request from an environment at any time. Verifying this property during the specification phase reduces the development costs of safety-critical reactive systems. This property of a specification is commonly known as realizability. The complexity of the realizability problem is 2EXPTIME-complete. We have introduced the concept of strong satisfiability, which is a necessary condition for realizability. Many practical unrealizable specifications are also strongly unsatisfiable. In this paper, we show that the complexity of the strong satisfiability problem is EXPSPACE-complete. This means that strong satisfiability offers the advantage of lower complexity for analysis, compared to realizability. Moreover, we show that the strong satisfiability problem remains EXPSPACE-complete even when only formulae with a temporal depth of at most 2 are allowed.

In this paper, we consider the XPath satisfiability problem under restricted DTDs called “duplicate free”. For an XPath expression q and a DTD D, q is satisfiable under D if there exists an XML document t such that t is valid against D and that the answer of q on t is nonempty. Evaluating an unsatisfiable XPath expression is meaningless, since such an expression can always be replaced by an empty set without evaluating it. However, it is shown that the XPath satisfiability problem is intractable for a large number of XPath fragments. In this paper, we consider simple XPath fragments under two restrictions: (i) only a label can be specified as a node test and (ii) operators such as qualifier ([]) and path union (∪) are not allowed. We first show that, for some small XPath fragments under the above restrictions, the satisfiability problem is NP-complete under DTDs without any restriction. Then we show that there exist XPath fragments, containing the above small fragments, for which the satisfiability problem is in PTIME under duplicate-free DTDs.

State Transition Matrix (STM) is a table-based modeling language that has been frequently used in industry for specifying behaviors of systems. Functional correctness of a STM design (i.e., a design developed with STM) could often be expressed as invariant properties. In this paper, we first present a formalization of the static and dynamic aspects of STM designs. Consequentially, based on this formalization, we investigate a symbolic encoding approach, through which a STM design could be bounded model checked w.r.t. invariant properties by using Satisfiability Modulo Theories (SMT) solving technique. We have built a prototype implementation of the proposed encoding and the state-of-the-art SMT solver - Yices, is used in our experiments to evaluate the effectiveness of our approach. Two attempts for accelerating SMT solving are also reported.

One of the critical issue in framework-based software development is a huge introduction cost caused by technical gap between developers and users of frameworks. This paper proposes a technique for deriving framework usages to implement a given requirements specification. By using the derived usages, the users can use the frameworks without understanding the framework in detail. Requirements specifications which describe definite behavioral requirements cannot be related to frameworks in as-is since the frameworks do not have definite control structure so that the users can customize them to suit given requirements specifications. To cope with this issue, a new technique based on satisfiability problems (SAT) is employed to derive the control structures of the framework model. In the proposed technique, requirements specifications and frameworks are modeled based on Labeled Transition Systems (LTSs) with branch conditions represented by predicates. Truth assignments of the branch conditions in the framework models are not given initially for representing the customizable control structure. The derivation of truth assignments of the branch conditions is regarded as the SAT by assuming relations between termination states of the requirements specification model and ones of the framework model. This derivation technique is incorporated into a technique we have proposed previously for relating actions of requirements specifications to ones of frameworks. Furthermore, this paper discuss a case study of typical use cases in e-commerce systems.

Finding fixed points in discrete dynamical systems is important because fixed points correspond to steady-states. The Boolean network is considered as one of the simplest discrete dynamical systems and is often used as a model of genetic networks. It is known that detection of a fixed point in a Boolean network with n nodes and maximum indegree K can be polynomially transformed into (K+1)-SAT with n variables. In this paper, we focus on the case of K=2 and present an O(1.3171n) expected time algorithm, which is faster than the naive algorithm based on a reduction to 3-SAT, where we assume that nodes with indegree 2 do not contain self-loops. We also show an algorithm for the general case of K=2 that is slightly faster than the naive algorithm.

For formal verification of large-scale digital circuits, a method using satisfiability checking of logic with equality and uninterpreted functions has been proposed. This logic, however, does not consider specific properties of functions or predicates at all, e.g. associative property of addition. In order to ease this problem, we introduce "equivalence constraint" that is a set of formulas representing the properties of functions and predicates, and check the satisfiability of formulas under the constraint. In this report, we show an algorithm for checking satisfiability with equivalence constraint and also experimental results.

This paper proposes flat and hierarchical approaches for generating a minimum-width transistor placement of CMOS cells in presence of non-dual P and N type transistors. Our approaches are the first exact method which can be applied to CMOS cells with any types of structure. Non-dual CMOS cells occupy a major part of an industrial standard-cell library. To generate the exact minimum-width transistor placement of non-dual CMOS cells, we formulate the transistor placement problem into Boolean Satisfiability (SAT) problem considering the P and N type transistors individually. Using the proposed method, the transistor placement problem of any types of CMOS cells can be solved exactly. In addition, the experimental results show that our flat approach generates smaller width placement for 29 out of 103 dual cells than that of the conventional method. Our hierarchical approach reduces the runtimes drastically. Although this approach has possibility to generate wider placements than that of the flat approach, the experimental results show that the width of only 3 out of 147 cells solved by our hierarchical approach are larger than that of the flat approach.

This paper proposes a cell layout synthesis method via Boolean Satisfiability (SAT). Cell layout synthesis problems are first transformed into SAT problems by our formulations. Our method realizes a high-speed layout synthesis for CMOS logic cells and guarantees to generate the minimum-width cells with routability under our layout styles. It considers complementary P-/N-MOSFETs individually during transistor placement, and can generate smaller width layout compared with pairing the complementary P-/N-MOSFETs case. To demonstrate the effectiveness of our SAT-based cell synthesis, we present experimental results which compare it with the 0-1 ILP-based transistor placement method and a commercial cell generation tool. The experimental results show that our SAT-based method can generate minimum-width placements in much shorter run time than the 0-1 ILP-based transistor placement method, and can generate the cell layouts of 32 static dual CMOS logic circuits in 54% run time compared with the commercial tool. Area increase of our method without compaction is only 3% compared with the commercial tool with compaction.

Combinational logic circuits are usually implemented as multi-level networks of logic nodes. Multi-level logic simplification using the don't cares on each node is widely used. Large don't cares give good simplification results, but suffer from huge memory area and computation time. Extraction of useful don't cares and reduction of the size of the don't cares are important problems on the simplification using don't cares. In the paper, we propose a new robust heuristic method for the selection of don't cares. We consider an adaptive subnetwork for each simplified node in the network and introduce a stepwise enhancement method of the subnetwork considering the memory area and the network structure. The don't cares extracted from the adaptive subnetworks are called the local don't cares. We have implemented our method for satisfiability don't cares and observability don't cares. We have applied the method on MCNC89 benchmarks, and compared the experimental results with those of the SIS system. The results demonstrate the superiority of our method on the quality of the results and on the size of applicable circuits.

Multi-cycle paths are paths between registers where 2 or more clock cycles are allowed to propagate signals, and the detection of multi-cycle paths is important in deciding proper clock period, timing verification and logic optimization. This paper presents a satisfiability-based multi-cycle path detection method, where the detection problems are reduced to CNF formulae and the satisfiability is checked using SAT provers. We also show heuristics on conversion from multi-level circuits into CNF formulae. We have applied our method to ISCAS'89 benchmarks and other sample circuits. Experimental results show the remarkable improvements on the size of manipulatable circuits.

Ordered Binary Decision Diagrams (OBDDs) are graph-based representations of Boolean functions which are widely used because of their good properties. In this paper, we introduce nondeterministic OBDDs (NOBDDs) and their restricted forms, and evaluate their expressive power. In some applications of OBDDs, canonicity, which is one of the good properties of OBDDs, is not necessary. In such cases, we can reduce the required amount of storage by using OBDDs in some non-canonical form. A class of NOBDDs can be used as a non-canonical form of OBDDs. In this paper, we focus on two particular methods which can be regarded as using restricted forms of NOBDDs. Our aim is to show how the size of OBDDs can be reduced in such forms from theoretical point of view. Firstly, we consider a method to solve satisfiability problem of combinational circuits using the structure of circuits as a key to reduce the NOBDD size. We show that the NOBDD size is related to the cutwidth of circuits. Secondly, we analyze methods that use OBDDs to represent Boolean functions as sets of product terms. We show that the class of functions treated feasibly in this representation strictly contains that in OBDDs and contained by that in NOBDDs.