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

Authors: Lafitte, Frédéric | Nakahara Jr, Jorge | Van Heule, Dirk

Article Type: Research Article

Abstract: This paper investigates the power of SAT solvers in cryptanalysis. The contributions are two-fold and are relevant to both theory and practice. First, we introduce an efficient, generic and automated method for generating SAT instances encoding a wide range of cryptographic computations. This method can be used to automate the first step of algebraic attacks, i.e. the generation of a system of algebraic equations. Second, we illustrate the limits of SAT solvers when attacking cryptographic algorithms, with the aim of finding weak keys in block ciphers and preimages in hash functions. SAT solvers allowed us to find, or prove the …absence of, weak-key classes under both differential and linear attacks of full-round block ciphers based on the International Data Encryption Algorithm (IDEA), namely, WIDEA-n for n ∈ { 4 , 8 } , and MESH-64(8). In summary: (i) we have found several classes of weak keys for WIDEA-n and (ii) proved that a particular class of weak keys does not exist in MESH-64(8). SAT solvers provided answers to two complementary open problems (presented in Fast Software Encryption 2009): the existence and non-existence of such weak keys. Although these problems were supposed to be difficult to answer, SAT solvers provided an efficient solution. We also report on experimental results about the performance of a modern SAT solver as the encoded cryptanalytic tasks become increasingly hard. The tasks correspond to preimage attacks on reduced MD4 algorithm. Show more

Keywords: SAT solvers, weak keys, preimage attacks, automated cryptanalysis, algebraic cryptanalysis

DOI: 10.3233/SAT190099

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 9, no. 1, pp. 1-25, 2014

Authors: Nadel, Alexander | Ryvchin, Vadim | Strichman, Ofer

Article Type: Research Article

Abstract: Various technologies are based on the capability to find small unsatisfiable cores given an unsatisfiable CNF formula, i.e., a subset of the clauses that are unsatisfiable regardless of the rest of the formula. If that subset is irreducible, it is called a Minimal Unsatisfiable Core (MUC). In many cases, the MUC is required not in terms of clauses, rather in terms of a preknown user-given set of high-level constraints , where each such constraint is a conjunction of clauses. We call the problem of minimizing the participation of such constraints high-level minimal unsatisfiable core (HLMUC) extraction. All the current …state-of-the-art tools for MUC- and HLMUC-extraction are deletion-based , which means that they iteratively try to delete clauses from the core. We propose nine optimizations to this general strategy, although not all apply to both MUC and HLMUC. For both cases we achieved over a 2X improvement in run time comparing to the state-of-the-art and a reduction in the core size, when applied to a benchmark set consisting of hundreds of industrial test cases. These techniques are implemented in our award-winning solvers HaifaMUC and HaifaHLMUC . Show more

Keywords: Minimal Unsat Core, Minimal High-Level Unsat Core, Resolution

DOI: 10.3233/SAT190100

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 9, no. 1, pp. 27-51, 2014

Authors: Niemetz, Aina | Preiner, Mathias | Biere, Armin

Article Type: Research Article

Abstract: In this paper, we discuss the most important changes and new features introduced with version 2.0 of our SMT solver Boolector, which placed first in the QF_BV and QF_ABV tracks of the SMT competition 2014. We further outline some features and techniques that were not yet described in the context of Boolector.

Keywords: SMT solving, Lemmas on Demand, Lambdas, Don’t Care Reasoning

DOI: 10.3233/SAT190101

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 9, no. 1, pp. 53-58, 2014

Authors: Martins, Ruben | Joshi, Saurabh | Manquinho, Vasco | Lynce, Inês

Article Type: Research Article

