---
abstract: 'The CDCL algorithm is the leading solution adopted by state-of-the-art solvers for SAT, SMT, ASP, and others. Experiments show that the performance of CDCL solvers can be significantly boosted by embedding domain-specific heuristics, especially on large real-world problems. However, a proper integration of such criteria in off-the-shelf CDCL implementations is not obvious. In this paper, we distill the key ingredients that drive the search of CDCL solvers, and propose a general framework for designing and implementing new heuristics. We implemented our strategy in an ASP solver, and we experimented on two industrial domains. On hard problem instances, state-of-the-art implementations fail to find any solution in acceptable time, whereas our implementation is very successful and finds all solutions.'
author:
- Carmine Dodaro
- Philip Gasteiger
- Nicola Leone
- |
    \
    Benjamin Musitsch
- Francesco Ricca
- Konstantin Schekotihin
title: Driving CDCL Search
---

Introduction
============

The Conflict Driven Clause Learning (CDCL) algorithm [@DBLP:journals/tc/Marques-SilvaS99] is the leading solution adopted by state-of-the-art solvers for Boolean Satisfiability (SAT) [@DBLP:series/faia/2009-185], Satisfiability Modulo Theories (SMT) [@DBLP:journals/jacm/NieuwenhuisOT06], and Answer Set Programming (ASP) [@DBLP:journals/cacm/BrewkaET11] to mention a few. Notably, CDCL solvers have been applied with success for solving several real-world problems ranging from hardware and software model checking, planning, equivalence checking, bioinformatics, configuration problems, hardware and software test, software package dependencies, cryptography and more [@DBLP:series/faia/2009-185].

As a matter of fact the performance of a CDCL solver heavily depends on the adoption of heuristics that drive the search for solutions. Among these, the heuristic for the selection of the branching literal (i.e., the criterion determining the literal to be assumed true at a given stage of the computation) can dramatically affect the overall performance of an implementation [@DBLP:series/faia/2009-185]. State-of-the-art CDCL implementations feature very good general purpose heuristics belonging to the family of VSIDS [@DBLP:conf/sat/BiereF15; @DBLP:conf/sat/EenS03; @DBLP:conf/dac/MoskewiczMZZM01]. Since their introduction, VSIDS heuristics proved to be a key ingredient for solving many relevant problems [@DBLP:conf/sat/BiereF15]. Nonetheless, no general heuristic is known to be the best possible choice for all problems [@DBLP:journals/ai/HutterXHL14]. Pioneering work on employing domain-specific heuristics corroborates the validity of that idea. In particular, Beame et al. demonstrated the utility of a domain-specific branching heuristic for solving the pebbling formulas with a CDCL solver [@DBLP:journals/jair/BeameKS04]; and Rintanen proposed to replace the standard VSIDS by a domain-heuristics for efficiently solving planning as satisfiability [@DBLP:journals/ai/Rintanen12]. Moreover, Gerhard Friedrich in his joint invited talk at CP-ICLP 2015 described a number of experiences in which “domain-specific heuristics turned out to be the key component in several industrial applications of problem solvers” [@InvitedFriedrich15]. However, as argued in [@DBLP:journals/ai/Rintanen12]: “the main challenge in defining a variable selection scheme is its integration in the CDCL algorithm in a productive way”. Indeed, domain experts can quickly provide promising heuristic-criteria based on properties of solutions, but they may not have the knowledge and the experience to plug them in CDCL implementations.

The goal of the paper is to ease the design and the evaluation of new heuristics for CDCL solvers as well as to reduce the efforts needed to provide effective implementations. To this end we distill the key ingredients that drive the search of CDCL solvers, and propose a general framework for designing and implementing new heuristics. Useless to say that one could invent new heuristics based on other different “ingredients”. Nevertheless, our framework is quite rich and flexible, and indeed it covers the definition of the most popular heuristics for CDCL, as well as enables the definition of interesting problem-specific heuristics. Moreover, further features could be easily incorporated. A number of examples are provided to demonstrate the applicability of the proposed framework for defining a variety of known heuristic criteria from the literature [@DBLP:conf/sat/BiereF15; @DBLP:journals/ai/Rintanen12]. Pragmatic evidence of the benefits of our framework in devising problem-specific heuristics is provided by reporting on a use case where two hard industrial domains defined by Siemens, the Partner Units Problem ([PUP]{}) [@DBLP:conf/iaai/TeppanFF12] and Combined Configuration Problem ([CCP]{}) [@DBLP:conf/lpnmr/GebserRS15], are solved efficiently.

In our use case, the framework has been implemented by extending the ASP solver [<span style="font-variant:small-caps;">wasp</span>]{} [@DBLP:conf/lpnmr/AlvianoDLR15]. Our implementation offers a wide range of possibilities to end users for developing new heuristics. In particular, it offers multi-language support including scripting languages for fast prototyping, an embedded C++ interface for performance-oriented implementations, as well as heuristic definition by means of declarative predicate-based paradigms.

Experiments on [PUP]{}and [CCP]{}confirm the viability of the framework in real-world scenarios, and the effectiveness of our implementation that is able to solve successfully hard problem instances which were not solvable by state-of-the-art ASP solvers. Furthermore, we were able to solve hardest [CCP]{}instances for which no solution was known before.

An overview of the CDCL algorithm
=================================

In this section we provide some basic knowledge about the Conflict-Driven Clause Learning (CDCL) algorithm [@DBLP:journals/tc/Marques-SilvaS99] for solving the satisfiability problem (SAT)  [@DBLP:conf/sat/BiereF15]. The Conflict-Driven Clause Learning (CDCL) [@DBLP:journals/tc/Marques-SilvaS99] backtracking search algorithm is a de facto standard for the satisfiability problem (SAT) [@DBLP:conf/ijcai/AudemardS09; @DBLP:conf/sat/BiereF15]. During the recent years, CDCL has been extended in order to fit specific requirements of formalisms in the neighborhood of SAT, e.g. Satisfiability Modulo Theories and Answer Set Programming. In the following, we first introduce some basic concepts of the satisfiability problem and then we describe the CDCL algorithm.

