21 Result(s)
-
Chapter and Conference Paper
A Tableau Calculus for Non-clausal Maximum Satisfiability
We define a non-clausal MaxSAT tableau calculus. Given a multiset o...
-
Chapter and Conference Paper
MinSAT versus MaxSAT for Optimization Problems
Despite their similarities, MaxSAT and MinSAT use different encodings and solving techniques to cope with optimization problems. In this paper we describe a new weighted partial MinSAT solver, define original ...
-
Chapter and Conference Paper
Exploiting Historical Relationships of Clauses and Variables in Local Search for Satisfiability
Variable properties such as score and age are used to select a variable to flip. The score of a variable x refers to the decrease in the number of unsatisfied clauses if x is flipped. The age of x refers to the n...
-
Chapter and Conference Paper
A New Encoding from MinSAT into MaxSAT
MinSAT is the problem of finding a truth assignment that minimizes the number of satisfied clauses in a CNF formula. When we distinguish between hard and soft clauses, and soft clauses have an associated weigh...
-
Chapter and Conference Paper
Satisfying versus Falsifying in Local Search for Satisfiability
During local search, clauses may frequently be satisfied or falsified. Modern SLS algorithms often exploit the falsifying history of clauses to select a variable to flip, together with variable properties such...
-
Chapter and Conference Paper
Analyzing the Instances of the MaxSAT Evaluation
The MaxSAT Evaluation [1] is an affiliated event of the SAT Conference that is held every year since 2006, and is devoted to empirically evaluate exact MaxSAT algorithms solving any of the following problems: ...
-
Chapter and Conference Paper
Exact MinSAT Solving
We present an original approach to exact MinSAT solving based on solving MinSAT using MaxSAT encodings and MaxSAT solvers, and provide empirical evidence that our generic approach is competitive.
-
Chapter and Conference Paper
Exploiting Cycle Structures in Max-SAT
We investigate the role of cycles structures (i.e., subsets of clauses of the form $\bar{l}_{1}\vee l_{2}, \bar{l}_{1}\vee l_{3},\bar{...
-
Chapter and Conference Paper
Transforming Inconsistent Subformulas in MaxSAT Lower Bound Computation
We define a new heuristic that guides the application of cycle resolution (CR) in MaxSAT, and show that it produces better lower bounds than those obtained by applying CR exhaustively as in Max-DPLL, and by ap...
-
Chapter and Conference Paper
A Preprocessor for Max-SAT Solvers
We describe a preprocessor that incorporates a variable saturation procedure for Max-SAT, and provide empirical evidence that it improves the performance of some of the most successful state-of-the-art solvers...
-
Chapter and Conference Paper
Switching among Non-Weighting, Clause Weighting, and Variable Weighting in Local Search for SAT
One way to design a local search algorithm that is effective on many types of instances is allowing this algorithm to switch among heuristics. In this paper, we refer to the way in which non-weighting algorithm a...
-
Chapter and Conference Paper
Combining Adaptive Noise and Look-Ahead in Local Search for SAT
The adaptive noise mechanism was introduced in Novelty+ to automatically adapt noise settings during the search [4]. The local search algorithm G 2 WSAT deterministically exploits prom...
-
Chapter and Conference Paper
On Inconsistent Clause-Subsets for Max-SAT Solving
Recent research has focused on using the power of look-ahead to speed up the resolution of the Max-SAT problem. Indeed, look-ahead techniques such as Unit Propagation (UP) allow to find conflicts and to quickl...
-
Chapter and Conference Paper
Exploiting Unit Propagation to Compute Lower Bounds in Branch and Bound Max-SAT Solvers
One of the main differences between complete SAT solvers and exact Max-SAT solvers is that the former make an intensive use of unit propagation at each node of the proof tree while the latter, in order to ensu...
-
Chapter and Conference Paper
Diversification and Determinism in Local Search for Satisfiability
The choice of the variable to flip in the Walksat family procedures is always random in that it is selected from a randomly chosen unsatisfied clause c. This choice in Novelty or R-Novelty heuristics also contain...
-
Article
A Parallelization Scheme Based on Work Stealing for a Class of SAT Solvers
Because of the inherent NP-completeness of SAT, many SAT problems currently cannot be solved in a reasonable time. Usually, in order to tackle a new class of SAT problems, new ad hoc algorithms must be designe...
-
Chapter and Conference Paper
A Two-Level Search Strategy for Packing Unequal Circles into a Circle Container
We propose a two-level search strategy to solve a two dimensional circle packing problem. At the first level, a good enough packing algorithm called A1.0 uses a simple heuristic to select the next circle to be pa...
-
Chapter and Conference Paper
Characterizing SAT Problems with the Row Convexity Property
Using the literal encoding of the satisfiability problem (SAT) as a binary constraint satisfaction problem (CSP), we relate the path consistency concept and the row convexity of CSPs with the inference rules i...
-
Chapter and Conference Paper
A Hybrid Approach for SAT
Exploiting variable dependencies has been shown very useful in local search algorithms for SAT. In this paper, we extend the use of such dependencies by hybridizing a local search algorithm, Walksat, and the D...
-
Chapter and Conference Paper
Look-ahead versus look-back for satisfiability problems
CNF propositional satisfiability (SAT) is a special kind of the more general Constraint Satisfaction Problem (CSP). While lookback techniques appear to be of little use to solve hard random SAT problems, it is...
