Execution of most of the modern DPLL-based SAT solvers is guided by a number of heuristics. Decisions made during the search process are usually driven by some fixed heuristic pol...
Probabilistic inference techniques can be used to estimate variable bias, or the proportion of solutions to a given SAT problem that fix a variable positively or negatively. Metho...
Abstract. We present a new method to break symmetry in graph coloring problems. While most alternative techniques add symmetry breaking predicates in a pre-processing step, we deve...
In this paper we consider the class of boolean formulas in Conjunctive Normal Form (CNF) where for each variable all but at most d occurrences are either positive or negative. This...
Daniel Johannsen, Igor Razgon, Magnus Wahlströ...
Recent work has shown the value of using unsatisfiable cores to guide maximum satisfiability algorithms (Max-SAT) running on industrial instances [5,9,10,11]. We take this concep...
We investigate the role of cycles structures (i.e., subsets of clauses of the form ¯l1 ∨ l2, ¯l1 ∨ l3, ¯l2 ∨ ¯l3) in the quality of the lower bound (LB) of modern MaxSAT ...