Theory and Applications of Satisfiability Testing – SAT 2021
24th International Conference, Barcelona, Spain, July 5-9, 2021, Proceedings
Page
%P
-
Article
Parallel Bounded Search for the Maximum Clique Problem
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
Open AccessClausal Forms in MaxSAT and MinSAT
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
Inference in MaxSAT and MinSAT
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
-
Article
A branching heuristic for SAT solvers based on complete implication graphs
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
A Tableau Calculus for Non-clausal Maximum Satisfiability
We define a non-clausal MaxSAT tableau calculus. Given a multiset o...
-
Chapter and Conference Paper
Breaking Cycle Structure to Improve Lower Bound for Max-SAT
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
Incremental MaxSAT Reasoning to Reduce Branches in a Branch-and-Bound Algorithm for MaxClique
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
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: ...
-
Article
Resolution-based lower bounds in MaxSAT
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
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...
-
Article
Exploiting multivalued knowledge in variable selection heuristics for SAT solvers
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...