#### SAT.

Let $\A$ be a fixed, countable set of propositional atoms including $\bot$. A literal $\ell$ is either an atom $a$ or its negation $\neg a$, and $atom(\ell)=a$ denotes the atom associated to $\ell$. The complement of $\ell$ is denoted by $\overline{\ell}$, where $\overline{a} = \neg a$ and $\overline{\neg a} = a$ for an atom $a$. For a set $L$ of literals, $\overline{L} := \{\overline{\ell} \mid \ell \in L\}$, $L^+ :=L \cap \A$, and $L^- := \overline{L} \cap \A$. A (partial) interpretation is a set of literals $I$ containing $\lnot \bot$. $I$ is inconsistent if $I^+ \cap I^- \neq \emptyset$, otherwise $I$ is consistent. $I$ is total if $I^+ \cup I^- = \A$. Given an interpretation $I$, a literal $\ell$ is true if $\ell \in I$; is false if $\overline{\ell} \in I$, and is undefined otherwise. A clause $\varphi$ is a set of literals, and a formula $\Gamma$ is a set of clauses. An interpretation $I$ satisfies a clause $\varphi$ if $\varphi \cap I \neq \emptyset$. A consistent, total interpretation $I$ is a model of a formula $\Gamma$ if all clauses in $\Gamma$ are satisfied. A formula $\Gamma$ is said to be consistent if it admits some model, inconsistent otherwise. Given a formula $\Gamma$, the SAT problem consists in determining whether $\Gamma$ is consistent.

\[ex:ex1\] Consider the formula $\Gamma=\{\{a, b,\neg c\}, \{a\},$ $ \{\neg b\}, \{c, d\}, \{c, \neg d\}\}$. $I=\{a,\neg b, c, d\}$ is a model of $\Gamma$.

#### CDCL algorithm.

The CDCL algorithm takes as input a formula $\Gamma$, and determines whether it is consistent. The first step of the algorithm consists of the simplification of $\Gamma$. Polynomial algorithms for clause rewriting and variable elimination are applied on $\Gamma$, which strengthen and/or remove redundant clauses [@DBLP:conf/sat/EenB05]. After the simplifications step, the partial interpretation $I$ is set to $\{\lnot \bot\}$, and the backtracking search starts. First, $I$ is extended with all the literals that can be deterministically inferred by applying some inference rule (*propagation* step). The main inference rule of a SAT solver is *unit propagation* that extends $I$ by an undefined literal $\ell$ whenever there is a clause $\varphi\in\Gamma$ such that $\ell \in \varphi$ and $\varphi \setminus \ell \subseteq \overline{I}$. Three cases are possible after a propagation step is completed: $(i)$ $I$ is consistent but not total. In that case, an undefined literal $\ell$ (called *branching literal*) is chosen according to some heuristic criterion, and is added to $I$. Then, a propagation step is performed that infers the consequences of this choice. $(ii)$ $I$ is inconsistent, thus there is a conflict, and $I$ is analyzed. The reason of the conflict is modeled by a fresh clause $\varphi$ that is added to $\Gamma$ (clause *learning*), e.g. by applying the *first Unique Implication Point (UIP)* technique [@DBLP:conf/iccad/ZhangMMM01]. Moreover, the algorithm backtracks (i.e. choices and their consequences are undone) until the consistency of $I$ is restored. Then the algorithm propagates inferences starting from the fresh clause $\varphi$. Otherwise, if the consistency of $I$ cannot be restored, the algorithm terminates returning [<span style="font-variant:small-caps;">inconsistent</span>]{}. Finally, in case $(iii)$ $I$ is consistent and total, i.e. $I$ is a model, the algorithm terminates returning [<span style="font-variant:small-caps;">consistent</span>]{}.

\[ex:ex2\] Consider the formula $\Gamma$ of Example \[ex:ex1\]. The search starts with $I:=\{\lnot \bot\}$. Unit propagation extends $I$ with $a$ and $\neg b$ to satisfy clauses $\{a\}$ and $\{\neg b\}$. No other inferences can be done, thus a choice is performed among $c$, $\neg c$, $d$, and $\neg d$. Choosing $\neg c$ would lead to an inconsistency, while all other choices would directly lead to a model.

#### Heuristics.

It is well-known that the selection the branching literal plays a crucial role for efficiency. Nowadays, state-of-the-art solvers, such as [<span style="font-variant:small-caps;">lingeling</span>]{} [@DBLP:conf/sat/BiereF15] and [<span style="font-variant:small-caps;">glucose</span>]{} [@DBLP:conf/ijcai/AudemardS09], implement branching criteria belonging to the VSIDS [@DBLP:conf/dac/MoskewiczMZZM01] family that are a variant of the [<span style="font-variant:small-caps;">minisat</span>]{} [@DBLP:conf/sat/EenS03] heuristic. Thus, in the following, the [<span style="font-variant:small-caps;">minisat</span>]{} [@DBLP:conf/sat/EenS03] heuristic is referred to as the *default branching heuristic* of a CDCL solver. The [<span style="font-variant:small-caps;">minisat</span>]{}heuristic is based on the *activity* value for each atom in the input formula $\Gamma$, which is initially set to 0. The activity of $atom(\ell)$ is incremented by a value $inc$ when a literal $\ell$ occurs in a learned clause. Then, after learning the clause, the value of $inc$ is multiplied by a constant slightly greater than 1, to give more and more importance to variables that occur in recently-learned clauses. Once a choice is needed, the literal $\lnot at$ is chosen, where $at$ is the undefined atom having the highest activity value (ties are broken randomly).

For the sake of completeness, we mention that the CDCL is usually complemented with heuristics that control the number of learned clauses, and restart the computation to explore different branches of the search tree [@DBLP:series/faia/2009-185].

