1,720,960 research outputs found
Minimally Unsatisfiable Subformulae
No full textMinimal unsatis?ability is a topic in the ?eld of satis?ability (SAT). Minimally unsatis?able subformulae (MUSes) are minimal subsets of an unsatis?able formula that are unsatis?able. They can therefore be seen as causes of unsatis?ability. With recent improvements in SAT solving, extracting MUSes has also become faster. Lately increasingly more effort has been put in getting MUS extraction to industrial strength. This thesis tries to speed up MUS extraction by applying preprocessing techniques from the ?eld of SAT solving. Application is not always straightforward. Some techniques have to be modi?ed and some are not applicable at all. For each of the discussed techniques, this thesis describes how they affect MUSes and what has been done to apply them.AlgorithmicsSoftware TechnologyElectrical Engineering, Mathematics and Computer Scienc
Concurrent Cube-and-Conquer
No full textRecent work introduced the cube-and-conquer technique to solve hard SAT instances. It combines the two dominant SAT solving techniques: lookahead and conflict-driven clause learning (CDCL). First, it partitions the search space into so called cubes using a lookahead solver. Each cube is tackled by a conflict-driven clause learning solver. Crucial for strong performance is the cutoff heuristic that decides when to switch from lookahead to CDCL. Yet, this offline heuristic is far from ideal. In this work, we present a novel hybrid solver that applies lookahead and CDCL simultaneously. Both solvers work together on each cube, while communication is restricted to synchronization. Our concurrent cube-and-conquer (CCC) solver can solve many instances faster than pure lookahead, pure CDCL and offline cube-and-conquer, but is not suitable for all instances. We have developed two metrics that can be used to accurately select when to apply CCC or to fall back to pure CDCL. We think CCC is especially useful as part of a portfolio that selects a suitable solver based on machine learning techniques, and show that machine learning techniques can indeed be used to select accurately whether CCC or CDCL works best.Computer ScienceAlgorithmics groupElectrical Engineering, Mathematics and Computer Scienc
SmArT solving: Tools and techniques for satisfiability solvers
No full textThe satisfiability problem (Sat) lies at the core of the complexity theory. This is a decision problem: Not the solution itself, but whether or not a solution exists given a specified set of requirements is the central question. Over the years, the satisfiability problem has taken center stage as a means of effective representation to tackle problems with different characteristics: Many problems can first be translated into Sat and then solved by means of software dedicated to the Sat problem. Due to the increasing power of these Sat solvers, the number of applications climbs every year. Examples of this kind of translatable problems are scheduling problems, verification of software and hardware, bounded model checking and a wide variety of mathematical puzzles. Sat solvers come in two flavors: Complete and incomplete. Complete solvers systematically go over the whole search space and are able to determine with certainty whether a solution exists. Incomplete Sat solvers look for a solution at a venture. They dont follow a system, yet they might hit a solution. Most complete Sat solvers are based on the ConflictDriven architecture. At a dead end, they analyze what went wrong and where in the search space it happened. Then they resume the search from there. Conflict-driven solvers make relatively cheap decisions (in terms of computational costs), which enables them to search the space swiftly. Only a few complete Sat solvers are based on an architecture that chooses its battles, so to speak. The LookAhead architecture peers further into the search space before making the next move. Look-ahead solvers make expensive decisions in order to keep the search space as small as possible. Incomplete Sat solvers have a dominant and a rare type of architecture as well. The commonly used WalkSat makes cheap decisions, while UnitWalk a bit off the wall makes more costly moves. This thesis deals with a number of contributions to the development of Sat solvers both complete and incomplete. With the adagium poundwise, Pennyfoolish in mind, its focus is primarily set on both rare, more expensive approaches. On one hand, expensive procedures are implemented efficiently to reduce their relative costs, while they maintain their impact on the search space. On the other hand, building up reasoning power further limits the search space. The growing attention for Sat solvers generates a growing group of users. More and more of them will not be familiar with the specific ins and outs of their application, which makes it difficult to tune the Sat solvers. Here, adaptive heuristics may be of use. Given a specific problem, these heuristics set the parameters in such a way that the solver performs (almost) optimally. This thesis presents some elegant adaptive heuristics for a technique that looks even further ahead into the search area to learn even more: The DoubleLook procedure. Thanks to these adaptive heuristics that keep on fine-tuning the parameters on the fly this binocular-technique can be helpful to solve more problems. The raison dÊtre of incomplete Sat solvers is the assumption that on many problems, they find a solution faster than complete solvers. Yet they are only superior within a certain niche; they work well on big (random) problems. To extend the span of incomplete Sat solvers, this thesis presents a Sat solver with the more rarely used UnitWalk architecture. Several expensive calculations are run simultaneously on a single processor which keeps costs relatively low. In addition, the solver features some communicative skills: Whenever a solution is found for part of the problem, all further calculations will run more efficiently. Despite these enhancements and its good results, this solver is not (yet) competitive on structured problems; an field dominated by complete Sat solvers. However, our complete Sat solver march, based on the LookAhead architecture, has won many awards in the prestigious Sat competitions, among which the gold medal for random problems without solutions (2007); a traditional stronghold of LookAhead solvers. More intriguing is the gold medal for crafted problems with solutions (2007). This is a field which is dominated besides march by conflict-driven solvers. In conclusion, the new techniques presented in this thesis have enhanced the LookAhead architecture to such an extend, that this type of solvers can compete on more problems while sustaining dominance on random instances.Electrical Engineering, Mathematics and Computer Scienc
Enhancing incomplete SAT solver performance through integration of complete SAT solver strategies
No full textThis research focuses on improving the incomplete multi-bit local search solver UnitMarch performance by the incorporating complete satisfiability techniques for variable ordering, autarky resolvents and learning methods. The result is better performing version UnitMarch 2.0 with the possibility to detect unsatisfiability. The complete solver branch heuristic variable ordering variable state independent decaying sum (VSIDS) was added to incomplete multi-bit solver UnitMarch. Using reverse ordering to the original heuristic shows a significant performance increase. A new method for finding 1-autarkies is introduced in UnitMarch, in combination with the addition of autarky resolvents. This is done as a preprocessing technique and during the solving process. The learning methods for indirect implications, failed literals and necessary assignments are introduced to UnitMarch as global learning methods. Failed literals are expanded to failed clauses. Necessary Assignments optimally use the structure of multi-bit assignments. UnitMarch 2.0 demonstrates a good performance increase with the succesfull integration of the complete solver techniques. The combined techniques results in better performance than the original solver. Using global learning methods allows UnitMarch to function as a complete solver and thus detect unsatisfiability.AlgorithmicsSoftware TechnologyElectrical Engineering, Mathematics and Computer Scienc
MiniMerge: Symmetry-Free Learning in Combinatorial Problems
No full textWe present a new method to break symmetry in graph coloring problems, which can be applied in many classes of combinatorial problems. While most alternative techniques add symmetry breaking predicates in a pre-processing step, we developed a learning scheme that translates each encountered conflict into one conflict clause which covers equivalent conflicts arising from any permutation of the colors. Our technique combines Extended Resolution with domain specific knowledge. Although the Extended Resolution proof system is powerful in theory, it is rarely used in practice because it is hard to determine which variables to introduce defining useful predicates. In case of graph coloring, the reason for each conflicting coloring can be expressed as a node in the Zykov-tree, that stems from merging some vertices and adding some edges. So, we focus on variables that represent the Boolean expression that two vertices can be merged (if set to true), or that an edge can be placed between them (if set to false). Further, our algorithm reduces the number of introduced variables by reusing them as much as possible. We implemented our technique in the state-of-the-art solver MiniSat2. It is competitive with alternative SAT based techniques for graph coloring problems. Moreover, our technique can be used on top of other symmetry breaking techniques. In fact, combined with adding symmetry breaking predicates, huge performance gains are realized.AlgorithmsElectrical Engineering, Mathematics and Computer Scienc
March dl: Adding Adaptive Heuristics and a New Branching Strategy
No full textWe introduce the march dl satisability (SAT) solver, a successor of march eq. The latter was awarded state-of-the-art in two categories during the Sat 2004 competition. The focus lies on presenting those features that are new in march dl. Besides a description, each of these features is illustrated with some experimental results. By extending the pre-processor, using adaptive heuristics, and by using a new branching strategy, march dl is able to solve nearly all benchmarks faster than its predecessor. Moreover, various instances which were beyond the reach of march eq, can now be solved - relatively easily - due to these new features.Software TechnologyElectrical Engineering, Mathematics and Computer Scienc
Parallel SAT Solving using Bit-level Operations
No full textWe show how to exploit the 32/64 bit architecture of modern computers to accelerate some of the algorithms used in satisfiability solving by modifying assignments to variables in parallel on a single processor. Techniques such as random sampling demonstrate that while using bit vectors instead of Boolean values solutions to satisfiable formulae can be obtained faster. Here, we reveal that more complex algorithms, like unit propagation and detection of autarkies, can be parallelized efficiently, as well. We capitalize on the developed parallel algorithms by modifying the state-of-the-art local search Sat solver UnitWalk accordingly. Experiments show that the parallel version performs much faster than the original implementation.Software TechnologyElectrical Engineering, Mathematics and Computer Scienc
Using a satisfiability solver to identify deterministic finite state automata
No full textWe present an exact algorithm for identification of deterministic finite automata (DFA) which is based on satisfiability (SAT) solvers. Despite the size of the low level SAT representation, our approach seems to be competitive with alternative techniques. Our contributions are threefold: First, we propose a compact translation of DFA identification into SAT. Second, we reduce the SAT search space by adding lower bound information using a fast max-clique approximation algorithm. Third, we include many redundant clauses to provide the SAT solver with some additional knowledge about the problem. Experiments on a well-known suite of random DFA identification problems show that SAT solvers can efficiently tackle all instances. Moreover, our exact algorithm outperforms state-of-the-art techniques on several hard problems.Software Computer TechnologyElectrical Engineering, Mathematics and Computer Scienc
Whose side are you on?: Finding solutions in a biased search-tree
No full textWe introduce a new jump strategy for look-ahead based satisfiability (Sat) solvers that aims to boost their performance on satisfiable formulae, while maintaining their behavior on unsatisfiable instances. Direction heuristics select which Boolean value to assign to a decision variable. They are used in various state-of-the-art Sat solvers and may bias the distribution of solutions in the search-tree. This bias can clearly be observed on hard random k-Sat formulae. While alternative jump / restart strategies are based on exploring a random new part of the search-tree, the proposed one examines a part that is more likely to contain a solution based on these observations. Experiments with - so-called distribution jumping - in the march ks Sat solver, show that this new technique boosts the number of satisfiable formulae it can solve. Moreover, it proved essential for winning the satisfiable crafted category during the Sat 2007 competition.Software TechnologyElectrical Engineering, Mathematics and Computer Scienc
Symmetry in gardens of Eden
No full textConway's Game of Life has inspired enthusiasts to search for a wide range of patterns for this classic cellular automaton. One important challenge in this context is finding the smallest Garden of Eden (GoE), a state without a predecessor. We take up this challenge by applying two techniques. First, we focus on GoEs that contain a symmetry. This significantly reduces the size of the search space for interesting sizes of the grid. Second, we implement the search using incremental satisfiability solving to check thousands of states per second. By combining these techniques, we broke several records regarding GoEs: the fewest defined cells, the smallest bounding box, and the lowest living density. Furthermore, we established a new lower bound for the smallest GoE.Software TechnologyElectrical Engineering, Mathematics and Computer Scienc
- …