Abstract: In recent years, unsatisfiability-based algorithms have become prevalent as state of the art for solving industrial instances of Maximum Satisfiability (MaxSAT). These algorithms perform a succession of unsatisfiable SAT solver calls until an optimal solution is found. In several of these algorithms, cardinality or pseudo-Boolean constraints are extended between iterations. However, in most cases, the formula provided to the SAT solver in each iteration must be rebuilt and no knowledge is reused from one iteration to the next. This paper describes how to implement incremental unsatisfiability-based algorithms for MaxSAT. In particular, we detail and analyze our implementation of the …MSU3 algorithm in the open-wbo framework that performed remarkably well in the MaxSAT Evaluation of 2014. Furthermore, we also propose to extend incrementality to weighted MaxSAT through an incremental encoding of pseudo-Boolean constraints. The experimental results show that the performance of MaxSAT algorithms can be greatly improved by exploiting the learned information and maintaining the internal state of the SAT solver between iterations. Finally, the proposed incremental encodings of cardinality and pseudo-Boolean constraints are not exclusive for MaxSAT usage and can be used in other domains. Show more

Keywords: Maximum Satisfiability, Unsatisfiability-based Algorithm, Incremental Encoding

DOI: 10.3233/SAT190102

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 9, no. 1, pp. 59-81, 2014

Authors: Janota, Mikoláš

Article Type: Research Article

Abstract: The main motivation behind the MaxSAT solver MiFuMax is twofold. It provides a baseline implementation of core-based algorithms for both weighted and unweighted MaxSAT. Such baseline implementation may serve for evaluation of evolving solvers. MiFuMax is written in literate programming and as such is instructive for anyone interested in learning about the implementation of modern core-based MaxSAT solvers. Despite its educative background, the solver has placed 1st in the Unweighted Max-SAT-Industrial track of the 2013 MaxSAT Evaluation and it has been successfully applied in other research.

Keywords: MaxSAT, SAT, Literate programming

DOI: 10.3233/SAT190103

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 9, no. 1, pp. 83-88, 2014

Authors: Abramé, André | Habet, Djamal

Article Type: Research Article

Abstract: Branch and bound (BnB) solvers for Max-SAT count at each node of the search tree the number of disjoint inconsistent subsets to compute the lower bound. In the last ten years, important advances have been made regarding the lower bound computation. Unit propagation based methods have been introduced to detect inconsistent subsets and a resolution-like inference rules have been proposed which allow a more efficient and incremental lower bound computation. We present in this paper our solver ahmaxsat , which uses these new methods and improves them in several ways. The main specificities of our solver over the state of …the art are: a new unit propagation scheme which considers all the variable propagation sources; an extended set of patterns which increase the amount of learning performed by the solver; a heuristic which modifies the order of application of the max-resolution rule when transforming inconsistent subset; and a new inconsistent subset treatment method which improves the lower bound estimation. All of them have been published in recent international conferences. We describe these four main components and we give a general overview of ahmaxsat , with additional implementation details. Finally, we present the result of the experimental study we have conducted. We first evaluate the impact of each component on ahmaxsat performance before comparing our solver to some of the current best performing complete Max-SAT solvers. The results obtained confirm the ones of the Max-SAT Evaluation 2014 where ahmaxsat was ranked first in three of the nine categories. Show more

Keywords: Max-SAT, branch and bound, max-resolution

DOI: 10.3233/SAT190104

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 9, no. 1, pp. 89-128, 2014

Authors: Morgado, Antonio | Ignatiev, Alexey | Marques-Silva, Joao

Article Type: Research Article

Abstract: Maximum Satisfiability (MaxSAT ) is a well-known optimization version of Propositional Satisfiability (SAT ) that finds a wide range of practical applications. This work describes and evaluates the Maximum Satisfiability using the Core-Guided approach solver (MSCG ), which is a robust MaxSAT solver that participated in the MaxSAT Evaluation 2014.

Keywords: maximum satisfiability, core-guided, Boolean optimization

DOI: 10.3233/SAT190105

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 9, no. 1, pp. 129-134, 2014

Authors: Cabodi, Gianpiero | Loiacono, Carmelo | Palena, Marco | Pasini, Paolo | Patti, Denis | Quer, Stefano | Vendraminetto, Danilo | Biere, Armin | Heljanko, Keijo

