Journal on Satisfiability,Boolean Modelling and Computation

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.

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.

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.

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.

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.

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.