Journal on Satisfiability, Boolean Modeling and Computation - Volume 8, issue 3-4

Authors: Van Gelder, Allen

Article Type: Research Article

Abstract: The SAT solver Contrasat is a small variation of the well-established Minisat solver. It was entered in the Minisat hack track of the 2011 SAT competition, and was judged to be first place in one category. This paper describes the code change and its motivation. The characterization as “contrarian” is explained. Experimental results are summarized.

Keywords: SAT solver, CDCL, Minisat, volunteer, Contrasat

DOI: 10.3233/SAT190093

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 8, no. 3-4, pp. 117-122, 2012

Authors: Belov, Anton | Marques-Silva, Joao

Article Type: Research Article

Abstract: Algorithms for extraction of Minimally Unsatisfiable Subformulas (MUSes) of CNF formulas find a wide range of practical applications, including product configuration, knowledge-based validation, hardware and software design and verification. This paper describes the MUS extractor MUSer2 . MUSer2 implements a wide range of MUS extraction algorithms, integrates a number of key optimization techniques, and represents the current state-of-the-art in MUS extraction.

Keywords: Minimal unsatisfiability, MUS extraction, SAT applications

DOI: 10.3233/SAT190094

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 8, no. 3-4, pp. 123-128, 2012

Authors: Weaver, Sean A. | Ray, Katrina J. | Marek, Victor W. | Mayer, Andrew J. | Walker, Alden K.

Article Type: Research Article

Abstract: Introduced here is a novel application of Satisfiability (SAT) to the set membership problem with specific focus on efficiently testing whether large sets contain a given element. Such tests can be greatly enhanced via the use of filters , probabilistic algorithms that can quickly decide whether or not a given element is in a given set. This article proposes SAT filters (i.e., filters based on SAT) and their use in the set membership problem. Both the theoretical advantages of SAT filters and experimental results show that this technique yields significant performance improvements over previous techniques. Specifically, a SAT …filter is a filter construction that is simple yet efficient in terms of both query time and filter size; i.e., SAT filters asymptotically achieve the information-theoretic limit while providing fast querying. As well, this is the first application that makes use of the random k -SAT phase transition results and may drive research into efficient solvers for this and similar applications. Show more

Keywords: Satisfiability, Set Membership, Filters, Random k-SAT

DOI: 10.3233/SAT190095

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 8, no. 3-4, pp. 129-148, 2012

Authors: Krzakala, Florent | Mézard, Marc | Zdeborová, Lenka

Article Type: Research Article

Abstract: We study the random K -satisfiability problem using a partition function where each solution is reweighted according to the number of variables that satisfy every clause. We apply belief propagation and the related cavity method to the reweighted partition function. This allows us to obtain several new results on the properties of random K -satisfiability problem. In particular the reweighting allows to introduce a planted ensemble that generates instances that are, in some region of parameters, equivalent to random instances. We are hence able to generate at the same time a typical random SAT instance and one of its solutions. …We study the relation between clustering and belief propagation fixed points and we give a direct evidence for the existence of purely entropic (rather than energetic) barriers between clusters in some region of parameters in the random K -satisfiability problem. We exhibit, in some large planted instances, solutions with a non-trivial whitening core; such solutions were known to exist but were so far never found on very large instances. Finally, we discuss algorithmic hardness of such planted instances and we determine a region of parameters in which planting leads to satisfiable benchmarks that, up to our knowledge, are the hardest known. Show more

Keywords: random satisfiability, belief propagation, planted ensemble, average hardness, entropic barriers, planted constraint satisfaction

DOI: 10.3233/SAT190096

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 8, no. 3-4, pp. 149-171, 2012

Authors: Schwerdtfeger, Konrad W.

Article Type: Research Article

Abstract: For Boolean satisfiability problems, the structure of the solution space is characterized by the solution graph, where the vertices are the solutions, and two solutions are connected iff they differ in exactly one variable. Motivated by research on heuristics and the satisfiability threshold, in 2006, Gopalan et al. studied connectivity properties of the solution graph and related complexity issues for constraint satisfaction problems [11]. They found dichotomies for the diameter of connected components and for the complexity of the st -connectivity question, and conjectured a trichotomy for the connectivity question. Their results could be improved based on findings by Makino …et al. [15]. Building on this work, we here prove the trichotomy for the connectivity question. Also, we correct a minor mistake in [11], which leads to a slight shift of the boundaries towards the hard side. Show more

Keywords: Boolean satisfiability, Boolean CSPs, computational complexity, PSPACE-completeness, dichotomy theorems, graph connectivity

DOI: 10.3233/SAT190097

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 8, no. 3-4, pp. 173-195, 2012

Authors: Le Berre, Daniel | Roussel, Stéphanie

Article Type: Research Article

Abstract: Taking the best of SAT (at large) technology for a given class of problems requires usually an expert knowledge of the solver used or to rely on an automatic configuration tool. The former condition is usually not satisfied as soon as the user is not a member of the SAT community, and the latter solution does not help the user to understand what is going on inside the solver. We propose an approach that allows the end users of Sat4j to configure a solver for a specific instance. Such an approach is based on both the ability to change dynamically …the main settings of the solver when it is running and to display to the user several metrics that inform her about the state of the search in the solver. While the latter has been already explored in the SAT community, and the former has been explored in the constraint programming community, we believe that the combination of that two features is quite unique for SAT solvers. We believe that such a tool could also be used in the classroom to help students to understand how CDCL solvers work. Show more

Keywords: runtime solver configuration, interactive solving, search visualisation

DOI: 10.3233/SAT190098

Citation: Journal on Satisfiability, Boolean Modeling and Computation, vol. 8, no. 3-4, pp. 197-202, 2012