Article Type: Research Article

Abstract: Model checkers and sequential equivalence checkers have become essential tools for the semiconductor industry in recent years. The Hardware Model Checking Competition (HWMCC) was founded in 2006 with the purpose of intensifying research interest in these technologies, and establishing more of a science behind them. For example, the competition provided a standardized benchmark format, a challenging and diverse set of industrially-relevant public benchmarks, and, as a consequence, a significant motivation for additional research to advance the state-of-the-art in model checkers for these verification problems. This paper provides a historical perspective, and an analysis of the tools and benchmarks submitted to …the competition. It also presents a detailed analysis of the results collected in the 2014 edition of the contest, showing relations among tools, and among tools and benchmarks. It finally proposes a list of considerations, lessons learned, and hints for both future organizers and competitors. Show more

Keywords: Model Checking, Equivalence Checking, Binary Decision Diagrams, Satisfiability Solvers, Interpolation, IC3, Property Directed Reachability

DOI: 10.3233/SAT190106

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 9, no. 1, pp. 135-172, 2014

Authors: Sighireanu, Mihaela | Cok, David R.

Article Type: Research Article

Abstract: A competition of solvers for Separation Logic was held in May 2014, as an unofficial satellite event of the FLoC Olympic Games. Six solvers participated in the competition; the success and performance of each solver was measured over an appropriate subset of a library of benchmarks accumulated for the purpose. The benchmarks consisted of satisfiability and entailment problems over formulas in the fragment of symbolic heaps with inductive definitions, which is the fragment of Separation Logic that is most used in program analysis and verification tools. We report in this paper on the competition rules, the participants, the results, the …findings, and the future of this event. Show more

Keywords: Separation Logic, SMT-LIB, SAT Modulo Theory

DOI: 10.3233/SAT190107

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 9, no. 1, pp. 173-186, 2014

Authors: Janota, Mikoláš | Jordan, Charles | Klieber, Will | Lonsing, Florian | Seidl, Martina | Van Gelder, Allen

Article Type: Research Article

Abstract: The QBF Gallery 2014 was a competitive evaluation for QBF solvers organized as part of the FLoC 2014 Olympic Games during the Vienna Summer of Logic. The QBF Gallery 2014 featured three different tracks on formulas in prenex conjunctive normal form (PCNF) including more than 1200 formulas to be solved. Gold, silver, and bronze track medals were awarded to the solvers that solved the most formulas in each of the three tracks. Additionally, the three participants that were most successful over the complete benchmark set were awarded with Kurt Gödel medals, the official prizes of the FLoC 2014 Olympic Games. …In this paper, we give an overview of the setup and rules of the competition, briefly review the participating solvers, and finally report on the results of the QBF Gallery 2014. Show more

Keywords: Quantified Boolean formulas, QBF solving, QBF competition

DOI: 10.3233/SAT190108

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 9, no. 1, pp. 187-206, 2014

Authors: Cok, David R. | Déharbe, David | Weber, Tjark

Article Type: Research Article

Abstract: The 2014 SMT Competition was held in conjunction with the SMT Workshop, affiliated with the CAV, IJCAR, and SAT conferences at FLoC 2014, at the Vienna Summer of Logic in July 2014. Eighteen solvers participated from thirteen different research groups, across 34 different logic divisions. The competition was also part of the FLoC Olympic Games event, which gave combined visibility to 14 different competitions related to automated logic problem solving. The 2014 edition of the SMT Competition was executed for the first time on the StarExec logic solving service. Several records were broken: number of participating solvers, number of new …entrants, number of logic divisions, number of benchmarks, and amount of computation. The detailed performance of each solver on each benchmark from this first year using StarExec will be a solid baseline to measure improvements in the state-of-the-art of solver performance in future years. Show more

Keywords: SMT solver, SMT-COMP, SMT-LIB, Satisfiability Modulo Theories, competitions

DOI: 10.3233/SAT190109

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 9, no. 1, pp. 207-242, 2014