Journal on Satisfiability, Boolean Modeling and Computation - Volume 5, issue 1-4

Authors: Velev, Miroslav N.

Article Type: Editorial

DOI: 10.3233/SAT190049

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 5, no. 1-4, pp. i-iii, 2009

Authors: Safarpour, Sean | Veneris, Andreas | Drechsler, Rolf

Article Type: Research Article

Abstract: The dramatic performance improvements of SAT solvers over the past decade have increased their deployment in hardware verification applications. Many problems that were previously too large and complex for SAT techniques can now be handled in an efficient manner. One such problem is reachability analysis, whose instances are found throughout verification applications such as unbounded model checking and trace reduction. In circuit-based reachability analysis important circuit information is often lost during the circuit-to-SAT translation process. Observability Don’t Cares (ODCs) are an example of such information that can potentially help achieve better and faster results for the SAT solver. This work …proposes to use the ODCs to improve the quality and performance of SAT-based reachability analysis frameworks. Since ODCs represent variables whose values do not a ect the outcome of a problem, it is possible to satisfy a problem with fewer assigned variables. This in turn leads to more compact solutions and thus fewer solutions to cover the entire solution space. Specifically, this work presents an efficient way to identify ODCs, proves the correctness of leaving ODC variables unassigned, and develops a reachability analysis platform that benefits greatly from the ODCs. The advantages of using ODCs in reachability analysis is demonstrated through extensive experiments on unbounded model checking and trace reduction applications. Show more

Keywords: SAT solver, reachability analysis, model checking, observability don’t cares

DOI: 10.3233/SAT190050

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 5, no. 1-4, pp. 1-25, 2009

Authors: Esparza, Javier | Kiefer, Stefan | Schwoon, Stefan

Article Type: Research Article

Abstract: Counterexample-guided abstraction refinement (CEGAR) has proven to be a powerful method for software model checking. In this paper, we investigate this concept in the context of sequential (possibly recursive) programs whose statements are given as Binary Decision Diagrams (BDDs). We examine how Craig interpolants can be computed efficiently in this case and propose a new special type of interpolants. Moreover, we show how to treat multiple counterexamples in one refinement cycle. We have implemented this approach within the model checker Moped and report on experiments.

Keywords: model-checking, abstraction refinement, Craig interpolation, BDDs, push-down systems

DOI: 10.3233/SAT190051

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 5, no. 1-4, pp. 27-56, 2009

Authors: Fujita, Masahiro | Seto, Kenshu | Sakunkonchak, Thanyapat

Article Type: Research Article

Abstract: Program slicing is a software-analysis technique that generates System Dependence Graphs (SDGs) by which dependencies among program statements can be identified through their traversal. We have developed a program slicing tool for SpecC, a C-based system level design language for hardware/software co-designs, on top of a program slicer for C/C++. This program slicing tool can generate SDGs from any combined descriptions in C, C++, and SpecC, and can be used to analyze design descriptions for hardware/software co-designs uniformly and smoothly in all the combined descriptions. In this paper, after reviewing our program slicer that generates SDGs, we present verification and …synthesis techniques for hardware/software co-designs through various analyses on SDGs and generations of SAT/ILP problems from them. For analysis and verification of the combined descriptions, we examine SDGs statically by traversing them with SAT/ILP solvers as verification engines. With this method, many static checks can be efficiently realized even if the target design descriptions are fairly large. We first present techniques for checking synchronization among concurrent processes described in SpecC through symbolic analysis on SDGs. The techniques could verify the synchronization of MPEG4 descriptions with about 48,000 lines within 10 seconds. The techniques can be applied to automatic conversions between sequential and parallel computations. One such application to automatic program serialization is presented. By using the technique for automatic program serialization, we could serialize Vocoder descriptions with about 10,000 lines in around 1 minute. As for synthesis from the combined descriptions, we present an optimal code generation method based on SAT formulation. It can generate codes for reconfigurable processors with minimum code lengths. The sizes of problems as SAT formulation range from 10,000 to 100,000 variables and 100,000 to 500,000 clauses for the largest configurations. With appropriate uses of the state-of-the-art SAT solvers and related tools, we show that fairly practical sizes of verification and synthesis problems can be solved by analyzing SDGs generated from the combined descriptions. Show more

