62642642
GRASP—a new search algorithm for satisfiability
This paper introduces GRASP (Generic seaRch Algorithm for the Satisfiability Problem), an integrated algorithmic framework for SAT that unifies several previously proposed search-pruning techniques and facilitates identification of additional ones. GRASP is premised on the inevitability of conflicts during search and its most distinguishing feature is the augmentation of basic backtracking search with a powerful conflict analysis procedure. Analyzing conflicts to determine their causes enables GRASP to backtrack non-chronologically to earlier levels in the search tree, potentially pruning large portions of the search space. In addition, by "recording" the causes of conflicts, GRASP can recognize and preempt the occurrence of similar conflicts later on in the search. Finally, straightforward bookkeeping of the causality chains leading up to conflicts allows GRASP to identify assignments that are necessary for a solution to be found. Experimental results obtained from a large number of benchmarks, including many from the field of test pattern generation, indicate that application of the proposed conflict analysis techniques to SAT algorithms can be extremely effective for a large number of representative classes of SAT instances.
195711464
Efficient data structures for backtrack search SAT solvers
The implementation of efficient Propositional Satisfiability (SAT) solvers entails the utilization of highly efficient data structures, as illustrated by most of the recent state-of-the-art SAT solvers. However, it is in general hard to compare existing data structures, since different solvers are often characterized by fairly different algorithmic organizations and techniques, and by different search strategies and heuristics. This paper aims the evaluation of data structures for backtrack search SAT solvers, under a common unbiased SAT framework. In addition, advantages and drawbacks of each existing data structure are identified. Finally, new data structures are proposed, that are competitive with the most efficient data structures currently available, and that may be preferable for the next generation SAT solvers.
12142779
On Applying Cutting Planes in DLL-Based Algorithms for Pseudo-Boolean Optimization
The utilization of cutting planes is a key technique in Integer Linear Programming (ILP). However, cutting planes have seldom been applied in Pseudo-Boolean Optimization (PBO) algorithms derived from the Davis-Logemann-Loveland (DLL) procedure for Propositional Satisfiability (SAT). This paper proposes the utilization of cutting planes in a DLL-style PBO algorithm, which incorporates the most effective techniques for PBO. We propose the utilization of cutting planes both during preprocessing and during the search process. Moreover, we also establish conditions that enable clause learning and non-chronological backtracking in the presence of conflicts involving constraints generated by cutting plane techniques. The experimental results, obtained on a large number of classes of instances, indicate that the integration of cutting planes with backtrack search is an extremely effective technique for PBO.
8449764
Breaking Symmetries in SAT Matrix Models
Symmetry occurs naturally in many computational problems. The use of symmetry breaking techniques for solving search problems reduces the search space and therefore is expected to reduce the search time. Recent advances in breaking symmetries in SAT models are mainly focused on the identification of permutable variables via graph automorphism. These symmetries are denoted as instance-dependent, and although shown to be effective for different problem instances, the advantages of their generalised use in SAT are far from clear. Indeed, in many cases symmetry breaking predicates can introduce significant computational overhead, rendering ineffective the use of symmetry breaking. In contrast, in other domains, symmetry breaking is usually achieved by identifying instance-independent symmetries, often with promising experimental results. This paper studies the use of instance-independent symmetry breaking predicates in SAT. A concrete application is considered, and techniques for symmetry breaking in matrix models from CP are used. Our results indicate that instance-independent symmetry breaking predicates for matrix models can be significantly more effective than instance-dependent symmetry breaking predicates.
14843099
Heuristic-Based Backtracking for Propositional Satisfiability
In recent years backtrack search algorithms for Propositional Satisfiability (SAT) have been the subject of dramatic improvements. These improvements allowed SAT solvers to successfully solve instances with thousands of variables and hundreds of thousands of clauses, and also motivated the development of many new challenging problem instances, many of which still too hard for the current generation of SAT solvers. As a result, further improvements to SAT technology are expected to have key consequences in solving hard real-world instances. The objective of this paper is to propose heuristic approaches to the backtrack step of backtrack search SAT solvers, with the goal of increasing the ability of a SAT solver to search different parts of the search space. The proposed heuristics are inspired by the heuristics proposed in recent years for the branching step of SAT solvers, namely VSIDS and some of its improvements. Moreover, the completeness of the new algorithm is guaranteed. The preliminary experimental results are promising, and motivate the integration of heuristic backtracking in state-of-the-art SAT solvers.
15163719
Solving satisfiability in combinational circuits
As EDA evolves, researchers continue to find modeling tools to solve problems of test generation, design verification, logic, and physical synthesis, among others. One such modeling tool is Boolean satisfiability (SAT), which has very broad applicability in EDA. The authors review modern SAT algorithms, show how these algorithms can account for structural information in combinational circuits, and explain what recursive learning can add to SAT.
14688474
A processor for testing mixed-signal cores in system-on-chip
This paper describes the design of a processor specific for testing cores embedded in system-on-chip. This processor, which can be implemented within a system's reconfigurable area, shall be responsible for scheduling and control test operations and perform preliminary data processing, as well as to provide the interface with an external tester. Building these test operations on-chip allows for simplifying external tester interface and to reduce testing time. The testing procedure and the infrastructure required to test an A/D converter is described as an example.
42069370
An Experimental Evaluation of Coordinated Checkpointing in a Parallel Machine
Coordinated checkpointing represents a very effective solution to assure the continuity of distributed and parallel applications in the occurrence of failures. In previous studies it has been proved that this approach achieved better results than independent checkpointing and message logging. However, we need to know more about the real overhead of coordinated checkpointing and get sustained insights about the best way to implement this technique of fault-tolerance. This paper presents an experimental evaluation of coordinated checkpointing in a parallel machine. It describes some optimization techniques and presents some performance results.
540709
The performance of coordinated and independent checkpointing
Checkpointing is a very effective technique to tolerate the occurrence of failures in distributed and parallel applications. The existing algorithms in the literature are basically divided into two main classes: coordinated and independent checkpointing. This paper presents an experimental study that compares the performance of these two classes of algorithms. The main conclusion of our study is that coordinated checkpointing is more efficient than independent checkpointing and all the arguments against the performance of coordinated algorithms were not verified in practice.
7296321
Towards CNC Programming Using Haskell
Recent advances in Computerized Numeric Control (CNC) have allowed the manufacturing of products with high quality standards. Since CNC programs consist of a series of assembler-like instructions, several high-level languages (e.g., AutoLISP, APL, OMAC) have been proposed to raise the programming abstraction level. Unfortunately, the lack of a clean semantics prevents the development of formal tools for the analysis and manipulation of programs. In this work, we propose the use of Haskell for CNC programming. The declarative nature of Haskell provides an excellent basis to develop program analysis and manipulation tools and, most importantly, to formally prove their correctness.
33382273
Implementation of mixed current/voltage testing using the IEEE P1149.4 infrastructure
The development of a mixed-signal test bus infrastructure-IEEE P1149.4-is now in the final stages of the standardization process. Evaluating the test capabilities enabled by this infrastructure is an important step needed to support it as a well established standard. This paper presents experiments carried out with a test chip provided by the P1149.4 working group, which explore the architecture of the proposed analog boundary module to implement alternative testing methods. These include a method for parametric testing of passive components based on the monitoring of the power supply current, and a mixed current/voltage technique allowing the implementation of correlation for testing analog and mixed-signal macros.