Journal on Satisfiability, Boolean Modeling and Computation - Volume 8, issue 1-2

Authors: Griggio, Alberto

Article Type: Research Article

Abstract: We present a detailed description of a theory solver for Linear Integer Arithmetic ( LA ( Z ) ) in a lazy SMT context. Rather than focusing on a single technique that guarantees theoretical completeness, the solver makes extensive use of layering and heuristics for combining different techniques in order to achieve good performance in practice. The viability of our approach is demonstrated by an empirical evaluation on a wide range of benchmarks, showing significant performance improvements over current state-of-the-art solvers.

Keywords: SMT, linear integer arithmetic, decision procedures

DOI: 10.3233/SAT190086

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 8, no. 1-2, pp. 1-27, 2012

Authors: Alberti, Francesco | Ghilardi, Silvio | Pagani, Elena | Ranise, Silvio | Paolo Rossi, Gian

Article Type: Research Article

Abstract: Model Checking Modulo Theories is a recent approach for the automated verification of safety properties of a class of infinite state systems manipulating arrays, called array-based systems. The idea is to repeatedly compute pre-images of a set of (unsafe) states by using certain classes of first-order formulae representing sets of states and transitions, and then reduce fix-point checks to Satisfiability Modulo Theories problems. Unfortunately, if the guards contain universally quantified index variables, the backward procedure cannot be fully automated. In this paper, we overcome the problem by describing a syntactic transformation on array-based systems, which can be seen as an …instance of the well-known operation of relativization of quantifiers in first-order logic. Interestingly, when specifying and verifying distributed systems, the proposed syntactic transformation can be interpreted as the adoption of the crash-failure model, which is well-known in the literature of fault-tolerant systems. By eliminating universal quantifiers from guards, the transformation significantly extends the scope of applicability of the symbolic backward reachability procedure. To provide empirical evidence of this claim, we discuss our findings in applying the proposed technique to a significant case-study in the verification of some classical algorithms for reliable broadcast. Show more

Keywords: model checking modulo theories, failure models, quantifiers instantiation, reliable broadcast

DOI: 10.3233/SAT190087

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 8, no. 1-2, pp. 29-61, 2012

Authors: Wild, Marcel

Article Type: Research Article

Abstract: While it was known that all models of a Horn formula can be generated in output-polynomial time, here we present an explicit algorithm as opposed to the rather vague oracle-scheme suggested in the proof of [6, Thm.4]. It is an instance of some principle of exclusion that compactly (thus not one by one) generates all models of certain Boolean formulae given in CNF. The principle of exclusion can be adapted to generate only the models of weight k . We compare and contrast it with constraint programming, 0, 1 integer programming, and binary decision diagrams.

Keywords: Horn-models, output-polynomial algorithm, fixed-cardinality models

DOI: 10.3233/SAT190088

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 8, no. 1-2, pp. 63-82, 2012

Authors: Chen, Huan | Marques-Silva, Joao

Article Type: Research Article

Abstract: Automatic Test Pattern Generation (ATPG) is arguably one of the practical applications that motivated the development of modern Boolean Satisfiability (SAT) solvers in the mid 90s. Despite the interest of using SAT in ATPG, the original model remained mostly unchanged for nearly two decades, even in the presence of renewed interest in applying modern SAT technology to large-scale hardware designs. This paper describes the SAT-based ATPG system TG-Pro . In contrast to all SAT-based ATPG work over the last two decades, TG-Pro is based on a new fundamentally different SAT-based ATPG model. Experimental results, obtained on well-known and publicly …available benchmarks, demonstrate that TG-Pro achieves major performance improvements over other well-established SAT-based ATPG models. Show more

Keywords: ATPG, Boolean SAT, EDA

DOI: 10.3233/SAT190089

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 8, no. 1-2, pp. 83-88, 2012

Authors: Janota, Mikoláš | Lynce, Inês | Manquinho, Vasco | Marques-Silva, Joao

Article Type: Research Article

Abstract: This paper presents PackUp (http://sat.inesc-id.pt/~mikolas/sw/packup ). (PACKage UPgradability with Boolean formulations) a framework for solving the the software package upgradability problem . Earlier versions of the framework (cudf2msu , cudf2pbo ) participated in the 3rd MISC-live, an international competition organized by the European project MANCOOSI. The framework encodes the problem as a weighted partial MaxSAT formula and invokes a dedicated solver to solve the formula. The framework supports two types of solvers: weighted partial MaxSAT solvers and optimization pseudo-Boolean (OPB) solvers. The paper discusses the design of the framework and the specifics of the problem encoding.

Keywords: package upgradability problem, MaxSAT, Boolean optimization

DOI: 10.3233/SAT190090

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 8, no. 1-2, pp. 89-94, 2012

Authors: Koshimura, Miyuki | Zhang, Tong | Fujita, Hiroshi | Hasegawa, Ryuzo

Article Type: Research Article

Abstract: We present a partial Max-SAT solver QMaxSAT which uses CNF encoding of Boolean cardinality constraints. The old version 0.1 was obtained by adapting a CDCL based SAT solver MiniSat to manage cardinality constraints. It was placed first in the industrial subcategory and second in the crafted subcategory of partial Max-SAT category of the 2010 Max-SAT Evaluation. The new version 0.2 is obtained by modifying version 0.1 to decrease the number of clauses for the cardinality encoding. We compare the two versions by solving Max-SAT instances taken from the 2010 Max-SAT Evaluation.

Keywords: partial Max-SAT solver, Boolean cardinality constraints, CDCL solver

DOI: 10.3233/SAT190091

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 8, no. 1-2, pp. 95-100, 2012

Authors: Bubeck, Uwe | Kleine Büning, Hans

Article Type: Research Article

Abstract: In this paper, we consider the problem of compactly representing nested instantiations of propositional subformulas with different arguments as quantified Boolean formulas (QBF). We develop a generic QBF encoding pattern which combines and generalizes existing QBF encoding techniques for simpler types of redundancy. We obtain an equivalence-preserving transformation in linear time from the PSPACE-complete language of nested Boolean functions (NBF), also called Boolean programs, to prenex QBF. A transformation in the other direction from QBF to NBF is also possible in at most quadratic time by simulating quantifier expansion.

Keywords: nested Boolean function, NBF, QBF, Boolean program, encoding

DOI: 10.3233/SAT190092

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 8, no. 1-2, pp. 101-116, 2012