Keywords: SAT-solver, lookahead, equivalence reasoning, local learning

DOI: 10.3233/SAT190052

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 5, no. 1-4, pp. 57-82, 2009

Authors: Bruno, Viviana | Garcia, Luz | Nocco, Sergio | Quer, Stefano

Article Type: Research Article

Abstract: Scheduling, or planning, is widely recognized as a very important step in several domains such as high level synthesis, real-time systems, and every-day applications. Given a problem described by a number of actions and their relationships, finding a schedule, or a plan, means to find a way to perform all the actions minimizing a specific cost function. The goal of this paper is to develop, analyze and compare different scheduling techniques on a new scheduling/planning problem. The new application domain is aircraft maintenance. It shares with previous ones the underlying problem definition, but it also unveils brand new challenging …characteristics, and a different optimization target. We show how to model the problem in a suitable way, and how to solve it with different methodologies going from Satisfiability solvers and Binary Decision Diagrams, to Timed Automata and Coloured Petri Nets. New ideas are put forward in the different domains having efficiency and scalability as main targets. Experimental results stress the different techniques, showing their application range and limits, and defining advantages and disadvantages of the underlying models. Overall, general-purpose tools have been easily applied to our problem, but failed as far as efficiency was concerned. The satisfiability-based approach proved to be faster and more scalable, being able to solve instances 3–4 times larger. To sum up, our contributions range from modeling the aircraft maintenance problem as a scheduling instance, to coding this problem with home-made and general-purpose tools, to dovetailing exact and heuristic techniques, and comparing these techniques in terms of efficiency and scalability. Show more

Keywords: Boolean satisfiability, SAT-solvers, timed automata, Petri nets, scheduling, planning

DOI: 10.3233/SAT190053

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 5, no. 1-4, pp. 83-110, 2009

Authors: Nocco, Sergio | Quer, Stefano

Article Type: Research Article

Abstract: In both the hardware and the software domains, non-canonical circuit-based state set representations have recently been the subject of intensive investigations. One of the limiting factors of these representations has been the difficulty to control their size during key operations. For example, existentially and universally quantifying a variable implies doubling the circuit size in the worst case. In this paper, we present a probabilistic approach to keep under control the size of circuit-based representations when manipulating them. Every time a formula is becoming too cumbersome, we estimate it instead of building the exact result. The nature of the estimate, …i.e., under- or over-approximation, depends on the problem that is being computed. The key idea of this process is to boost the expressiveness of the formula, delivering a dense representation, i.e., a formula compact in size but more expressive for the given verification problem. Experimental results show decisive reductions in terms of circuit size, and an increase in terms of density, i.e., the ratio between the cardinality of the on-set of a formula and the size of its representation. We applied the strategy to Bounded Model Checkingm, and circuit-based backward Unbounded Model Checking. We present experimental results from applying the approach to hard-to-solve verification instances. We observed speedups of more than one order of magnitude in some cases. Show more

Keywords: and-inverter graph, Boolean satisfiability, SAT-solvers, model checking, density, controllability

DOI: 10.3233/SAT190054

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 5, no. 1-4, pp. 111-132, 2009

Authors: Benedetti, Marco | Mangassarian, Hratch

Article Type: Research Article

Abstract: The language of Quantified Boolean Formulas (QBF) has a lot of potential applications to Formal Verification (FV) tasks, as it captures many of these tasks in a natural and compact way. Practical experience has been disappointing though. When compared with contending approaches such as SAT, QBF-based FV has invariably yielded unfavorable experimental results. This paper makes two contributions. We first provide an account of the status quo in QBF-based FV. We examine commonly adopted formalizations and the relative strengths of different decision procedures. In the second part of this paper, we investigate for the first time the relevance of …some advanced QBF techniques to FV tasks. In particular, we describe the use and the benefits of restricted quantifiers, QBF certificates, alternative encodings for classical model checking problems, and encodings with free variables. These promising research perspectives seem to reverse the negative standing of QBF applied to FV, as confirmed by the experimental evidence we discuss. Experiments are conducted by extending the publicly available solver sKizzo in several ways, and they include the first case studies where QBF compares favorably to SAT, its traditional competitor. QBF turns out to be an order of magnitude faster than SAT in some tasks (e.g., automated design debugging of large circuits). Moreover, as the size of the problems grows, the SAT encodings result in excessive memory requirements leading to out-of-memory conditions, while the more compact QBF encodings continue to be manageable and solvable. Show more