Driving CDCL Search {#sec:heur}
===================

[|p[.9]{}|]{}\
\
\
*Triggered when the backtracking search starts. $\Gamma'$ and $\A'$ are the formula and the atoms after the simplifications, resp.*\
\
\
*Triggered when the choice $\ell$ led to an inconsistency.*\
\
\
*Triggered when a conflict is detected after the choice of $\ell$.*\
\
\
*Triggered when the clause $\varphi$ is learned.*\
\
\
*Triggered when the literal $\ell$ is involved in the creation of a clause to learn, e.g., while applying the first UIP schema.*\
\
\
*Triggered when the clause $\varphi$ has been removed.*\
\
\
*Triggered when a restart of the search occurs.*\
\
\
*Triggered during backtracking if the literal $\ell$ is set to undefined.*\

In this section we present the results of our studies pinpointing the key ingredients needed to drive the search of CDCL solvers. These were distilled by considering the needs of well-known heuristics, as well as by applying the lessons learned while developing domain-specific heuristics in the case study reported in the next section.

In our framework we identify two main actors: the *solver* and the *driver*. The first is, basically, an implementation of the CDCL algorithm, and the second implements an external branching heuristic.

Selection of a branching literal may depend (or not depend) on properties of the input, on the (current) solver state, on employed optimization techniques (e.g., input rewritings), as well as on the status of variables that directly model some properties of the problem, etc. This information is possibly communicated by the solver to the driver by means of *events*. Events can be seen as asynchronous messages sent to the driver when specific points of the computation are reached, as detailed in Table \[tab:events\]. The driver could exploit this information to implement the heuristic criteria, e.g., updating counters or modifying its status. None of the events are mandatory for the driver (we expect that an efficient implementation smartly sends only those required by the driver).

We have also identified two main moments in the computation when the solver gets directions from the driver. These are modeled in our framework by means of *requests*, that are detailed in Table \[tab:responses\] together with the *responses* the solver expects to receive. Requests are synchronous, i.e., the solver waits for a response of (i.e., a command from) the driver.

The request [<span style="font-variant:small-caps;">GetAtomsToBeFrozen</span>($\A$)]{} is sent before starting the simplifications of the input formula. In fact, preprocessing can remove atoms that the heuristic strategy may want to keep (they may play a role in a domain-specific heuristic). The response [<span style="font-variant:small-caps;">\#Freeze($A \subseteq \A$)</span>]{} informs the solver to avoid eliminating the variables in $\A$.

[|p[.9]{}|]{}\
\
\
*Asks the heuristic strategy to provide a list of atoms $A \subseteq \A$ that must not be removed by simplifications.*\
\

[|p|]{}\
\
*Asks to not remove atoms in $A$ during preprocessing.*\

\
\
\
*Asks the heuristic strategy to provide the next branching literal(s) given the current interpretation $I$.*\
\

[|p|]{}\
\
*Asks the solver to perform the choices in list $\L$. $\L$ contains tuples of the form ($at,sign$), where $at \in \A'$ and $sign \in \{p,n,f\}$. Given tuple $(at,sign)$, the solver chooses $at$ if $sign=p$, $\neg at$ if $sign=n$, and if $sign=f$ the CDCL is left free to choose the sign.*\
\
\
*Asks the solver to backtrack until $\ell$ becomes undefined. To trigger a restart set $\ell=\bot$.*\
\
\
*Asks the solver to use the default heuristics for the next $n$ choices. The default heuristic is enable permanently if $n \leq 0$. Parameters $\I, \F, \S$ initialize the default heuristics as follows: $\I: A \rightarrow \mathbb{N}$ provides the initial activity of atoms; $\F: A \rightarrow \mathbb{N}$ associates to atoms an amplifying factor; $\S: A \rightarrow \{p,n\}$ to provide a priority on the sign of literals.*\
\
\
*Asks the solver to add the clause $\varphi$ to the formula.*\

\

The [<span style="font-variant:small-caps;">GetChoice</span>($I$)]{} request is the main one, and is made by the solver when a non-deterministic choice is required. A number of responses are possible besides the obvious one where the driver provides the solver with an ordered list of branching literals to be chosen. The list can hold just one element as in many well-known heuristics, or can provide in one call several choices so to reduce communication overheads in domain-heuristics that may provide at once an entire plan of choices. Alternative responses were inspired by domain-specific criteria. For example, the driver is likely to recognize specific paths in the search space that cannot lead to a solution, so it can issue a [<span style="font-variant:small-caps;">Unroll</span>($\ell$)]{} to cause a backtrack up to the last choice made before $\ell$. Moreover, the driver could add some additional domain knowledge modeled by a clause $\varphi$ in the solver by answering [<span style="font-variant:small-caps;">\#AddClause($\varphi$)</span>]{}. Finally, there are cases (see next section) in which it makes sense to blend custom heuristics with the default heuristic, to exploit the strengths of both. To this end the driver can respond [<span style="font-variant:small-caps;">\#Fallback($n,\I,\F,\S$)</span>]{} so to force the solver to use its default heuristic for the next $n$ choices. The parameters of [<span style="font-variant:small-caps;">\#Fallback(.)</span>]{} allow to customize this interaction by (possibly) tuning the activity values and the multiplying factors used by the default heuristic.

In the following we provide a number of examples that show how to encode several well-known conflict-based and domain-specific heuristics. This way the reader can appreciate the generality of our proposal that cover the needs of a wide range of conflict-based heuristics as well as domain-heuristics proposed in the literature. Nevertheless, we remark that our framework can be easily extended by adding new events/requests to fit the needs of future applications.

\[ex:minisat\] We first consider the [<span style="font-variant:small-caps;">minisat</span>]{}heuristic as described in [@DBLP:conf/sat/EenS03]. This criterion can be implemented in our framework by exploiting the events [<span style="font-variant:small-caps;">OnStartSearch($\Gamma',\A'$)</span>]{} and [<span style="font-variant:small-caps;">OnLearnClause($\varphi$)</span>]{}, as well as the [<span style="font-variant:small-caps;">GetChoice</span>($I$)]{} request. The first is used to initialize the activity values of atoms in the input; the second causes an increment the activity of atoms in the learned clause $\varphi$. Finally, the request [<span style="font-variant:small-caps;">GetChoice</span>($I$)]{} is answered with [<span style="font-variant:small-caps;">\#Choice($\{(a,n)\}$)</span>]{} by the driver, where $a$ is the undefined atom in $I$ with the highest value of activity.

\[ex:pigeonhole\] Consider the famous pigeonhole problem: given $n$ pigeons and $m$ holes, assign each pigeon to exactly one hole in such a way that two different pigeons do not share the same hole. It can be verified that state-of-the-art SAT solvers are not able to solve this problem efficiently when $n > m$, despite it is known that no solution exists in that case. A domain-specific heuristic based on this observation only uses the requests and no event. To [<span style="font-variant:small-caps;">GetAtomsToBeFrozen</span>($\A$)]{} the driver answers to not remove any atom (providing [<span style="font-variant:small-caps;">\#Freeze($\A$)</span>]{}), and computes $n$ and $m$ by interpreting the atoms in $\A$. Once the first choice is requested, if $n > m$ the heuristic replies with [<span style="font-variant:small-caps;">\#AddClause($\{\bot\}$)</span>]{} causing the termination of the CDCL returning [<span style="font-variant:small-caps;">inconsistent</span>]{}; otherwise, [<span style="font-variant:small-caps;">\#fallback($0, \emptyset, \emptyset, \emptyset$)</span>]{} is sent to go on with the default heuristic.

\[ex:rintanen\] In [@DBLP:journals/ai/Rintanen12], a heuristic for solving the planning problem modeled as SAT problem is proposed that intuitively forces the solver to prefer short and simple plans. This criterion can be implemented in our framework by using the event [<span style="font-variant:small-caps;">OnSearch($\Gamma',\A$)</span>]{}, and the request [<span style="font-variant:small-caps;">GetChoice</span>($I$)]{}. In fact, [<span style="font-variant:small-caps;">OnSearch(.)</span>]{} allows the driver to identify *actions* and *goals* literals; while the answer to [<span style="font-variant:small-caps;">GetChoice</span>(.)]{} is computed by running the algorithm in Figure 3 of [@DBLP:journals/ai/Rintanen12].

We mention that, one can easily obtain all the [<span style="font-variant:small-caps;">vsids</span>]{}-like heuristics described in [@DBLP:conf/sat/BiereF15] by applying small modifications to the solution presented in Example \[ex:minisat\].

Case study: Answer Set Programming
==================================

In this section we report on a case study that provides pragmatical evidence of the applicability of our framework. The case study is developed in the context of Answer Set Programming (ASP) [@DBLP:journals/cacm/BrewkaET11]. ASP is a declarative problem solving paradigm proposed in the area of logic programming and non-monotonic reasoning. ASP is an ideal test bed for our framework for two main reasons: $(i)$ ASP solvers are nowadays efficient CDCL implementations; $(ii)$ ASP has been applied to a variety of complex problems including hard industrial ones. In the following we first describe the implementation of our framework in a well-known ASP solver and, then, we report on the solution of two real-world configuration problems occurring in practice of Siemens: the Partner Units Problem ([PUP]{}) and the Combined Configuration Problem ([CCP]{}). These appeared to be among the hardest industrial benchmarks from the ASP Competition 2015 [@DBLP:conf/lpnmr/GebserMR15; @aspweb]; indeed, on hard problem instances state-of-the-art ASP solvers were not effective. Given the practical importance of these two problems, many researchers studied them in detail [@Falkner2010; @DBLP:conf/cpaior/AschingerDFGJRT11; @DBLP:conf/ijcai/AschingerDGJT11; @DBLP:conf/iaai/TeppanFF12; @DBLP:conf/ictai/Drescher12; @DBLP:conf/lpnmr/GebserRS15]. Their investigations resulted in a number of domain-specific heuristic approaches that, in some cases, significantly outperformed existing ASP solvers. We experimented with these heuristics, thus applying our framework in practice, to see whether these can be integrated successfully in a CDCL solver.

Implementation of the framework
-------------------------------

The framework has been implemented as an extension of the ASP solver [<span style="font-variant:small-caps;">wasp</span>]{}. [<span style="font-variant:small-caps;">wasp</span>]{}implements a variant of CDCL devised for evaluating ASP programs, thus featuring additional inference rules required for the evaluation of ASP programs, such as *unfounded-based* and *aggregate-based* inferences [@DBLP:journals/ai/GebserKS12]. The framework for specifying heuristics has been implemented in *C++* and it offers an infrastructure for easy specification and testing of heuristic strategies. The user can adopt several languages for implementing external heuristics that range from imperative to declarative ones. In particular, the heuristic strategies can be implemented in *perl* and *python* for obtaining fast prototypes and in *C++* for obtaining better performances. (In our tests, we observed that *C++* implementations are often faster than equivalent *perl* and *python* counterparts, which are usually easier to develop instead). In case the user would like to use a declarative language to implement a heuristic, our implementation provides a *predicates-based* interface extending the one proposed in [@DBLP:conf/aaai/GebserKROSW13]. We next sketch the idea by assuming that (on the lines of in [@DBLP:conf/aaai/GebserKROSW13]) one encodes the heuristic strategy in ASP by providing a logic program $\Pi$. Each request of the CDCL algorithm causes an evaluation of $\Pi$ together with *facts* modeling the request (intuitively, a fact is an atom that is always true). The evaluation of $\Pi$ with the aforementioned facts produces a set of atoms (i.e., the answer set produced by a solver) interpreted as responses for the request. For instance, consider Example \[ex:pigeonhole\], the request [<span style="font-variant:small-caps;">GetFrozenAtoms</span>($\A$)]{} is represented by the facts $get\_frozen\_atoms()$ and $atom(p(i,j))$ for each $p_{i,j} \in \A$. A call to an external solver produces an answer set containing $freeze(p(i,j))$, for each $p_{i,j} \in \A$, that is interpreted as [<span style="font-variant:small-caps;">\#Freeze($\A$)</span>]{}. Other request and corresponding responses are handled in a similar manner. Our implementation currently supports any external solver compliant with ASP solver output. The predicate-based interface can easily support variants of ASP (e.g., with *preferences* [@DBLP:conf/aaai/BrewkaD0S15], *CASP* [@DBLP:conf/iclp/GebserOS09], etc.) an could be adapted, in principle, also to support other languages based on predicate logic.

Partner Units Problem
---------------------

The [PUP]{}comes from the railway safety domain [@Falkner2010], but has a variety of other applications including security monitoring systems, peer-to-peer networks, etc. [@DBLP:conf/iaai/TeppanFF12]. In order to ensure the safety of train movements, railway tracks (see Figure \[fig:pup\_layout\]) are equipped with hardware *sensors* $s_1,\dots,s_6$ which register when a wagon passes by. All registered events are forwarded from sensors to *control units* $u_1,\dots,u_3$ belonging to a safety system. The latter has to prevent wagons of different trains from entering the same safety *zone* of the tracks $z_1,\dots,z_{24}$, hence avoiding unwanted collisions. To solve the problem one needs to (1) assign every zone and sensor to a control unit such that every unit is connected to at most [<span style="font-variant:small-caps;">UCap</span>]{}sensors and at most [<span style="font-variant:small-caps;">UCap</span>]{}zones. Moreover, (2) if a sensor contributes to a zone, it must be placed on the same or on a connected unit (partner unit). However, every unit can be a partner of at most [<span style="font-variant:small-caps;">IUCap</span>]{}other units.

#### Heuristics.

For our evaluation we selected the [<span style="font-variant:small-caps;">Quick[PUP]{}</span>]{}heuristic and its derivatives, since search algorithms using these heuristics were able to outperform best ASP solvers.

-   [<span style="font-variant:small-caps;">Quick[PUP]{}</span>]{} [@DBLP:conf/iaai/TeppanFF12] generates an order of zones and sensors in the first step by selecting some zone as a root and traversing the input zone-sensor relations breadth-first. Then, a depth-first search selects the next unassigned zone or sensor in the order and assigns it to a new unit. If the assignment cannot be done due to a violation of requirement (2), then the already used units are tested starting from the last created one. In case [<span style="font-variant:small-caps;">Quick[PUP]{}</span>]{}is not able to assign a zone or sensor to any unit it unrolls the last made assignment and tries another possibility. Finally, if no more assignments are possible, [<span style="font-variant:small-caps;">Quick[PUP]{}</span>]{}falls back to the default heuristic.

-   [$\textsc{Quick{PUP\xspace}}^*$]{}is a modification of [<span style="font-variant:small-caps;">Quick[PUP]{}</span>]{}that tests already used units first and a new one afterwards.

-   [<span style="font-variant:small-caps;">Pred</span>]{} [@DBLP:conf/ictai/Drescher12] tries first to connect an unassigned zone or sensor to one of the units that already have connections to neighbour zones or sensors, i.e. reachable over at most two input zone-sensor relations. If this fails, [<span style="font-variant:small-caps;">Pred</span>]{}tries a new unit first and used ones subsequently.

#### Implementation details.

We implemented the four heuristics in [<span style="font-variant:small-caps;">wasp</span>]{}using the C++ interface given in Section \[sec:heur\]. A heuristic is initialized as [<span style="font-variant:small-caps;">OnSearch($\Gamma',\A'$)</span>]{} event is invoked by the solver. Next, the ordering of vertices is generated and used to determine sets of chosen literals $L$ in response to [<span style="font-variant:small-caps;">GetChoice</span>($I$)]{} requests. In addition, a heuristic registers [<span style="font-variant:small-caps;">OnUnrollLit($\ell$)</span>]{} events in order to synchronize its inner state with decisions made by [<span style="font-variant:small-caps;">wasp</span>]{}between two subsequent [<span style="font-variant:small-caps;">GetChoice</span>($I$)]{} requests. If a heuristic finds that the current partial interpretation is inconsistent, i.e. no further assignments can be made, it backtracks and sends [<span style="font-variant:small-caps;">\#Unroll($\ell$)</span>]{} to [<span style="font-variant:small-caps;">wasp</span>]{}. In this case, $\ell$ is one of the literals that were selected by a heuristic at the previous choice event. Finally, the fallback from [<span style="font-variant:small-caps;">Quick[PUP]{}</span>]{}-based heuristics to the default one was implemented using [<span style="font-variant:small-caps;">\#Fallback($0,\emptyset,\emptyset,\emptyset$)</span>]{} response.

#### Setup.

The evaluation was done by using the set of instances provided by Siemens[^1]. This package comprises instances of four types: (1) double, (2) double-variant, (3) triple and (4) grid. The first three types are instances representing topologies occurring frequently in practice, whereas grids are parts of real railway systems (see [@DBLP:conf/cpaior/AschingerDFGJRT11] for details). The instances were tested with two encodings: [PUP]{}-E1 – the original straightforward encoding published in [@DBLP:conf/cpaior/AschingerDFGJRT11] (Section 3.1, p. 6) and [PUP]{}-E2 – a complex encoding comprising symmetry breaking and ordering rules used in the ASP Competition 2015. Moreover, in all experiments with [<span style="font-variant:small-caps;">wasp</span>]{}using heuristics, we removed rule 9 (line 14) from [PUP]{}-E2. This rule is a symmetry breaker that does not allow our heuristics to select the starting zone. For each encoding we grounded all instances with [<span style="font-variant:small-caps;">gringo</span>]{}(version 4.5.3). Then each solver was run for 900 sec.  on a system equipped with i7-3030K CPU, 64GB RAM and Ubuntu 11.10.

#### Results.

A summary of our evaluation results is presented in Figures \[fig:eval:a\] and \[fig:eval:b\]. The results of [<span style="font-variant:small-caps;">clasp</span>]{} [@DBLP:conf/aaai/GebserKROSW13], which was used as a reference system, show that it was able to solve at most 23 instances using the tested encodings. Moreover, in both experiments [<span style="font-variant:small-caps;">clasp</span>]{}failed to find a model for most of the double as well as for some double-variant and triple instances. Also [<span style="font-variant:small-caps;">wasp</span>]{}with [<span style="font-variant:small-caps;">Quick[PUP]{}</span>]{}solved only 12 and 15 instances using [PUP]{}-E1 and [PUP]{}-E2 respectively. The main reason for this discrepancy between our results and the ones obtained by [@DBLP:conf/iaai/TeppanFF12] is due to inability of the underlying ASP solver to generate new units on-the-fly. Therefore, the number of ground literals denoting available units is determined in the grounding step and cannot be changed later. [@DBLP:conf/iaai/TeppanFF12], instead, try to quickly build a solution by using new units whenever possible. This strategy appears to be successful for greedy algorithms, but works poorly as a heuristic for [<span style="font-variant:small-caps;">wasp</span>]{}.

The two remaining heuristics assign zones and sensors to already existing units first. This allowed [<span style="font-variant:small-caps;">wasp</span>]{}to outperform [<span style="font-variant:small-caps;">clasp</span>]{}and [<span style="font-variant:small-caps;">Quick[PUP]{}</span>]{}in all experiments. The best result was observed for [<span style="font-variant:small-caps;">wasp</span>]{}with [<span style="font-variant:small-caps;">Pred</span>]{}, which solved *all* instances independently of the encoding. Moreover, [PUP]{}-E2 allowed [<span style="font-variant:small-caps;">wasp</span>]{}to reduce its average solving time to only 27 sec. Finally, we would like to emphasize the fact that [<span style="font-variant:small-caps;">Pred</span>]{}allowed [<span style="font-variant:small-caps;">wasp</span>]{}to find solutions for all instances with the [PUP]{}-E1 encoding. This is an important feature of our approach. It allows a programmer to easily model a problem using a declarative language, like ASP-Core, and then to scale performance of the solver using heuristics defined in a procedural way.

Combined Configuration Problem
------------------------------

Similarly to the [PUP]{}, this problem was derived from a number of real-world problems including railway interlocking systems, safety automation, resource distribution, etc. The [CCP]{}is an abstract problem that demonstrates an important case occurring in practice of Siemens when a complex problem can be represented as a set of subproblems [@DBLP:conf/lpnmr/GebserRS15].

A [CCP]{}instance is defined by a directed acyclic graph $G=(V,E)$ representing a track layout (see Figure \[fig:ccp\]). Each vertex has a type, e.g. $b$ and $p$, with an associated size, e.g. 1 and 3. Furthermore, an instance includes two disjoint paths $P_1$ and $P_2$, shown in red and green, as well as several sets of border elements, e.g. $\mathit{BE}_1=\{b_1,b_2,b_3\}$ and $\mathit{BE}_2=\{b_2,b_4,b_5\}$. Finally, it defines parameters specifying a maximal number of border elements per safety area $M$, a number of colors $C$, a number of available bins $B$ per color and capacity of a bin $K$. The goal is to find a solution that satisfies all requirements of the following subproblems:

(P1) Coloring

:   Every vertex must have exactly one color.

(P2) Bin-Packing

:   For every set $V_i \subseteq V$ comprising all vertices of one color, assign each vertex $v_j \in V_i$ to exactly one bin such that for each bin the sum of the vertex sizes is less or equal to $K$ and at most $B$ bins are used.

(P3) Disjoint Paths

:   Colors of any two vertices $v_i \in P_1$ and $v_j \in P_2$ must be different.

(P4) Matching

:   For every input set of border elements $\mathit{BE}_i$ find a safety area $A_i\subseteq \mathit{BE}_i$ such that all border elements of one area are colored in one color, $|A_i| \leq M$ and every border element is exactly in one area.

(P5) Connectedness

:   Two vertices of the same color must be connected via a path that comprises only vertices of this color.

Let the sample [CCP]{}instance comprise the following parameters: $B=2$, $K=3$, $C=3$ and $M=3$. The solution presented in Figure \[fig:ccp\] assigns 3 colors to vertices, places them into 2 bins, shown in subscript of each vertex, and defines two safety areas $A_1=\{b_1,b_2,b_3\}$ and $A_2=\{b_4,b_5\}$.

#### Heuristics.

The [CCP]{}has a number of heuristics suggested in [@DBLP:conf/lpnmr/GebserRS15] which can be used to obtain a partial solution of a problem instance. It turned out that it is quite simple to find a heuristic that solves one or some of the subproblems. However, no complete heuristics, like [<span style="font-variant:small-caps;">Quick[PUP]{}</span>]{}or [<span style="font-variant:small-caps;">Pred</span>]{}for [PUP]{}, are known for [CCP]{}.

The heuristics suggested in [@DBLP:conf/lpnmr/GebserRS15] were designed to be used with the heuristic interface of [<span style="font-variant:small-caps;">clasp</span>]{}. This interface allows a programmer to define a heuristic function in the program using $\_heuristic/4$ predicate. If a ground “heuristic” atom over this predicate becomes true in a partial interpretation, then terms of the atom are used by [<span style="font-variant:small-caps;">clasp</span>]{}to modify behavior of the [<span style="font-variant:small-caps;">vsids</span>]{}heuristic. Therefore, given a [CCP]{}instance, the proposed approach first runs a heuristic search method to find a partial solution of the instance. Next, [<span style="font-variant:small-caps;">clasp</span>]{}is forced to start the search from the found partial solution by expending the [CCP]{}instance with facts comprising “heuristic” atoms representing it. Gebser et al. [@DBLP:conf/lpnmr/GebserRS15] use three heuristics:

-   [A1]{} solves the matching problem (P4). In every iteration it assigns an unassigned border element to a safety area which comprises the minimum number of already assigned elements.

-   [A2]{}. This heuristic is designed to solve three subproblems (P1), (P2) and (P5). First, it sets the color to 1 and adds some vertex $v \in V$ to a queue $Q$. Next, it retrieves an element $v_i \in Q$, assigns it the current color, places it to a bin according to the best-fit heuristic and adds all uncolored neighbors of $v_i$ to $Q$. The process continues, until no further vertices can be placed to bins. In this case the algorithm increases the value of current color and adds some uncolored node $v_j$ to $Q$.

-   [A1A2]{}. This is a combination of the previous two which first applies [A1]{} and then uses [A2]{} to extend the output of [A1]{}.

All original heuristics were designed to run only once prior to solving whereas in our solver a heuristic is queried multiple times. Therefore, we suggest the following modifications:

-   [A2F]{}is based on [A2]{} which is extended with a fallback to a default solver heuristic if (i) a partial solution is found or (ii) the 10 seconds timeout is reached or (iii) [A2]{} cannot make a choice. The latter situation might occur if all atoms used in subproblems (P1), (P2) and (P5) already have assigned truth values.

-   [A2FO]{}. Originally [A2F]{}processes the vertices of $G$ in no specific order. To increase its performance we extended [A2F]{}with an ordering that assigns a score of $2$ to all vertices with only incoming or outgoing edges, a score of $1$, it is in a path, and $3$, if both applies. Then, [A2FO]{}runs [A2F]{}such that in every iteration it sorts the unprocessed vertices in the decreasing order of their scores.

-   [A2AFO]{}. This version of [A2FO]{}uses a fallback strategy which alternates between [A2FO]{}and a default solver heuristic. Thus, [A2AFO]{}runs [A2FO]{}with the first ordering until it cannot make any further choices. Then, it switches to the default heuristic for the next 10 seconds. If solver was unable to get a complete solution within this time, [A2AFO]{}creates a new ordering and executes [A2FO]{}once more. In the case all possible orderings starting with vertices with a score higher than zero has been used, [A2AFO]{}falls back to the default heuristic permanently. The idea is to allow the default heuristic of the solver to acquire enough representative conflicts and hence to improve its performance.

#### Implementation details.

The heuristics were implemented similarly to the ones used for the [PUP]{}using the C++ version of the [<span style="font-variant:small-caps;">wasp</span>]{}interface. When [A2AFO]{}decides to use the default solver heuristic, it starts a timer and responses all [<span style="font-variant:small-caps;">GetChoice</span>($I$)]{} requests with [<span style="font-variant:small-caps;">\#Fallback($1,\emptyset,\emptyset,\emptyset$)</span>]{}. When the timeout is reached, [A2AFO]{}generates another ordering, restarts the search using [<span style="font-variant:small-caps;">\#Unroll($\bot$)</span>]{} and answers all subsequent requests itself.

#### Setup.

We evaluated [A2F]{}, [A2FO]{}and [A2AFO]{}on the set of hard instances[^2] and the encoding submitted to the ASP Competition 2015. The package contains a set of real-world instances used in the evaluation of [@DBLP:conf/lpnmr/GebserRS15] as well as a number of new instances. The latter have a grid-like graph structure in which all vertices are of the same type. The evaluation was done in the same settings as the [PUP]{}and similar to [@DBLP:conf/lpnmr/GebserRS15]. The average grounding time was about 2 seconds and is excluded from results.

#### Results.

The evaluation results, presented in Figure \[fig:eval:c\], show that the reference system could solve 3 out of 36 instance with an average solution time of 246 sec. Our approach using [A2F]{}, [A2FO]{}and [A2AFO]{}heuristics was able to solve 22, 27 and 36 instances with an average solution time 6, 7, and 14 sec.  resp. [A2AFO]{}heuristic has a greater solving time only because it was able to solve the hardest instances. Our approach shows also better results in comparison with  [@DBLP:conf/lpnmr/GebserRS15], which solved 6 out of 16 real-world instances.

Moreover, since [A2AFO]{}is based on an alternating usage of two heuristics we performed an additional evaluation. The goal was to test whether conflict learning is essential or the heuristic has to find a “correct” ordering as it was often the case for [PUP]{}heuristics. Therefore, we saved the last ordering [A2AFO]{}used before the last fallback and then started a new experiment in which this ordering was used first. The results show that in none of the experiments this strategy allowed [<span style="font-variant:small-caps;">wasp</span>]{}to find a solution with only one fallback. In all test cases [A2AFO]{}run [A2]{} at least twice, i.e. generates at least two orderings, to find a solution. This indicates that learned clauses are essential.

Conclusion
==========

The branching heuristic is a key ingredient of the CDCL algorithm. Despite several effective heuristics have been proposed in the literature, their integration in existing solvers is usually nontrivial. The paper proposed a novel framework that simplifies the design of new heuristics for CDCL solvers by distilling the key ingredients useful to drive the search. The proposal has been validated in a case study where our framework was employed for solving effectively two hard industrial problems. Results are positive: hard instances that were not solvable by previous approaches are efficiently solved by our implementation. Ongoing work concerns the implementation of our framework in other well-known solvers. Moreover, we plan to apply it in further practical use cases.

Acknowledgements {#acknowledgements .unnumbered}
================

This work was partially supported by the Carinthian Science Fund (KWF) contract KWF-3520/26767/38701, the Austrian Science Fund (FWF) contract I 2144 N-15, the Italian Ministry of University, Research under PON project “Ba2Know (Business Analytics to Know) Service Innovation – LAB”, No.  PON03PE\_00001\_1, and by the Italian Ministry of Economic Development under project “PIUCultura (Paradigmi Innovativi per l’Utilizzo della Cultura)” n. F/020016/01–02/X27.

[10]{} \[1\][`#1`]{}

Alviano, M., Dodaro, C., Leone, N., Ricca, F: [Advances in WASP]{}. In [LPNMR]{} 2015. pp. 40–54. (2015)

Aschinger, M., Drescher, C., Friedrich, G., Gottlob, G., Jeavons, P., Ryabokon, A., Thorstensen, E.: [Optimization Methods for the Partner Units Problem]{}. In: [CPAIOR]{} 2011. pp. 4–19. (2011)

Aschinger, M., Drescher, C., Gottlob, G., Jeavons, P., Thorstensen, E.: [Tackling the Partner Units Configuration Problem]{}. In: [IJCAI]{} 2011. pp. 497–503. (2011)

Audemard, G., Simon, L.: [Predicting Learnt Clauses Quality in Modern [SAT]{} Solvers]{}. In: [IJCAI]{} 2009. pp. 399–404. (2009)

Beame, P., Kautz, H.A., Sabharwal, A.: [Towards Understanding and Harnessing the Potential of Clause Learning]{}. J. Artif. Intell. Res. [(JAIR)]{} 22, 319–351 (2004)

Biere, A., Fr[ö]{}hlich, A.: [Evaluating [CDCL]{} Variable Scoring Schemes]{}. In: [SAT]{} 2015. pp. 405–422. (2015)

Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.): [H]{}andbook of [S]{}atisfiability, Frontiers in Artificial Intelligence and Applications, vol. 185. [IOS]{} Press (2009)

Brewka, G., Delgrande, J.P., Romero, J., Schaub, T.: [asprin: Customizing Answer Set Preferences without a Headache]{}. In: [AAAI]{} 2015. pp. 1467–1474. (2015)

Brewka, G., Eiter, T., Truszczynski, M.: [Answer set programming at a glance]{}. Commun. [ACM]{} 54(12), 92–103 (2011)

Drescher, C.: [T]{}he [P]{}artner [U]{}nits [P]{}roblem a [C]{}onstraint [P]{}rogramming [C]{}ase [S]{}tudy. In: [ICTAI]{} 2012. pp. 170–177. (2012)

E[é]{}n, N., Biere, A.: [Effective Preprocessing in [SAT]{} Through Variable and Clause Elimination]{}. In: [SAT]{} 2005. pp. 61–75. (2005)

E[é]{}n, N., S[ö]{}rensson, N.: [An Extensible SAT-solver]{}. In: [SAT]{} 2003. pp. 502–518. (2003)

Falkner, A., Haselb[ö]{}ck, A., Schenner, G.: [Modeling Technical Product Configuration Problems]{}. In: Workshop on Configuration, ECAI 2010. pp. 40–46. (2010)

Friedrich, G.: Industrial success stories of [ASP]{} and [CP]{}: What’s still open? (2015), joint invited talk at ICLP and CP 2015

Gebser, M., Kaufmann, B., Romero, J., Otero, R., Schaub, T., Wanko, P.: [Domain-Specific Heuristics in Answer Set Programming]{}. In: [AAAI]{} 2013. (2013)

Gebser, M., Kaufmann, B., Schaub, T.: [Conflict-driven answer set solving: From theory to practice]{}. Artif. Intell. 187, 52–89 (2012)

Gebser, M., Maratea, M., Ricca, F.: The design of the sixth answer set programming competition report. In: [LPNMR]{} 2015. pp. 531–544. (2015)

Gebser, M., Maratea, M., Ricca, F.: The sixth answer set programming competition web site. <http://aspcomp2015.dibris.unige.it/>

Gebser, M., Ostrowski, M., Schaub, T.: [Constraint Answer Set Solving]{}. In: [ICLP]{} 2009. pp. 235–249. (2009)

Gebser, M., Ryabokon, A., Schenner, G.: [Combining Heuristics for Configuration Problems Using Answer Set Programming]{}. In: [LPNMR]{} 2015. pp. 384–397. (2015)

Hutter, F., Xu, L., Hoos, H.H., Leyton[-]{}Brown, K.: [Algorithm runtime prediction: Methods [&]{} evaluation]{}. Artif. Intell. 206, 79–111 (2014)

Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: [Chaff: Engineering an Efficient [SAT]{} Solver]{}. In: [DAC]{} 2001. pp. 530–535. (2001)

Nieuwenhuis, R., Oliveras, A., Tinelli, C.: [Solving [SAT]{} and [SAT]{} Modulo Theories: From an abstract Davis–Putnam–Logemann–Loveland procedure to DPLL(*T*)]{}. J. [ACM]{} 53(6), 937–977 (2006)

Rintanen, J.: [Planning as satisfiability: Heuristics]{}. Artif. Intell. 193, 45–86 (2012)

Silva, J.P.M., Sakallah, K.A.: [[GRASP:]{} [A]{} Search Algorithm for Propositional Satisfiability]{}. [IEEE]{} Trans. Computers 48(5), 506–521 (1999)

Teppan, E.C., Friedrich, G., Falkner, A.A.: [QuickPup: [A]{} Heuristic Backtracking Algorithm for the Partner Units Configuration Problem]{}. In: IAAI 2012. (2012)

Heuristic Wasp Website. [<http://yarrick13.github.io/hwasp/>]{}

Zhang, L., Madigan, C.F., Moskewicz, M.W., Malik, S.: [Efficient Conflict Driven Learning in Boolean Satisfiability Solver]{}. In: [ICCAD]{} 2001. pp. 279–285. (2001)

[^1]: http://demo2-iwas.uni-klu.ac.at/pupsolver/benchmark.rar

[^2]: http://isbi.aau.at/hint/images/ccp/ccp.tgz
