% This is samplepaper.tex, a sample chapter deFmonstrating the
% LLNCS macro package for Springer Computer Science proceedings;
% Version 2.20 of 2017/10/04
%
\documentclass[runningheads]{llncs}
%
\usepackage{graphicx}
\usepackage[ruled,vlined]{algorithm2e}
\usepackage{adjustbox}
\usepackage{color}
% Used for displaying a sample figure. If possible, figure files should
% be included in EPS format.
%
% If you use the hyperref package, please uncomment the following line
% to display URLs in blue roman font according to Springer's eBook style:
% \renewcommand\UrlFont{\color{blue}\rmfamily}
\usepackage{amsmath,amssymb}
\usepackage{tikz}
\usetikzlibrary{fit}
\usetikzlibrary{arrows,shapes,positioning}
\usepackage{wrapfig}
\usepackage{hyperref}
\synctex=1
\tikzset{
% Define arrow style
pil/.style={
->,
thick,
shorten <=2pt,
shorten >=2pt,}
}
%\usepackage{times}
\usepackage{caption}
\newcommand{\MaxSAT}{MaxSAT }
\newcommand{\formula}{F}
\newcommand{\instance}{\mathcal{F}}
\newcommand{\core}{\kappa}
\newcommand{\CNF}{\textsc{CNF}}
\newcommand{\pjs}[1]{\textcolor{blue}{$\textsc{Pjs}$:#1}}
\newcommand{\emir}[1]{\textcolor{blue}{$\textsc{Emir}$:#1}}
\newcommand{\jerx}[1]{\textcolor{blue}{$\textsc{Jeremias}$:#1}}
\newcommand{\TODO}[1]{\textcolor{red}{#1}}
\begin{document}
\title{Core-Boosted Linear Search \\for Incomplete MaxSAT\thanks{The first author is financially supported by the University of Helsinki Doctoral Program in Computer Science and the Academy of Finland (grant 312662). We thank the University of Melbourne and the Melbourne School of Engineering Visiting Fellows scheme for supporting the visit of Jeremias Berg.}\thanks{The final authenticated version is
available online at \url{https://doi.org/10.1007/978-3-030-19212-9_3}}.}
%
%\titlerunning{Core-Boosted Linear Search}
% If the paper title is too long for the running head, you can set
% an abbreviated paper title here
%
\author{Jeremias Berg\inst{1} \and
Emir Demirovi\'c\inst{2} \and
Peter J. Stuckey\inst{3,4}}
%
\authorrunning{Berg et al.}
% First names are abbreviated in the running head.
% If there are more than two authors, 'et al.' is used.
%
\institute{HIIT, Department of Computer Science, University of Helsinki, Finland,
\email{jeremias.berg@cs.helsinki.fi}\\
\and
University of Melbourne, Australia,
\email{emir.demirovic@unimelb.edu.au}\\
\and
Monash University, Australia,
\email{peter.stuckey@monash.edu}\\
\and
Data61, CSIRO, Australia
}
%
\maketitle % typeset the header of the contribution
%
\begin{abstract}
Maximum Satisfiability (MaxSAT), the optimisation extension of the well-known Boolean Satisfiability (SAT) problem, is a competitive
approach for solving NP-hard problems encountered in various artificial intelligence and industrial domains.
Due to its computational complexity, there is an inherent tradeoff between scalability and guarantee on solution quality in MaxSAT solving.
Limitations on available computational resources in many practical applications motivate the development of \emph{complete any-time} MaxSAT solvers, i.e. algorithms that compute optimal solutions while providing intermediate results.
In this work, we propose \emph{core-boosted linear search}, a generic search-strategy that combines two central approaches in modern MaxSAT solving,
namely linear and core-guided algorithms.
Our experimental evaluation on a prototype combining reimplementations of two state-of-the-art MaxSAT solvers, PMRES as the core-guided approach and LinSBPS as the linear algorithm, demonstrates that our core-boosted linear algorithm often outperforms its individual components and shows competitive and, on many domains, superior results when compared to other state-of-the-art solvers for incomplete MaxSAT solving.
\keywords{Maximum Satisfiability \and MaxSAT \and SAT-based MaxSAT \and incomplete solving \and linear algorithm \and core-guided MaxSAT}
\end{abstract}
%
%
%
\section{Introduction}
Discrete optimisation problems are ubiquitous throughout society. When solving a discrete optimisation problem, the goal is to find the best solution according to a given objective function among a finite, but potentially large set of possibilities.
Examples of such problems include scheduling, routing, timetabling, and other forms of management decision problems. The solution approaches to discrete optimisation can be divided into
\emph{complete} and \emph{incomplete} methods. The aim of complete methods is to find the best possible solution and prove its optimality. However, in many real world applications
complete solving is a difficult, and in many cases, a practically infeasible task.
Hence, in practice, one might resort to incomplete solving, i.e. computing the best possible solution within a \emph{limited time}, rather than exclusively searching for an optimal solution.
There is a wide range of technologies available for discrete optimisation.
The focus of this work is on the Boolean optimisation paradigm of Maximum (Boolean) Satisfiability (MaxSAT), the optimization extension of the well-known
Boolean satisfiability (SAT) problem. MaxSAT can be used to solve any NP-hard discrete optimisation problem that can be formulated as minimising a
linear objective over Boolean variables
subject to a set of clausal constraints. Modern MaxSAT solving technology builds on the exceptional performance improvements of SAT solvers, starting in the late 90s~\cite{Silva:1997:GNS:244522.244560,zhang2001efficient}. Most MaxSAT solvers used in real-world applications are SAT-based, i.e. reduce the discrete optimisation problem into a sequence of satisfiability queries of Boolean formulas conjunctive normal form (CNF), and tackle the queries with SAT solvers.
In the last decade, MaxSAT solving technology has matured significantly, leading to successful applications of MaxSAT in a wide range of AI and industrial domains, such as timetabling, planning, debugging, diagnosis, machine learning, and systems biology \cite{maxLNS,asin2012curriculum,DBLP:journals/corr/abs-1007-1021,DBLP:journals/tcad/ChenSMV10,DBLP:conf/fmcad/ZhuWM11,DBLP:conf/cp/GuerraL12,BunteJBMPK:AAAI2014,BergJ:AIJ2015,MSJI:ijcai15}.
See \cite{DBLP:journals/ai/AnsoteguiBL13,DBLP:conf/sat/AnsoteguiBL09,DBLP:journals/constraints/MorgadoHLPM13} for more details.
SAT-based MaxSAT solvers can be roughly partitioned into \emph{linear}~\cite{qmaxsat,sat4j}, \emph{core-guided}~\cite{DBLP:conf/ijcai/AlvianoDR15,DBLP:conf/aaai/HerasMM11,DBLP:conf/cp/MorgadoDM14,DBLP:conf/ijcai/AnsoteguiDG15,DBLP:conf/aaai/NarodytskaB14,DBLP:conf/cp/MorgadoDM14}, and \emph{implicit hitting-set-based}~\cite{DBLP:conf/sat/DaviesB13,SaikkoBJ:SAT2016} algorithms.
The two most relevant ones for this work are the linear and core-guided algorithms. Linear algorithms are upper bounding approaches that encode the MaxSAT instance, along with its pseudo-Boolean objective function, into \emph{conjunctive normal form} (CNF) and iteratively query a SAT solver for a solution better than the current best one. In contrast, core-guided algorithms are lower-bounding approaches that use a SAT solver to extract a series of \emph{unsatisfiable cores}, i.e. sets of soft constraints that cannot be simultaneously satisfied, and reformulate the underlying MaxSAT instance to rule out each core as a source of unsatisfiability. Both search strategies have shown strong performance in the annual MaxSAT evaluations, linear search is particularly effective for incomplete solving while many of the best performing complete solvers are core-guided.
As our main contribution, we propose \emph{core-boosted linear search} for incomplete MaxSAT solving, a
novel search strategy that combines linear and core-guided search with the aim of achieving the best of both worlds. A core-boosted solver initially reformulates an input instance with a core-guided solver and then solves the reformulated
instance with a linear search solver.
The exchange of information from the core-guided phase to the linear phase tightens the gap between the lower and upper bound, allowing the use of a simpler pseudo-Boolean encoding. As a result,
the approach
%core-boosted linear search
is often more effective than either a pure linear or a pure core-guided search.
To demonstrate the potential of core-boosted linear search we report on an experimental evaluation of a prototype solver that combines reimplementations of two state-of-the-art MaxSAT solvers, PMRES~\cite{DBLP:conf/aaai/NarodytskaB14} as the core-guided algorithm and LinSBPS~\cite{MaxSATevaluation} as the linear algorithm.
We compare core-boosted linear search to its individual components on a standard set of benchmarks. Our results indicate that core-boosted linear search is indeed more effective
that either core-guided or linear search for incomplete solving. An in-depth look at the search progression on three selected instances demonstrates the ability of core-boosted linear search to both avoid the worst-case executions of its components, and make use the information flow between them to more quickly find solutions of higher quality.% than either core-guided or linear search.
The rest of the paper is organised as follows. After the preliminaries in Section~\ref{sec:prelim}, we give a detailed discussion of core-guided and linear search methods for MaxSAT in Section~\ref{sec:baseAlgs}. Core-boosted linear search is then presented in Section~\ref{sec:CB}. We discuss related work in Section~\ref{sec:rel}, after which we present our experimental evaluation in Section~\ref{sec:exp}. Lastly, we give concluding remarks in Section~\ref{sec:conc}.
\section{Preliminaries} \label{sec:prelim}
\newcommand{\var}{\textsc{Var}}
For a Boolean variable $x$ there are two literals, the positive $x$ and the negative $\lnot x$.
The negation $\lnot l$ of a literal $l$ satisfies $\lnot \lnot l = l$.
A clause $C$ is a disjunction ($\lor$) of literals (represented as a set of its literals), and a CNF formula $\formula$ a
conjunction ($\wedge$) of clauses (represented as a set of its clauses). The set $\var(\formula)$ of the variables of $\formula$ contains
all variables $x$ s.t. $x \in C$ or $\lnot x \in C$ for some $C \in F$.
We assume familiarity with other logical connectives and
denote by $\CNF(\phi)$ a set of clauses logically equivalent to the formula $\phi$. We also assume without loss of generality, that the size of $\textsc{CNF}(\phi)$ is linear in the size of $\phi$~\cite{Tseitin1983}.
A truth assignment $\tau$ is a function mapping Boolean variables to
$1$ (true) or $0$ (false). A clause $C$ is satisfied by $\tau$ (denoted by $\tau(C) = 1$) if
$\tau(l) = 1$ for a positive or $\tau(l) = 0$ for
a negative literal $l \in C$, otherwise $C$ is falsified by $\tau$ (denoted $\tau(C) = 0$). A CNF formula $\formula$ is satisfied by $\tau$
($\tau(\formula) = 1$) if $\tau$ satisfies all clauses in the formula and falsified otherwise ($\tau(\formula) = 0$). If some $\tau$
satisfies a CNF formula $\formula$, then $\formula$ is satisfiable, otherwise it is unsatisfiable. The NP-complete Boolean Satisfiability problem (SAT)
asks to decide if a given CNF formula $\formula$ is satisfiable~\cite{Biere:2009:HSV:1550723}.
\newcommand{\cost}{\textsc{COST}}
\newcommand{\s}{\textsc{Soft}}
\newcommand{\h}{\textsc{Hard}}
A (weighted partial) MaxSAT instance $\instance$ consists of two sets of clauses: the hard $\h(\instance)$, the soft $\s(\instance)$, and a function
$w^{\instance} \colon \s(\instance) \to \mathbb{N}$ associating a positive integral cost to each soft clause. The set $\var(\instance)$ of the variables
of $\instance$ is $\var(\h(\instance)) \cup \var(\s(\instance))$.
An assignment $\tau$ is a solution to $\instance$ if $\tau(\h(\instance)) = 1$. The cost $\cost(\instance, \tau)$ of a
solution $\tau$ to $\instance$ is the sum of the weights of the soft clauses it falsifies i.e.
$\cost(\instance, \tau) = \sum_{C \in \s(\instance)} w^{\instance}(C) \times (1 - \tau(C)).$
A solution $\tau$ is optimal if $\cost(\instance, \tau) \leq \cost(\instance, \tau')$ for all solutions $\tau'$ to $\instance$. We denote the cost of the optimal solutions
to $\instance$ by $\cost(\instance)$.
The NP-hard (weighted partial) MaxSAT problem asks to compute an optimal solution to a given instance $\instance$.
In the rest of the paper we will assume that all MaxSAT instances have solutions, i.e. that $\h(\instance)$ is satisfiable.
A central concept in many SAT-based MaxSAT algorithms is that
of an \emph{(unsatisfiable) core}. For a
MaxSAT instance $\instance$, a subset $\core \subseteq \s(\instance)$ of soft
clauses is an unsatisfiable core of $\instance$ iff $\h(\instance) \land \core$ is
unsatisfiable.
\section{Core-Guided and Linear Search for Incomplete MaxSAT} \label{sec:baseAlgs}
\newcommand{\satB}{\textsc{SATSolve}}
\newcommand{\sat}{\textsc{Extract-Core}}
\newcommand{\algCG}{\textsc{Core-Guided}}
\newcommand{\algLIN}{\textsc{Lin-Search}}
We detail two abstract MaxSAT solving algorithms, $\algLIN$ (Algorithm~\ref{alg:Lin}) and $\algCG$ (Algorithm~\ref{alg:CG}), representing linear and core-guided search,
respectively. Both use SAT-solvers to reduce MaxSAT solving into a sequence of satisfiability queries. However, the manner in which the SAT solver is used differs
significantly. We present both algorithms as complete \emph{any-time} algorithms, i.e. algorithms that, given enough resources, compute the optimal solution to a MaxSAT instance while also providing intermediate solutions during search.
In the following descriptions of the MaxSAT algorithms, we abstract the use of the SAT-solver into two functions.
The function $\satB$ represents a basic SAT-solver query.
Given a CNF formula $\formula$, the query $\satB(\formula)$ returns a tuple $(\mbox{\emph{res}}, \tau)$, where \emph{res} denotes
whether the formula is satisfiable and $\tau$ is a satisfying assignment to $\formula$ if one exists. The extended function $\sat(\h(\instance), \s(\instance))$
takes as input the hard and soft clauses of a MaxSAT instance $\instance$
and returns a triplet $(\mbox{\emph{res}}, \core, \tau)$, where \emph{res} indicates if $\h(\instance) \land \s(\instance)$ is satisfiable,
$\tau$ is a satisfying assignment for $\h(\instance) \land \s(\instance)$ if one exists, and $\core \subset \s(\instance)$ is a core of
$\instance$ if $\h(\instance) \land \s(\instance)$ is unsatisfiable.
%To the best of our knowledge,
Practically all SAT-solvers used in MaxSAT solving offer a so-called \emph{assumption interface}~\cite{DBLP:conf/sat/NadelR12} that can be used
to implement $\satB$ and $\sat$.
\begin{algorithm}[t]
\DontPrintSemicolon
\KwIn{A MaxSAT instance $\instance$}
\KwOut{An optimal solution $\tau$ to $\instance$}
\Begin{
$n \gets |\s(\instance)|$, \quad
$\tau^\star \gets \textsc{InitialSolution}(\instance)$ \;
$\mathcal{R} \gets \{r_1, \ldots, r_{n}\}$, \quad
$\formula^R_s = \{C_i \lor r_i \mid C_i \in \s(\instance), r_i \notin \var(\instance) \}$ \;
\While {true} {
\lIf{\mbox{Resource-Out}}{return $\tau^\star$}
$PB \gets \sum_{i=1}^n w^\instance(C_i) \times r_i < \cost(\instance, \tau^\star)$\;
$\formula_w \gets \h(\instance) \cup \formula^R_s \cup \CNF(PB)$ \;
$(\mbox{\emph{res}}, \tau) \gets \satB(\formula_w)$\;
\lIf{\mbox{res}=''satisfiable''}{$\tau^\star \gets \tau$}
\lElse{\KwRet{$\tau^\star$} }
}
}
\caption{$\algLIN$ \label{alg:Lin}}
\end{algorithm}
The pseudocode of $\algLIN$, is detailed in Algorithm~\ref{alg:Lin}. When solving an instance $\instance$, $\algLIN$ refines an upper bound on $\cost(\instance)$
by maintaining and iteratively improving a best known solution $\tau^\star$ to $\instance$. Initially, $\tau^\star$ is set to any solution of $\instance$, for example
by invoking the SAT solver on $\h(\instance)$. During search, the existence of a solution $\tau$ having cost less that $\tau^\star$ is checked by querying the internal SAT solver.
If no such solution is found, then $\tau^{\star}$
is optimal and $\algLIN$ terminates. Otherwise $\tau^{\star}$ is updated and the search continues. In more detail, the existence of a solution $\tau$ for which
$\cost(\instance, \tau) < \cost(\instance, \tau^\star)$ is checked by querying the SAT-solver for the satisfiability of a working formula
$\formula_w = \h(\instance) \cup \formula^R_s \cup \CNF(PB)$
consisting of the hard clauses, the soft clauses each extended with a unique \emph{relaxation variable} $r_i$ and
a CNF-encoding of a \emph{pseudo-Boolean} (PB) constraint $PB = \sum_{i=1}^n w^\instance(C_i) \times r_i < \cost(\instance, \tau^\star)$ that is satisfied
by an assignment $\tau$ iff $ \sum_{i=1}^n w^\instance(C_i) \times \tau(r_i) < \cost(\instance, \tau^\star)$. The intuition underlying
$\formula_w$ is that setting a relaxation variable $r_i$ to true allows falsification of the corresponding soft clause $C_i$.
Thus the PB constraint essentially limits the sum of the weights of the soft clauses falsified by an assignment $\tau$ to be less than the current best known upper bound
$\cost(\instance, \tau^{\star})$ on $\cost(\instance)$. In other words, $\formula_w$ is satisfied by an assignment $\tau$ iff $\tau$ is a solution to $\instance$ for which
$\cost(\instance, \tau) < \cost(\instance, \tau^{\star})$.
Before proceeding with core-guided search, we make two observations regarding the effectiveness of $\algLIN$ that are important for understanding core-boosted linear search. As
the search in $\algLIN$ is focused on decreasing the best known upper bound, we expect it to be most effective for solving an instance $\instance$ when the difference
between $\cost(\instance)$ and the cost $\cost(\instance, \tau^{\star})$ of the initial solution $\tau^{\star}$ is small. Thus, a high quality, i.e. low cost, initial solution can have a significant impact on the overall performance of $\algLIN$. The second observation concerns the PB constraint
$ \sum_{i=1}^n w^\instance(C_i) \times r_i < \cost(\instance, \tau^\star)$.
Similar constraints are encountered in many different domains, as such a lot of research has been put into developing efficient CNF encodings of them~\cite{sinz2005towards,asin2009sortingnetworks,DBLP:conf/cp/0001MM15}. Even so, the PB constraint is arguably the main bottleneck of the overall performance of $\algLIN$
and we expect any further techniques that allow the use of simpler, and more compact (encodings) PB constraints to improve the overall performance of $\algLIN$.
\iffalse
\begin{example}\label{ex:lin}
Let $\instance$ be a MaxSAT instance having $\h(\instance) = \{ (x_1 \lor x_2), (x_3 \lor x_4)\}$,
$\s(\instance) = \{ (\lnot x_i) \mid i=1\ldots 4\}$ with $w^{\instance} ( (\lnot x_1) ) = w^{\instance} ( (\lnot x_2) ) = 1$ and
$w^{\instance} ( (\lnot x_3) ) = w^{\instance} ( (\lnot x_4) ) = 2$ and $\tau^{\star}$ a solution to $\instance$ that sets
$\tau^{\star}(x_i) = 1$ for all $i=1,\ldots, 4$. We sketch one possible execution of $\algLIN$ when invoked on $\instance$ with $\tau^{\star}$
as the initial solution. Let
$\formula_w(B) = \h(\instance) \cup \{ (\lnot x_i \lor r_i) \mid i=1\ldots 4\} \cup \CNF( \sum_{i=1}^4 w^\instance( (\lnot x_i) ) \times r_i < B)$.
Since $\cost(\instance, \tau^{\star}) = 6$ the SAT solver is initially invoked on the satisfiable formula $\formula_w(6)$. Assume it returns
a solution $\tau$ setting $\tau(x_1) = \tau(x_3) = \tau(x_4) = 1$ and $\tau(x_2) = 0$ for which $\cost(\instance, \tau) = 5$.
During the next iteration the SAT solver is then invoked on the satisfiable formula $\formula_w(5)$. Assume it returns
a solution $\tau$ setting $\tau(x_1) = \tau(x_3) = 1$ for which $\cost(\instance, \tau) = 3$.
Finally, the SAT solver is invoked on the formula $\formula_w(3)$. The formula is unsatisfiable so $\algLIN$ terminates, requiring three SAT solver calls in total.
\end{example}
\fi
\newcommand{\strat}{ \textsc{STRAT}}
\newcommand{\stratB}{\textsc{B}}
\newcommand{\reform}{\textsc{Reformulate}}
\begin{algorithm}[t]
\DontPrintSemicolon
\KwIn{A MaxSAT instance $\instance$}
\KwOut{An optimal solution $\tau$ to $\instance$}
\Begin{
$\tau^\star \gets \textsc{InitialSolution}(\instance)$, \quad
$b^{\strat} \gets \max\{ w^\instance(C) \mid C \in \s(\instance)\}$ \;
$\instance^1 \gets \instance$, \quad $i \gets 1$ \;
\While{true} {
\lIf{\mbox{Resource-Out}}{return $\tau^\star$}
$\textsc{STRAT} \gets \{ C \mid C \in \s(\instance^i), w^{\instance^i}(C) \geq b^{\strat}\}$ \;
$(\mbox{\emph{res}}, \core^i, \tau) \gets \sat(\h(\instance^i), \textsc{STRAT} )$\;
\If{\mbox{res}=''satisfiable''}{
\lIf{$\cost(\instance, \tau) < \cost(\instance, \tau^\star)$}{$\tau^\star \gets \tau$}
\lIf{$\textsc{STRAT} = \s(\instance^i)$}{\KwRet{$\tau$} }
\lElse{$b^{\strat} \gets \max\{ w^{\instance^i}(C) \mid C \in \s(\instance^i), w^{\instance^i}(C) < b^{\strat} \}$}
}
\Else{
$\instance^{i+1} \gets \reform(\instance^i, \core^i)$ \;
$i \gets i +1$
}
}
}
\caption{$\algCG$ \label{alg:CG}}
\end{algorithm}
The pseudocode of $\algCG$, basic core-guided search extended with \emph{stratification} \cite{DBLP:journals/amai/Marques-SilvaAGL11,DBLP:conf/cp/AnsoteguiBGL12},
is detailed in Algorithm \ref{alg:CG}. Stratification is a heuristic designed to steer the core extraction of $\algCG$ toward cores $\core$ for which the minimum weight of the clauses in $\core$ is high. Stratification is a standard technique in modern core-guided solvers. Importantly for this work, stratification allows us to treat core-guided search as an any-time method for MaxSAT.
When solving an instance $\instance$, $\algCG$ maintains a working instance initialised to $\instance$ and a stratification bound $b^{\strat}$ initialised
to the highest weight of the soft clauses in $\instance$.
During iteration $i$ of the main search loop, the SAT solver is queried for a core $\core^i$ of a subset of the current working instance
$\instance^i$ containing all hard clauses and $\textsc{STRAT}$,
all soft clauses with weight greater than or equal to $b^{\strat}$. If no such core exists, an intermediate solution $\tau$
is obtained and compared to the best known solution $\tau^{\star}$. If all soft clauses were considered in the SAT call, the obtained solution is also optimal
and the algorithm terminates. If not, the bound $b^{\strat}$ is lowered and the search continues. When a core $\core^i$ is extracted,
the working instance is updated by the function $\reform$. Informally speaking, $\reform$
reformulates $\instance^i$ in a way that rules out $\core^i$ as a source of unsatisfiability and allows falsifying one clause in $\core^i$ without incurring cost.
Most of the core-guided MaxSAT solvers that fit the $\algCG$ abstraction~\cite{DBLP:conf/ijcai/AlvianoDR15,DBLP:conf/aaai/HerasMM11,DBLP:conf/cp/MorgadoDM14,DBLP:conf/ijcai/AnsoteguiDG15,DBLP:conf/aaai/NarodytskaB14,DBLP:conf/cp/MorgadoDM14} differ mainly in the implementation of $\reform$.
The correctness of such solvers is often established by showing that $\instance^{i}$ is MaxSAT-reducible to $\instance^{i+1}$ and that $\var(\instance^{i}) \subset \var(\instance^{i+1})$~\cite{DBLP:journals/ai/AnsoteguiBL13}. While a precise treatment of MaxSAT-reducibility is outside the scope of this work, the next proposition summarises
the consequences of it that are important for understanding core-boosted linear search.
\begin{proposition}\label{prop:MSRed}
Let $\instance$ be a MaxSAT instance, $\core$ a core of $\instance$, $w^{\core} = \min \{ w^{\instance}(C) \mid C \in \core\}$
and $\instance^R = \reform(\instance, \core)$. Assume that $\instance$ is MaxSAT reducible to $\instance^{R}$ and that $\var(\instance) \subset \var(\instance^R)$.
Then the following hold:
(i) any solution $\tau$ to $\instance$ can be extended into a solution $\tau^R$ to $\instance^R$ s.t. $\cost(\instance, \tau) = \cost(\instance^R, \tau^R) + w^{\core}$ and
(ii) any solution $\tau^R$ to $\instance^R$ is a solution to $\instance$ for which $\cost(\instance^R, \tau^R) = \cost(\instance, \tau^R) - w^{\core}$.
\end{proposition}
\medskip
An alternative intuition to core-guided search offered by Proposition~\ref{prop:MSRed} is thus a search strategy that lowers the optimal cost of its working instance by
extracting cores that witness lower bounds and reformulating the instance s.t the cost of every solution to the instance is lowered exactly by the identified lower bound.
Core-guided search terminates once the optimum cost of the working instance has been lowered to $0$.
\iffalse
\begin{example} \label{ex:concrete}
For a concrete example of an implementation of $\reform$ we consider the PMRES algorithm~\cite{DBLP:conf/aaai/NarodytskaB14}.
Let $\instance$ be an instance, $\core = \{C_1, \ldots, C_n\} \subset \s(\instance)$ a core of $\instance$
and $w^{\core} = \min \{ w(C) \mid C \in \core\}$. The reformulation used by PMRES forms the
instance $\instance^R$ having
$\h(\instance^R) = \h(\instance) \land \bigwedge_{i=1}^n \CNF(C_i \leftrightarrow \lnot r_i ) \land \bigwedge_{i=1}^{n-1} \textsc{CNF}( d_i \leftrightarrow (r_{i+1} \lor d_{i+1} )) \land (\lnot d_n)$ and
$\s(\instance^R) = (\s(\instance) \setminus \core) \land \textsc{CLONE}(\core) \land \bigwedge_{i=1}^{n-1} (\lnot r_i \lor \lnot d_i)$.
Each $r_i$ and $d_i$ is a new variable and $\textsc{CLONE}(\core) = \{ \textsc{CLONE}(C) \mid C \in \core \mbox{ and } w(C) > w^{\core} \}$
is a set of clones of the clauses in $\core$ that have weight higher than $w^{\core}$.
The weight of each new soft clause of form $(\lnot r_i \lor \lnot d_i)$ is $w^{\core}$ and the weight of each clone $\textsc{CLONE}(C)$
is the residual weight $w(C) - w^{\core}$. The intuition underlying the set $\textsc{CLONE}(\core)$ is that it allows treating all clauses
in $\core$ as having weight $w^{\core}$. A similar clause cloning technique is employed by most core-guided solvers~\cite{Li2005,DBLP:conf/aaai/NarodytskaB14,DBLP:conf/ijcai/BjornerN15,ANSOTEGUI201737}.
\end{example}
\fi
\begin{example} \label{ex:CG}
Let $\instance$ be a MaxSAT instance having $\h(\instance) = \{ (x_1 \lor x_2), (x_3 \lor x_4)\}$ and
$\s(\instance) = \{ (\lnot x_i) \mid i=1\ldots 4\}$ with $w^{\instance} ( (\lnot x_1) ) = w^{\instance} ( (\lnot x_2) ) = 1$ and
$w^{\instance} ( (\lnot x_3) ) = w^{\instance} ( (\lnot x_4) ) = 2$.
We sketch one possible execution of the PMRES algorithm~\cite{DBLP:conf/aaai/NarodytskaB14}, an instantiation of $\algCG$, when invoked on
$\instance$.
First, the initial working formula $\instance^1$ is set to $\instance$ and the stratification bound
$b^{\strat}$ is set to the highest weight of soft clauses, i.e. $2$. Thus $\strat = \{(\lnot x_3), (\lnot x_4)\}$ in the first iteration.
The formula $\h(\instance^1) \land \strat$ is unsatisfiable, the only core obtainable at this point is $\core^1 = \{ (\lnot x_3), (\lnot x_4)\}$.
Using the PMRES algorithm, the next working instance $\instance^2 = \reform(\instance^1, \core^1)$ has
$\h(\instance^2) = \h(\instance^1) \cup \{ ( \lnot x_3 \lor \lnot r_1),
\CNF(d_1 \leftrightarrow \lnot x_4)\}$, $\s(\instance^2) = \{ (\lnot x_1),(\lnot x_2) , (\lnot r_1 \lor \lnot d_1) \}$ with
$w^{\instance^2}(x_1) = w^{\instance^2}(x_2) = 1$ and $w^{\instance^2}( (\lnot r_1 \lor \lnot d_1) ) = 2$.
The stratification bound is not altered so $\strat = \{ (\lnot r_1 \lor \lnot d_1) \}$ during the next iteration.
Now $\h(\instance^2) \land \strat$
is satisfiable so $b^{\strat}$ is lowered to $1$. In the next iteration $\strat = \s(\instance^2)$
and the SAT solver obtains the core $\core^2 = \{(\lnot x_1),(\lnot x_2)\}$. The instance is again reformulated and the next working instance
$\instance^3 =\reform(\instance^2, \core^2) $ has $\h(\instance^3) = \h(\instance^2) \cup \{(\lnot x_1 \lor \lnot r_2),
\CNF(d_2 \leftrightarrow \lnot x_2) )\} $ and $\s(\instance^3) = \{ ( \lnot r_2 \lor \lnot d_2 ), (\lnot r_1 \lor \lnot d_1) \}$ with
$w^{\instance^3}( ( \lnot r_2 \lor \lnot d_2 ) ) = 1$ and $w^{\instance^3}( (\lnot r_1 \lor \lnot d_1) ) = 2$.
In the final iteration $\strat = \s(\instance^3)$ and since $\h(\instance^3) \land \s(\instance^3)$ is satisfiable, $\algCG$
terminates.
\end{example}
\medskip
We conclude this section with a few observations regarding $\algCG$ that are important for understanding core-boosted linear search.
When solving an instance $\instance$, $\algCG$ focuses its search on the
lower bound of $\cost(\instance)$. Thus, we expect $\algCG$ to be effective if $\cost(\instance)$ is low and, in particular, to
not be significantly affected by the quality of the initial solution.
The main bottleneck of $\algCG$ is instead the increased complexity of the core-extraction steps. Note that the core $\core^i$ extracted during
the i:th iteration of $\algCG$ is a core of the i:th working instance $\instance^i$ and not necessarily of the original instance $\instance$. While the effects of reformulation on the complexity of the $\sat$ calls are not fully understood, it has been shown that extracting a core of $\instance^i$ can be
exponentially harder than extracting a core of $\instance$~\cite{DBLP:conf/sat/BacchusN14}.
\section{Core-Boosted Linear Search for incomplete MaxSAT} \label{sec:CB}
In this section, we propose and discuss \emph{core-boosted linear search}, the main contribution of our work. The execution of a core-boosted (linear search) algorithm is split into two phases. On input $\instance$, the algorithm begins search in a core-guided phase
by invoking $\algCG$ on $\instance$. If $\algCG$ is able to find an optimal solution within the resources allocated to it, then
the core-boosted algorithm terminates. Otherwise $\algCG$ returns its final working instance $\instance_w$ along with the best solution $\tau^{\star}$ it found.
The core-boosted algorithm then moves on to its linear phase by invoking
$\algLIN$ on $\instance_w$ using $\tau^{\star}$ as the initial solution.
The linear phase runs until either finding the optimal solution to $\instance_w$, or running out of computational resources. By Proposition~\ref{prop:MSRed}, the
best solution $\tau^{\star}$ to $\instance_w$ found by $\algLIN$ is also a solution to $\instance$. Specifically, an optimal solution of $\instance_w$ is also an optimal solution
to $\instance$ implying the completeness of core-boosted linear search for MaxSAT. We emphasize that the linear component $\algLIN$ of a core-boosted algorithm
is invoked on $\instance_w$, the final working instance of $\algCG$, and not on $\instance$, the initial input instance.
As we discuss next and demonstrate in our experiments, this allows
the linear phase of core-boosted linear search to benefit from the core-guided phase in a non-trivial manner.
\iffalse
\begin{figure}[t]
\begin{tikzpicture}
\node[rectangle, align=left] (INST) at (-2.5, 1.5) {$\instance$};
\node[rectangle, draw, align=left] (CG) at (0, 0) {$\algCG(\instance)$};
\node[rectangle, align=left] (RCG) at (1.5, -1.5) {\textbf{return:} $\tau^\star$};
\node[rectangle, draw, align=left] (LIN) at (6, 0) {$\algLIN(\instance_w, \tau^\star)$};
\node[rectangle, align=left] (RLIN) at (7.5, -1.5) {\textbf{return:} $\tau^\star$};
\path[every node/.style={font=\sffamily\small}]
(INST.south) edge [pil, bend right=35] node [right, pos=0.3] {\scriptsize \textit{Input}} (CG.west)
(CG.south) edge [pil, bend right=35] node [right, pos=0.5] {\scriptsize \textit{Optimum found}} (RCG.west)
(CG.east) edge [pil] node [above, pos=0.5, align=left] {\scriptsize \textit{CG-resources out} \\ \scriptsize $(\instance_w, \tau^\star)$} (LIN.west)
(LIN.south) edge [pil, bend right=35] node [right, pos=0.4, align=left] {\scriptsize \textit{Optimum found or} \\ \scriptsize\textit{resources out}} (RLIN.west)
;
\end{tikzpicture}
\caption{ The structure of a core-boosted linear search algorithm. \label{fig:main} }
\end{figure}
\fi
The discussion on $\algLIN$ and $\algCG$ in Section~\ref{sec:baseAlgs} serves as useful basis for understanding the potential benefits of core-boosted linear search.
Since core-boosted linear search makes use of both core-guided and linear search, we expect it to be effective both on the same instances
as linear search, and as core-guided search, or at least not significantly worse. For example,
if the instance $\instance$ being solved has low optimal cost, then we expect a core-boosted algorithm to be able to solve the instance effectively during its initial
core-guided phase. Similarly, if $\cost(\instance)$ is close to the cost $\cost(\instance, \tau^{\star})$ of the initial solution $\tau^{\star}$, then
$\cost(\instance_w)$ is also close to $\cost(\instance_w, \tau^\star)$. Hence we expect a core-boosted algorithm to be effective during its linear phase, even factoring in the reformulations
done during the core-guided phase.
The potential benefits of core-boosted linear search go beyond merely averaging out the performance of core-guided and linear search.
As discussed in the previous section, one of the main drawbacks of core-guided search is the increased complexity of core extraction over time. Thus stopping the core-guided phase
and solving the working instance by linear search should be beneficial. Further, the linear phase can also benefit from the reformulation steps performed by the core-guided phase.
Specifically, such reformulations can decrease the size of the PB
constraint $PB = \sum_{i=1}^n w^{\instance}(C_i) \times r_i < \cost(\instance, \tau^\star)$ that needs to be encoded during linear search. Depending on the specific encoding used,
the number of clauses resulting from encoding $PB$ into CNF depends either on the magnitudes of the weights of the soft clauses and the right-hand side~\cite{sortingNetworks} or
on the number of unique sums that can be created from those weights~\cite{DBLP:conf/cp/0001MM15}. The reformulation steps performed during the
core-guided phase of a core-boosted algorithm can affect both of these factors.
By Proposition~\ref{prop:MSRed} $\cost(\instance_w, \tau^{\star}) \leq \cost(\instance, \tau^{\star})$ which implies
that both the magnitude of the weights in $\instance_w$ and the initial right hand side $\cost(\instance_w, \tau^{\star})$ of PB are smaller in the reformulated $\instance_w$ than in
the original $\instance$. Additionally, the core-guided phase can also decrease the number of soft clauses in the instance;
the second working instance of Example~\ref{ex:CG} has one less soft clause than the first one.
Finally, the so-called \emph{hardening rule}~\cite{DBLP:conf/cp/AnsoteguiBGL12} commonly used in conjunction with core-guided search, can also decrease the number of soft clauses
of the instance, and thus allow the linear phase of a core-boosted algorithm to use a more compact PB constraint
\section{Related Work} \label{sec:rel}
We begin by detailing the instantiations of $\algLIN$ and $\algCG$ that we use in the prototype core-boosted linear search algorithm experimented with
in the next section. As the linear search component we use the basic $\algLIN$
extended with varying resolution and solution-based phase-saving in the style of LinSBPS, the best performing
solver of the incomplete 300s track of the 2018 MaxSAT evaluation~\cite{MaxSATevaluation}. Solution-based phase-saving
is a heuristic designed to steer the search towards the currently best known solution by modifying the branching heuristic of the internal SAT solver to
always prefer setting the polarity of a literal it branches on to equal its polarity in the currently best known solution.
Varying resolution is a heuristic designed to alleviate the issues that $\algLIN$
has with large PB constraints. When invoked on an instance $\instance$ a linear search algorithm using varying resolution starts its search by creating a lower resolution version
of $\instance$ by dividing all weights of soft clauses by some constant $d$ and removing all clauses $C \in \s(\instance)$ for which $\lfloor w^{\instance}(C) / d\rfloor = 0$.
The low resolution version is then solved by standard linear search. When an optimal solution is found, the value of $d$ is decreased and the search continued in higher resolution.
Following LinSBPS, we used the generalized totalizer encoding (GTE)~\cite{DBLP:conf/cp/0001MM15} to convert the PB constraints to CNF.
Given a set of input literals $L = \{l_1, \ldots, l_n\}$ and their corresponding weights $W= \{w_1, \ldots w_n\}$
the GTE creates a set of output literals $o_1, \ldots o_k$ s.t. each $o_i$ corresponds to a sum $s_i$ formable with the weights in $W$
for which $s_i < s_j$ if $i < j$. The sum of weights of the literals in $L$ set to true is then restricted to be less than $s_i$ with the unit clause
$(\lnot o_i)$.
As the instantiation of $\algCG$ we use the PMRES algorithm~\cite{DBLP:conf/aaai/NarodytskaB14} extended with weight aware core extraction (WCE)~\cite{berg2017weight} and
the hardening rule. Weight aware core extraction is a heuristic designed to allow $\algCG$ to extract multiple cores before
reformulating the instance and increasing its complexity. When extracting a new core $\core$
PMRES with WCE first computes $c^{\core} = \min\{ w^{\instance}(C) \mid C \in \core\}$, then lowers the weight of all clauses in $\core$ by $c^{\core}$ (removing all clauses with weight $0$). When no new cores can be extracted, the $\reform$ function is invoked on
all of the found cores and the stratification bound is reset. The search continues until no new cores can be found after a reformulation step. This strategy corresponds
to the S/to/WCE strategy of~\cite{berg2017weight}. While an alternative strategy that prefers reformulating to lowering the stratification bound was deemed more effective for complete
MaxSAT solving in~\cite{berg2017weight}, we found that S/to/WCE is more effective for incomplete solving. For lowering the stratification bound, we use the
\emph{diversity heuristic}~\cite{DBLP:conf/cp/AnsoteguiBGL12} that balances the amount that $b^{\strat}$ is lowered with
the number of new soft clauses introduced.
In the next section, we report on a comparison of core-boosted linear search and all of the solvers that participated in the incomplete track of the 2018 MaxSAT Evaluation:
LinSBPS, maxroster, SATLike, Open-WBO and Open-WBO-Inc and their variations.
Most of them implement variations of an approach where: i) a heuristic of some kind if used to find a good initial solution to the instance being
solved and ii) that solution is used to initialise a complete any-time algorithm. In most cases, the complete algorithm is some variant of $\algLIN$.
The solver SATLike~\cite{SATLike} deviates from this description and instead uses local-search techniques in order to quickly traverse the search space and look for solutions
of increasing quality. A more detailed description of the solvers can be found on the evaluation homepage~\cite{MaxSATevaluation}.
For related work from the field of complete MaxSAT solving,
the Primal-Dual MaxSAT algorithm~\cite{DBLP:conf/ijcai/BjornerN15} extends PMRES with a second instance reformulation used to rule out solutions that
falsify the same clauses as an intermediate solution obtained during search. The main two differences between Primal-Dual
and core-boosted linear search are that Primal-Dual reformulates the instance on each iteration, thus increasing the complexity of core extraction steps, and
that the reformulation only rules out solutions that falsify a particular set of clauses. In contrast, lowering the bound on the PB constraint in $\algLIN$ rules out
all solutions that have higher cost than the best known solution. The WMSU3~\cite{DBLP:journals/corr/abs-0712-1097} algorithm maintains a cardinality constraint over
soft clauses similar to $\algLIN$ but only relaxes a soft clause $C$ after extracting a core $\core$ for which $C \in \core$.
The similar WPM3~\cite{ANSOTEGUI201737} uses linear-search as a subroutine within core-guided search in order to obtain tighter bounds on the cardinality constraints.
In addition to core-guided and linear search, a third central approach to SAT-based MaxSAT solving is based on
\emph{implicit-hitting sets}~\cite{DBLP:conf/sat/DaviesB13,SaikkoBJ:SAT2016}.
When solving, such solvers maintain a set of cores of the input instance. During each iteration, a minimum-cost hitting set over the set of cores is computed.
The clauses in the hitting set are then removed from the instance and the SAT solver invoked on the remaining clauses. If the SAT solver reports satisfiable, the obtained
solution is optimal. Otherwise, a new core is obtained and the search continues. Finally, MaxSAT solvers based on branch and bound have been shown to be
effective on random MaxSAT instances as well as challenging instances of smaller size. Such instances are encountered for example in combinatorics~\cite{Li2005,li2010efficient,abrame2015ahmaxsat,liu2016breaking,abrame2016learning,li2007new,xing2005maxsolver,lin2008within}.
\section{Experimental Evaluation} \label{sec:exp}
Next we present the results on a experimental evaluation of a prototype core-boosted linear search algorithm that combines
the instantiations of $\algLIN$ and $\algCG$ discussed in Section~\ref{sec:rel}. We refer to our implementation of $\algLIN$ extended with varying resolution
and solution-guided phase saving by Linear-Search. Similarly, we use Core-Guided to refer to our implementation of PMRES extended with WCE and hardening.
Finally, Core-Boosted-XXs is the core-boosted algorithm that first runs Core-Guided until either XX seconds have passed or no more cores can be
found with the stratification bound at $1$, then reformulates the instance and solves the reformulated instance with Linear-Search.
The state of the internal SAT solver of Core-Boosted-XXs is kept throughout the core-guided phase, but
reset (that is learned clauses are eliminated and activities of all variables reset to 0)
when execution is switched to the linear search phase and
whenever resolution is increased during the linear phase.
All three algorithms were implemented on top of the publicly available Open-WBO system~\cite{DBLP:conf/sat/MartinsML14} using Glucose 4.1~\cite{glucose} as the back-end SAT solver.
The initial solution of all three algorithms is obtained by invoking the SAT solver on the hard clauses of the instance being solved.
We emphasise that core-boosted linear search is a general idea applicable with all implementations and extensions of $\algLIN$ and $\algCG$ that we are aware off.
The goal of these experiments is to show that core-boosting can be used to improve performance of modern core-guided and linear search solvers, not to evaluate different instantiations and extensions of
$\algCG$ and $\algLIN$.
Our experimental setup is similar to the 300s weighted incomplete track of the 2018 MaxSAT evaluation~\cite{MaxSATevaluation}.
In most of the experiments, we use the 172 benchmarks from the
weighted incomplete track of the evaluation, available from \url{https://maxsat-evaluations.github.io/2018/benchmarks.html}.
We enforce a per-instance time limit of 300 seconds and memory limit of 32GB.
All of the experiments were run on the StarExec cluster (\url{https://www.starexec.org}) that has 2.4-GHz Intel(R) Xeon(R) E5-2609 0 quad-core
machines with 128-GB RAM.
\newcommand{\costB}{\textsc{BEST-COST}}
\newcommand{\score}{\textsc{Score}}
As the metric for comparing solvers we use the same incomplete score as the evaluation. For an instance $\instance$ let $\costB(\instance)$ denote the lowest cost
found in 300 seconds by any of (the variants of) the solvers Linear-Search, Core-Guided, Core-Boosted-XXs or the solvers that participated in the evaluation.
The score a solver $S$ on $\instance$ is defined as the ratio between $\costB(\instance)$ and the cost of the best solution $\tau^S$ to $\instance$ found by $S$, i.e.
$\score(S, \instance) = \frac{\costB(\instance) + 1}{\cost(\instance, \tau^S) + 1}$. In other words, the score of $S$ is the ratio
between the cost of the solution of the virtual-best-strategy (VBS) among our methods and the MaxSAT Evaluation 2018 solvers, and the cost obtained by $S$.
Hence the score difference between two solvers shows the percentage points by which the better solver is closer to the VBS.
\begin{table}[t!]
\caption{Average score obtained by Core-Boosted-XXs with different maximum times for the core-guided phase as well as its core-guided
and linear search components. In the table CB-XXs refers to the Core-Boosted-XXs solver, Lin to the Linear-Search solver and CG to the Core-Guided solver.
\label{tbl:cbvariants} }
\resizebox{\columnwidth}{!}{%
\begin{tabular}{l|r|r|r|r|r|r|r}
\textbf{Domain (\#benchmarks) } & \multicolumn{1}{l|}{\textbf{CB-30s}} & \multicolumn{1}{l|}{\textbf{CB-75s}} & \multicolumn{1}{l|}{\textbf{CB-150s}} & \multicolumn{1}{l|}{\textbf{CB-225s}} & \multicolumn{1}{l|}{\textbf{CB-300s}} & \multicolumn{1}{l|}{\textbf{CG}} & \multicolumn{1}{l}{\textbf{Lin}} \\ \hline
BTBNSL (16) & \textbf{0.996} & 0.995 & \textbf{0.996} & 0.995 & 0.965 & 0.956 & 0.959 \\ \hline
abstraction-refinement (2) & \textbf{1.000} & \textbf{1.000} & \textbf{1.000} & \textbf{1.000} & \textbf{1.000} & \textbf{1.000} & 0.517 \\ \hline
af-synthesis (19) & 0.990 & 0.990 & 0.990 & 0.990 & 0.990 & 0.944 & \textbf{0.991} \\ \hline
causal-discovery (14) & 0.776 & 0.776 & 0.799 & \textbf{0.803} & 0.795 & 0.563 & 0.454 \\ \hline
cluster-expansion (20) & \textbf{0.941} & \textbf{0.941} & \textbf{0.941} & \textbf{0.941} & \textbf{0.941} & \textbf{0.941} & \textbf{0.941} \\ \hline
correlation-clustering (12) & 0.953 & \textbf{0.956} & 0.953 & 0.953 & 0.953 & 0.736 & 0.675 \\ \hline
hs-timetabling (13) & 0.701 & 0.655 & 0.566 & 0.459 & 0.144 & 0.076 & \textbf{0.717} \\ \hline
lisbon-wedding (12) & \textbf{0.582} & \textbf{0.582} & \textbf{0.582} & \textbf{0.582} & \textbf{0.582} & 0.544 & \textbf{0.582} \\ \hline
maxcut (11) & \textbf{0.892} & \textbf{0.892} & \textbf{0.892} & \textbf{0.892} & \textbf{0.892} & 0.594 & 0.884 \\ \hline
min-width (16) & 0.961 & \textbf{0.965} & 0.962 & 0.956 & 0.962 & 0.825 & 0.898 \\ \hline
miplib (5) & \textbf{0.587} & \textbf{0.587} & 0.584 & 0.584 & 0.444 & 0.309 & 0.571 \\ \hline
power-distribution (2) & \textbf{0.704} & \textbf{0.704} & \textbf{0.704} & \textbf{0.704} & \textbf{0.704} & 0.497 & 0.484 \\ \hline
railway-transport (4) & 0.927 & 0.923 & 0.916 & 0.920 & \textbf{0.935} & 0.708 & 0.906 \\ \hline
relational-inference (2) & 0.041 & 0.041 & 0.041 & 0.041 & \textbf{0.429} & 0.414 & 0.041 \\ \hline
robot-nagivation (3) & \textbf{0.943} & \textbf{0.943} & \textbf{0.943} & \textbf{0.943} & 0.000 & 0.000 & \textbf{0.943} \\ \hline
spot5 (3) & 0.990 & 0.990 & 0.990 & 0.990 & 0.990 & 0.914 & \textbf{0.999} \\ \hline
staff-scheduling (10) & \textbf{0.895} & \textbf{0.895} & 0.863 & 0.840 & 0.493 & 0.385 & 0.877 \\ \hline
tcp (7) & \textbf{1.000} & 0.998 & 0.998 & \textbf{1.000} & \textbf{1.000} & 0.864 & 0.988 \\ \hline
timetabling (1) & 0.667 & 0.148 & 0.130 & 0.131 & 0.131 & 0.026 & \textbf{0.941} \\ \hline \hline
Total (172) & \textbf{0.870} & 0.864 & 0.857 & 0.847 & 0.785 & 0.680 & 0.807
\end{tabular}
}
\end{table}
The first experiment we report on evaluates effect of different time limits on the core-guided phase of Core-Boosted-XXs.
As limits we chose 30 seconds (10\% of the total time), 75s (25\%), 150s (50\%), 225s (75\%) and 300s (100\%), respectively. An important fact to keep in mind is that the core-guided
phase can end earlier than the limit. For example, the solver Core-Boosted-150s runs its core-guided phase until no more cores can be found with the
stratification bound at $1$ \emph{or} 150 seconds have elapsed.
Table~\ref{tbl:cbvariants} lists the average score obtained by the Core-Boosted-XXs (CB-XXs in the table) solver for different values of XX.
Overall we observe a decrease in the average score when the time limit is increased, even if the effect is small in most domains.
A possible explanation for this behavior is offered by Figure~\ref{fig:CG-time} showing the duration of
the core-guided phase of the Core-Boosted-300s solver on all benchmarks. On 107 out of the 172 benchmarks, the core-guided phase ended within 30 seconds and on 38
benchmarks Core-Boosted-300s did not enter its linear search phase at all. In other words, on a clear majority of the benchmarks, the duration of core-guided phase was
either very short or very long, which explains the good performance of Core-Boosted-30s. For the rest of the experiments, we fix the time limit for the core-guided phase to 30 seconds.
Table~\ref{tbl:cbvariants} also lists the average score obtained by the two components of Core-Boosted individually. The scores clearly demonstrate
the potential of core-boosted linear search. The average score of Core-Boosted-30s is higher than either Core-Guided (CG in the table) or Linear-Search (Lin in the table)
on 10 out of 19 domains and equal to its better component on 3 more.
\iffalse
\begin{wrapfigure}{r}{0.4\textwidth}
\includegraphics[width=0.4\textwidth]{Results/LinstartHistogram-Fine-crop.pdf}
\caption{Time spent in core-guided phase by Core-Boosted-300s \label{fig:CG-time}}
\end{wrapfigure}
\fi
\begin{figure}
\centering
\includegraphics[width=0.4\textwidth]{Results/LinstartHistogram-Fine-crop.pdf}
\caption{Time spent in core-guided phase by Core-Boosted-300s. \label{fig:CG-time}}
\end{figure}
Figure~\ref{fig:gapTests} shows a detailed analysis on the behaviour of core-boosted linear search in the form of plots showing
the evolution of the gap between the upper and lower bound (in logscale) of Core-Boosted-30s, Linear-Search and Core-Guided on three hand-picked benchmarks.
The benchmark on the left shows a case where core-guided search is effective. During the first 30 seconds, both Core-Boosted-30s and Core-Guided
rapidly decrease the gap. After 30 seconds, Core-Boosted-30s switches to its linear search phase, which on this benchmark slows its search progression.
Core-Guided continues with the same search strategy, finding (and proving optimality of) a solution of cost 76250 in just under 190 seconds.
Even if the gap of Core-Boosted-30s is larger due to a smaller lower bound, it still finds an ``almost optimal" solution having cost 76251. On this benchmark Linear-Search
is unable to improve on its initial solution at all and returns a solution with cost 226338.
An important observation to make is that, in contrast to Linear-Search, Core-Boosted-30s did manage to improve its solution also in the linear phase. This indicates that
the linear search phase of core-boosted search can indeed benefit from the reformulation steps performed and the best solution obtained during the core-guided phase.
The benchmark in the middle of Figure~\ref{fig:gapTests} demonstrates the opposite behaviour to the one on the left. On this benchmark Core-Guided is unable to improve
on its initial solution having cost 651, while Linear-Search continuously improves it and ends up finding one that has cost 17. Core-Boosted-30s is initially unable
to make progress, but starts decreasing its gap when switching to the linear phase after 30s and ends up finding a solution of cost 23. Finally, the benchmark on the right demonstrates
a best-case scenario for core-boosted search. On this benchmark Linear-Search is unable to improve at all on its initial solution that has cost 311544.
Core-Guided is able to decrease the gap by increasing the lower bound to 104585, but is unable to find a single better solution and returns the initial solution of cost 311544 as well.
Core-Boosted-30s is able to use the best of both worlds by first increasing the lower bound during the core-guided phase and then switching to the linear phase in order
to find a solution of cost 171437, significantly better than either of its components. Notice that the initial solution given to the linear phase of Core-Boosted-30s is the same as
the one found by Linear-Search, so the performance difference between the two is only due to the reformulation steps done during core-guided search.
The results shown in Figure~\ref{fig:gapTests} suggest, that a more sophisticated strategy for deciding when to switch from the core-guided to the linear phase could be used
to further improve the empirical performance of core-boosted linear search. Even though the instances in Figure~\ref{fig:gapTests} are hand-picked, the average scores over all
benchmarks in the corresponding domains listed in Table~\ref{tbl:cbvariants} support the observations. For example, the instances in the hs-timetabling domain (Figure~\ref{fig:gapTests}, middle) tend to contain only a few very large cores that are difficult to extract, making them well suited for approaches that compute solutions. On the other hand, instances in
the causal-discovery domain (Figure~\ref{fig:gapTests}, right) contain very many small cores that make finding good intermediate solutions to them difficult without first ruling out
some of the cores with core guided search.
\begin{figure}
\centering
\begin{minipage}{0.32\textwidth}
\centering
\includegraphics[width=\textwidth] {Results/Gaps-AbstractionRefinement-crop.pdf}
\end{minipage}
\begin{minipage}{0.32\textwidth}
\centering
\includegraphics[width=0.98\textwidth]{Results/Gaps-TimeTabling-crop.pdf}
\end{minipage}
\begin{minipage}{0.32\textwidth}
\centering
\includegraphics[width=0.98\textwidth]{Results/Gaps-Causal-crop.pdf}
\end{minipage}
\caption{Evolution of the gap between the upper and lower bound during search. The specific benchmarks shown are
abstraction-refinement-downcast-antlr (left)~\cite{Zhang:2014:ARP:2594291.2594327}, hs-timetabling-BrazilInstance5.xml (middle)~\cite{maxLNS}, causal-discovery-causal\_carpo\_8\_100 (right)~\cite{DBLP:conf/uai/HyttinenEJ14}. \label{fig:gapTests}}
\end{figure}
Figure~\ref{fig:effectTests} shows a per-instance comparison of the score obtained by Core-Boosted-30s and four variants of it: 1) Core-Boosted-30s-no-reformulation that
ignores the reformulated instance and invokes the linear phase on the original instance, 2) Core-Boosted-30s-no-solution that ignores the best solution
obtained during the core-guided phase in the linear phase and instead initialises a new solution by invoking the SAT-solver on the hard clauses of the reformulated instance,
3) Core-Boosted-30s-keep-SAT-solver that keeps the state of the internal SAT solver throughout the entire
search and 4) Core-Boosted-30s-wce-to-strat that uses of the original search strategy proposed in~\cite{berg2017weight} during the core-guided phase.
In all plots Core-Boosted-30s is on the y-axis, so any data points in the upper left triangle correspond to benchmarks on which the baseline performed better than the variant.
We observe that the baseline solver performs better than all of its variants, justifying our design choices. The results suggest that using the reformulated instance and initialising the Linear Search with the best
solution obtained during core-guided search are especially important for the overall performance.
\begin{figure}
\centering
\begin{minipage}{0.24\textwidth}
\centering
\includegraphics[width=\textwidth]{Results/Scatter_NoReform-crop.pdf}
\end{minipage}
\begin{minipage}{0.24\textwidth}
\centering
\includegraphics[width=0.815\textwidth]{Results/Scatter_NoModel-crop.pdf}
\end{minipage}
\begin{minipage}{0.24\textwidth}
\centering
\includegraphics[width=0.815\textwidth]{Results/Scatter_KeepClauses-crop.pdf}
\end{minipage}
\begin{minipage}{0.24\textwidth}
\centering
\includegraphics[width=0.82\textwidth]{Results/Scatter_WCE2strat-crop.pdf}
\end{minipage}
\caption{The effect of different factors of Core-Boosted-30s on the overall performance. \label{fig:effectTests}}
\end{figure}
Finally, we compare Core-Boosted-30s and its components to the other solvers that participated in the 2018 evaluation.
Due to running our experiments in the same environment as the evaluation,
we did not rerun the other solvers but instead compared our solvers directly to the results of the evaluation. Figure~\ref{fig:comp} demonstrates the performance of our solvers on the 300s weighted (left) and unweighted (right) tracks\footnote{A consequence of the metric we use
is that the scores of the other solvers we report are lower than in the evaluation. Their relative ranking is however the same.}.
We observe that Core-Boosted-30s performs very well in the weighted track, improving the previous state-of-the-art (LinSBPS) by approximately
$2\%$ while also finishing 3rd in the unweighted category.
In more detail, out of the $172$ weighted instances, Core-Boosted-30s and LinSBPS are equal on $63$ instances ($36\%$),
Core-Boosted-30s finds a solution of strictly lower cost on $65$ ($37\%$), and LinSBPS on $44$ ($25\%$).
We also evaluated our solvers in the 60s track of the evaluation, i.e. with the time out set to 60 seconds. In the weighted track, Core-Boosted-30s gets the average score $0.814$
which is again highest of all solvers followed by Open-WBO-Inc-BMO ($0.793$). In the unweighted track, the average score of Core-Boosted-30s is $0.696$ which is second highest after SATLike-c ($0.699$).
\begin{figure}
\centering
\begin{minipage}{0.48\textwidth}
\centering
\includegraphics[width=\textwidth]{Results/CompW300-crop.pdf}
\end{minipage}
\begin{minipage}{0.48\textwidth}
\centering
\includegraphics[width=0.975\textwidth]{Results/CompUW300-crop.pdf}
\end{minipage}
\caption{Performance of Core-Boosted-30s, Linear-Search and Core-Guided compared to the results of the 300s weighted (left) and unweighted (right) track of the 2018 MaxSAT Evaluation.\label{fig:comp}}
\end{figure}
\iffalse
\begin{table}[htbp]
\caption{Performance of core-boosted linear search in the 60s tracks of the MaxSAT Evaluation. In the table a value of N/A signifies a particular solver not participating in a particular track. \jerx{Remove table and write the info into the text if space problem}}
\centering
\begin{tabular}{l|r|r}
\multicolumn{1}{l|}{\textbf{Solver}} & \multicolumn{1}{l|}{\textbf{Weighted}} & \multicolumn{1}{l}{\textbf{Unweighted}} \\ \hline
\textbf{Core-Boosted-30s } & \textbf{0.814} & 0.696 \\ \hline
\textbf{Open-WBO-Inc-BMO} & 0.793 & \multicolumn{1}{r}{N/A} \\ \hline
\textbf{LinSBPS} & 0.779 & 0.672 \\ \hline
\textbf{maxroster} & 0.756 & 0.528 \\ \hline
\textbf{Open-WBO-Inc-Cluster} & 0.726 & \multicolumn{1}{r}{N/A} \\ \hline
\textbf{SATLike-c} & 0.683 & \textbf{0.699} \\ \hline
\textbf{Open-WBO-Gluc} & 0.656 & 0.588 \\ \hline
\textbf{SATLike} & 0.650 & 0.64 \\ \hline
\textbf{Open-WBO-Riss} & 0.626 & 0.542 \\ \hline
\textbf{Linear-Search } & 0.753 & 0.679 \\ \hline
\textbf{Core-Guided} & 0.657 & 0.481 \\ \hline
\textbf{Open-WBO-Inc-OBV} & \multicolumn{1}{r|}{N/A} & 0.627 \\ \hline
\textbf{Open-WBO-Inc-MCS} & \multicolumn{1}{r|}{N/A} & 0.607
\end{tabular}
\label{tab:60s}
\end{table}
\fi
\section{Conclusions} \label{sec:conc}
We proposed core-boosted linear search, a novel search strategy for incomplete MaxSAT solving, that combines the strengths of core-guided and linear search and is, to the best of our knowledge, the first effective application of core-guided reformulation techniques in incomplete MaxSAT solving.
Our experimental evaluation on a prototype implementation indicates that the information flow between the two phases of a core-boosted linear search solver
often allows it to perform better than either of its individual components, while very rarely performing significantly worse. Furthermore, our comparison to other incomplete
solvers shows that core-boosted linear search can be used to obtain state-of-the-art performance in weighted incomplete MaxSAT solving.
As future work we plan to develop more dynamic ways of deciding when to switch between
the core-guided and the linear search phase. Another interesting research directions to consider is the inclusion of MaxSAT preprocessing before, or even in-between, the core-guided and
linear phases. Finally we also plan to look into extensions of core-boosted linear search to other constraint optimization paradigms.
%\section{Acknowledgments}
\bibliographystyle{splncs04}
\bibliography{references}
\end{document}