Satisfiability (SAT) solvers often benefit from clauses learned by the DPLL procedure, even though they are by definition redundant. In addition to those derived from conflicts, the clauses learned by dominator analysis during the deduction procedure tend to produce smaller implication graphs and sometimes increase the deductive power of the input CNF formula. We extend dominator analysis with an efficient self-subsumption check. We also show how the information collected by dominator analysis can be used to detect redundancies in the satisfied clauses and, more importantly, how it can be used to produce supplemental conflict clauses. We characterize these transformations in terms of deductive power and proof conciseness. Experiments show that the main advantage of dominator analysis and its extensions lies in improving proof conciseness.

Satisfiability (SAT) solvers often benefit from transformations of the formula to be decided that allow them to do more through deduction and decrease their reliance on enumeration. For formulae in conjunctive normal form, subsumed clauses may be removed or partial resolution may be applied. The objectives of simplifying the formula and speeding up the solver are sometimes competing. We characterize existing transformations in terms of their impact on the deductive power of the formula and their effects on the sizes of the implication graphs. For example, we show that variable elimination works by improving implication graphs. We also present two new techniques that try to increase deductive power. The first is a check performed during the computation of resolvents. The second is a new preprocessing algorithm based on distillation that combines simplification and increase of deductive power. Most current SAT solvers apply resolution at various stages to derive new clauses or simplify existing ones. The former happens during conflict analysis, while the latter is usually done during preprocessing. We show how subsumption of the operands by the resolvent can be inexpensively detected during resolution; we then discuss how this detection is used to improve three stages of the SAT solver: variable elimination, clause distillation, and conflict analysis. The “on-the-fly” subsumption check is easily integrated in a SAT solver. In particular, it is compatible with strong conflict analysis and the generation of unsatisfiability proofs. Experiments show the effectiveness of the new techniques.

We present a new approach to conflict analysis for propositional satisfiability solvers based on the DPLL procedure and clause recording. When conditions warrant it, we generate a supplemental clause from a conflict. This clause does not contain a unique implication point, and therefore cannot replace the standard conflict clause. However, it is very effective at reducing excessive depth in the implication graphs and at preventing repeated conflicts on the same clause. Experimental results show consistent improvements over state-of-the-art solvers and confirm our analysis of why the new technique works.

We propose a new intra-task dynamic voltage scaling (DVS) method to capture an important fact of ‘software runtime distribution ’ and integrate it into DVS effectively. Specifically, the proposed method finds performance levels, for a given software runtime distribution, i.e. statistical profiling of execution cycles (neither the execution cycle of worst-case execution path nor the worst-case execution cycles of basic blocks), which leads to a minimal energy consumption while satisfying the given deadline constraints. Experimental results report that the proposed method gives 19.2%~33.3 % further energy reduction compared with the best-known methods for two industrial multimedia software programs, H.264 decoder and MPEG4 decoder. 1.

The authors propose a scalable abstraction-refinement method for model checking invariant properties on large sequential circuits, which is based on fine-grain abstraction and simultaneous analysis of all abstract counterexamples of the shortest length. Abstraction efficiency is introduced to measure for a given abstraction-refinement algorithm how much of the concrete model is required to make the decision. The fully automatic techniques presented in this paper can efficiently reach or come near to the maximal abstraction efficiency. First, a fine-grain abstraction approach is given to keep the abstraction granularity small by breaking down large combinational logic cones with Boolean network variables (BNVs) and then treating both state variables and BNVs as atoms in abstraction. Second, a refinement algorithm is proposed based on an improved Ariadne's bundle In the legend of Theseus, Ariadne's bundle contained one ball of thread to help Theseus navigate the labyrinth. In this paper, we work with multiple threads-hence, the "improved." of synchronous onion rings on the abstract model, through which the transitions contain all shortest abstract counterexamples. The synchronous onion rings are exploited in two distinct ways to provide global guidance to the abstraction refinement process. The scalability of our algorithm is ensured in the sense that all the analysis and computation required in our refinement algorithm are conducted on the abstract model. Finally, we derive sequential don't cares from the invisible variables and use them to constrain the behavior of the abstract model. We conducted experimental comparisons of our new method with various existing techniques. The results show that our method outperforms other counterexample-guided methods in terms of both run time and abstraction efficiency

Finding all satisfying assignments of a propositional formula has many applications in the design of hardware and software. An approach to this problem augments a clause-recording propositional satisfiability solver with the ability to add blocking clauses, which prevent the solver from visiting the same solution more than once. One generates a blocking clause from a satisfying assignment by taking its complement. In this paper, we present an improved algorithm for finding all satisfying assignments for a generic Boolean circuit. An optimization based on lifting-which generates minimal satisfying assignments-yields prime blocking clauses. Thanks to the primality of the blocking clauses, the derived conflict clauses usually prune both satisfiable and unsatisfiable points at once. The efficiency of our new algorithm is demonstrated by our preliminary results on SAT-based unbounded model checking.

Bounded Model Checking (BMC) relies on solving a sequence of highly correlated Boolean satisfiability (SAT) problems, each of which checks for the existence of counter-examples of a bounded length. The performance of SAT search depends heavily on the variable decision ordering. We propose an algorithm to exploit the correlation among different SAT problems in BMC, by predicting and successively refining a partial variable ordering. This ordering is based on the analysis of all previous unsatisfiable instances, and is combined with the SAT solver's existing decision heuristic to determine the final variable decision ordering. Experiments on real designs from industry show that our new method improves the performance of SAT-based BMC significantly.

We propose an abstraction refinement method for invariant checking, which is based on the simultaneous analysis of all abstract counter examples of shortest length in the current abstraction. The algorithm is focused on an improved Ariadne's Bundle/sup 1/ of SORs (Synchronous Onion Rings) of the abstract model; the transitions through these SORs contain all shortest ACEs (Abstract Counter Examples) and no other ACEs. The SORs are exploited in two distinct ways to provide global guidance to the abstraction refinement process: (1) Refinement variable selection is based on the entirety of transitions connecting the SORs, and (2) a SAT-based concretization test is formulated to test all ACEs in the SORs at once. We call this test multi-thread concretization. The scalability of our refinement algorithm is ensured in the sense that all the analysis and computation required in our refinement algorithm are conducted on the abstract model. The abstraction efficiency of a given abstraction refinement algorithm measures how much of the concrete model is required to make the decision. We include experimental comparisons of our new method with recently published techniques. The results show that our scalable method, based on global guidance from the entire bundle of shortest ACEs, outperforms these other methods in terms of both run time and abstraction efficiency.

In this paper, we present CubicPower which is a dynamic power estimator based on Verilog/VHDL simulators.We propose the power characterieation model and the probablistic contribution measure(PCM) algorithm to calculate the actual power consumption of cell instances with given switching information.In addition to PCM, the state dependency and non-switching activity of gates are taken into account for more accurate power estimation.Experimental results of CubicPower show less than 10% error compared with the results of PowerMill simulation and the measured values of the IMS test equipment.Due to the PCM algorithm, CubicPower is more accurate than the leading commercial dynamic power estimator at the gate level and is 2-3 orders of magnitude faster than PowerMill.