10515113
Validating SAT solvers using an independent resolution-based checker: practical implementations and other applications
As the use of SAT solvers as core engines in EDA applications grows, it becomes increasingly important to validate their correctness. In this paper, we describe the implementation of an independent resolution-based checking procedure that can check the validity of unsatisfiable claims produced by the SAT solver zchaff. We examine the practical implementation issues of such a checker and describe two implementations with different pros and cons. Experimental results show low overhead for the checking process. Our checker can work with many other modern SAT solvers with minor modifications, and it can provide information for debugging when checking fails. Finally we describe additional results that can be obtained by the validation process and briefly discuss their applications.
6941919
Optimizations for Compiling Declarative Models into Boolean Formulas
Advances in SAT solver technology have enabled many automated analysis and reasoning tools to reduce their input problem to a SAT problem, and then to use an efficient SAT solver to solve the underlying analysis or reasoning problem. The solving time for SAT solvers can vary substantially for semantically identical SAT problems depending on how the problem is expressed. This property motivates the development of new optimization techniques whose goal is to produce more efficiently solvable SAT problems, thereby improving the overall performance of the analysis or reasoning tool. 
 
This paper presents our experience using several mechanical techniques that enable the Alloy Analyzer to generate optimized SAT formulas from first-order logic formulas. These techniques are inspired by similar techniques from the field of optimizing compilers, suggesting the potential presence of underlying connections between optimization problems from two very different domains. Our experimental results show that our techniques can deliver substantial performance improvement results—in some cases, they reduce the solving time by an order of magnitude.
6311626
Combining strengths of circuit-based and CNF-based algorithms for a high-performance SAT solver
We propose Satisfiability Checking (SAT) techniques that lead to a consistent performance improvement of up to 3x over state-of-the-art SAT solvers like Chaff on important problem domains in VLSI CAD. We observe that in circuit oriented applications like ATPG and verification, different software engineering techniques are required for the portions of the formula corresponding to learnt clauses compared to the original formula. We demonstrate that by employing the same innovations as in advanced CNF-based SAT solvers, but in a hybrid approach where these two portions of the formula are represented differently and processed separately, it is possible to obtain the consistently highest performing SAT solver for circuit oriented problem domains. We also present controlled experiments to highlight where these gains come from. Once it is established that the hybrid approach is faster, it becomes possible to apply low overhead circuit-based heuristics that would be unavailable in the CNF domain for greater speedup.
6908840
Vigilante: end-to-end containment of internet worms
Worm containment must be automatic because worms can spread too fast for humans to respond. Recent work has proposed network-level techniques to automate worm containment; these techniques have limitations because there is no information about the vulnerabilities exploited by worms at the network level. We propose Vigilante, a new end-to-end approach to contain worms automatically that addresses these limitations. Vigilante relies on collaborative worm detection at end hosts, but does not require hosts to trust each other. Hosts run instrumented software to detect worms and broadcast self-certifying alerts (SCAs) upon worm detection. SCAs are proofs of vulnerability that can be inexpensively verified by any vulnerable host. When hosts receive an SCA, they generate filters that block infection by analysing the SCA-guided execution of the vulnerable software. We show that Vigilante can automatically contain fast-spreading worms that exploit unknown vulnerabilities without blocking innocuous traffic.
14199573
Zapato: Automatic Theorem Proving for Predicate Abstraction Refinement
Counterexample-driven abstraction refinement is an automatic process that produces abstract models of finite and infinite-state systems. When this process is applied to software, an automatic theorem prover for quantifier-free first-order logic helps to determine the feasibility of program paths and to refine the abstraction. In this paper we report on a fast, lightweight, and automatic theorem prover called Zapato which we have built specifically to solve the queries produced during the abstraction refinement process.
70202123
The Quest for Efficient Boolean Satisfiability Solvers
The classical NP-complete problem of Boolean Satisfiability (SAT) has seen much interest in not just the theoretical computer science community, but also in areas where practical solutions to this problem enable significant practical applications. Since the first development of the basic search based algorithm proposed by Davis, Putnam, Logemann and Loveland (DPLL) about forty years ago, this area has seen active research effort with many interesting contributions that have culminated in state-of-the-art SAT solvers today being able to handle problem instances with thousands, and in same cases even millions, of variables. In this paper we examine some of the main ideas along this passage that have led to our current capabilities. Given the depth of the literature in this field, it is impossible to do this in any comprehensive way; rather we focus on techniques with consistent demonstrated efficiency in available solvers. For the most part, we focus on techniques within the basic DPLL search framework, but also briefly describe other approaches and look at some possible future research directions.
18465833
Contract-based mutation for testing components
Testing plays an important role in the maintenance of component based software development. Test adequacy for component testing is one of the hardest issues for component testing. To tackle this problem, it is a natural idea to apply mutation testing, which is a fault-based testing method used for measuring test adequacy, for component contracts, whose aim is to improve the testability of the component. Though powerful, mutation testing is usually very computation-expensive, as many mutants need to be produced and executed in mutation testing. In this paper, we propose a contract-based mutation technique for testing components. Based on the discordance between contracts and specification, our approach employs a set of high level contract mutation operators. The experimental results show that these operators can greatly reduce the number of mutants compared with traditional mutation operators. At the same time, the contract-based mutation using our contract mutation operators can provide almost the same ability as that of using traditional mutation operators. Moreover, effective test suite can be produced to reduce the maintenance effort.
6035916
Ranking web objects from multiple communities
Vertical search is a promising direction as it leverages domain-specific knowledge and can provide more precise information for users. In this paper, we study the Web object-ranking problem, one of the key issues in building a vertical search engine. More specifically, we focus on this problem in cases when objects lack relationships between different Web communities, and take high-quality photo search as the test bed for this investigation. We proposed two score fusion methods that can automatically integrate as many Web communities (Web forums) with rating information as possible. The proposed fusion methods leverage the hidden links discovered by a duplicate photo detection algorithm, and aims at minimizing score differences of duplicate photos in different forums. Both intermediate results and user studies show the proposed fusion methods are practical and efficient solutions to Web object ranking in cases we have described. Though the experiments were conducted on high-quality photo ranking, the proposed algorithms are also applicable to other ranking problems, such as movie ranking and music ranking.
9614158
Edge choosability of planar graphs without small cycles
Abstract We investigate structural properties of planar graphs without triangles or without 4-cycles, and show that every triangle-free planar graph G is edge-( Δ ( G )+1)-choosable and that every planar graph with Δ ( G )≠5 and without 4-cycles is also edge-( Δ ( G )+1)-choosable.
24114295
WS-EPM: Web services for enterprise project management
This work presents a new service-oriented architecture for enterprise project management that integrates business process, human resources and project management within an enterprise or across the value chain network. In the proposed WS-EPM framework, the project resources include business processes, skilled people, physical resources, control policies, and so forth. The project resources used in WS-EPM are described by WSResource properties language. In addition, the coordination of project resources is guided by a set of operations modeled by business process execution language for Web services (BPEL4WS). At the end of this paper, we present an industry application scenario that leverages the proposed WS-EPM for achieving maximum ROI with limited resources.
9779472
H-Walk: hierarchical distance computation for moving convex bodies
This paper presents the Hierarchical Walk, or H-Walk algorithm, which maintains the distance between two moving convex bodies by exploiting both motion coherence and hierarchical representations. For convex polygons, we prove that H-Walk improves on the classic Lin-Canny and DobkinKirkpatrick algorithms. We have implemented H-Walk for moving convex polyhedra in three dimensions. Experimental results indicate that, unlike previous incremental distance computation algorithms, H-Walk adapts well to variable coherence in the motion.