Theory and Applications of Satisfiability Testing – SAT 2021
24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings
Article
Given an undirected graph, the Maximum Clique Problem (MCP) is to find a largest complete subgraph of the graph. MCP is NP-hard and has found many practical applications. In this paper, we propose a parallel B...
Article
We tackle the problem of reducing non-clausal MaxSAT and MinSAT to clausal MaxSAT and MinSAT. Our motivation is twofold: (i) the clausal form transformations used in SAT are unsound for MaxSAT and MinSAT, beca...
Chapter
Logical calculi applied to solve SAT are unsound for MaxSAT and MinSAT because they preserve satisfiability but not the minimum and the maximum number of unsatisfied clauses, respectively. This paper overviews...
Book and Conference Proceedings
24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings
Article
The performance of modern conflict-driven clause learning (CDCL) SAT solvers strongly depends on branching heuristics. State-of-the-art branching heuristics, such as variable state independent decaying sum (VS...
Chapter and Conference Paper
We define a non-clausal MaxSAT tableau calculus. Given a multiset o...
Chapter and Conference Paper
Many practical optimization problems can be translated to Max-SAT and solved using a Branch-and-Bound (BnB) Max-SAT solver. The performance of a BnB Max-SAT solver heavily depends on the quality of the lower b...
Chapter and Conference Paper
When searching for a maximum clique of a graph using a branch-and-bound algorithm, it is usually believed that one should minimize the set of branching vertices from which search is necessary. It this paper, w...
Chapter and Conference Paper
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
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
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
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
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: ...
Article
The lower bound (LB) implemented in branch and bound MaxSAT solvers is decisive for obtaining a competitive solver. In modern solvers like MaxSatz and MiniMaxSat, the LB relies on the cooperation of the undere...
Chapter and Conference Paper
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
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
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
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
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...
Article
We show that we can design and implement extremely efficient variable selection heuristics for SAT solvers by identifying, in Boolean clause databases, sets of Boolean variables that model the same multivalued...