Keywords: quantified Boolean formulas, formal verification, empirical evaluation

DOI: 10.3233/SAT190055

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 5, no. 1-4, pp. 133-191, 2009

Authors: Codish, Michael | Lagoon, Vitaly | Stuckey, Peter J.

Article Type: Research Article

Abstract: This paper introduces a propositional encoding for lexicographic path orders (LPOs) and the corresponding LPO termination property of term rewrite systems. Given this encoding, termination analysis can be performed using a state-of-the-art Boolean satisfiability solver. Experimental results are unequivocal, indicating orders of magnitude speedups in comparison with previous implementations for LPO termination. The results of this paper have already had a direct impact on the design of several major termination analyzers for term rewrite systems. The contribution builds on a symbol-based approach towards reasoning about partial orders. The symbols in an unspecified partial order are viewed as variables that take …integer values and are interpreted as indices in the order. For a partial order statement on n symbols, each index is represented in ⌈ log 2 n ⌉ propositional variables and partial order constraints between symbols are modeled on the bit representations. The proposed encoding is general and relevant to other applications which involve propositional reasoning about partial orders. Show more

Keywords: Boolean satisfiability, lexicographic path orders, proving termination, term rewrite systems

DOI: 10.3233/SAT190056

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 5, no. 1-4, pp. 193-215, 2009

Authors: Goldberg, Eugene

Article Type: Research Article

Abstract: Most successful systematic SAT-solvers are descendants of the DPLL procedure and so operate on partial assignments. Using partial assignments is explained by the “enumerative semantics” of the DPLL procedure. Current clause learning SAT-solvers, in a sense, have outgrown this semantics. Instead of enumerating the search space as the DPLL procedure does, they explicitly build a resolution proof. In this paper, we suggest a semantics that, in our opinion, is more suitable for clause learning SAT-solvers. The idea is to consider a set of complete assignments not just as a part of the search space but as an “encryption” of a …resolution proof or a part thereof. Importantly, a set of points encrypting a resolution proof can be dramatically smaller than the entire search space. We introduce a resolution based SAT-solver with clause learning called FI (short for Find point Image of a proof) that is inspired by the new semantics. FI operates on complete assignments. We compare our naive implementation of FI with Minisat and BerkMin . Experiments show that FI is competitive with Minisat and BerkMin in terms of backtracks. In terms of performance, FI is slower than Minisat and BerkMin for small CNF formulas. On the other hand, even the current primitive implementation of FI is competitive with Minisat and BerkMin on large Bounded Model Checking formulas due to its superior decision making. Show more

Keywords: SAT-solver, resolution, decision-making, local search, complete assignment

DOI: 10.3233/SAT190057

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 5, no. 1-4, pp. 217-242, 2009

Authors: Fang, Lei | Hsiao, Michael S.

Article Type: Research Article

Abstract: Due to the widespread demands for efficient SAT solvers in Electronic Design Automation applications, methods to boost the performance of the SAT solver are highly desired. We propose a Hybrid Solution to boost SAT solver performance in this paper, via an integration of local and DPLL-based search approaches. A local search is used to identify a subset of clauses from the original formula to be passed to a DPLL SAT solver incrementally until all the clauses have been passed. In addition, the solution obtained by the DPLL solver on the subset of clauses is fed back to the local search …solver to jump over any locally optimal points. The proposed solution is highly portable to the existing SAT solvers. For satisfiable instances, up to an order of magnitude speedup was obtained via the proposed hybrid solver. For unsatisfiable instances, the speedup was smaller due to the overhead. Show more

Keywords: satisfiability, DPLL, WalkSAT, hybrid

DOI: 10.3233/SAT190058

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 5, no. 1-4, pp. 243-261, 2009