Inferring Simple Solutions to Recursion-freeHorn Clauses via Sampling⋆
Hiroshi Unno1 and Tachio Terauchi2
1

University of Tsukuba
uhiro@cs.tsukuba.ac.jp
2
JAIST
terauchi@jaist.ac.jp

Abstract. Recursion-free Horn-clause constraints have received muchrecent attention in the verification community. It extends Craig interpolation, and is proposed as a unifying formalism for expressing abstraction refinement. In abstraction refinement, it is often desirable to infer“simple” refinements, and researchers have studied techniques for inferring simple Craig interpolants. Drawing on the line of work, this paper
presents a technique for inferring simple solutions to recursion-free Hornclause constraints. Our contribution is a constraint solving algorithm
that lazily samples fragments of the given constraints whose solution
spaces are used to form a simple solution for the whole. We have implemented a prototype of the constraint solving algorithm in a verification
tool, and have confirmed that it is able to infer simple solutions that aid
the verification process.

1

Introduction

In program verification, Craig interpolation [3] is a technique for discovering
predicates that can be used to prove the correctness of the given program. For
example, in predicate abstraction, interpolants from the formula representing
the counterexample are used as predicates to refute the counterexample [7], andin lazy abstraction via interpolation, interpolants from the formula representing the program unwinding are used to construct sufficient loop invariants [12].
In general, there is more than one interpolant that can be inferred from thesame formula, and which interpolant is inferred can significantly affect the performance of the client verifier. The “goodness” of an interpolant is an elusive
characteristic, and while there is not yet a definite measure, it has been suggested that simple interpolants often work better (perhaps justified by the belief
that correct programs tend to be correct for simple reasons, per Occam’s razor). Recently, researchers have proposed to infer simple interpolants between apair of formulas by sampling conjunctions of atoms from each formula, inferring
their interpolant, and repeating the process until the interpolant for the whole⋆This work was supported by MEXT Kakenhi 23220001, 26330082, 25280023, and25730035.

is found [17, 1]. By inferring simple interpolants for the samples that are likely
to generalize, the method efficiently infers a simple interpolant for the whole.
In this paper, we extend the idea to inferring simple solution to recursion-free
Horn-clause constraints. Recently, recursion-free Horn-clause constraints havereceived much attention in the verification community as they generalize interpolation and can express the predicate discovery process of a wide variety ofsoftware verifiers (imperative, procedural, higher-order functional, concurrent,
etc. [20, 18, 6, 5, 4, 14, 2, 19]).3 We emphasize that inferring a simple solution torecursion-free Horn-clause constraints is non-trivial and cannot be done by simply applying the methods for interpolation, because one must look simultaneously
for simple predicates to be assigned to each predicate variable in the given constraints that together satisfy the constraints (e.g., it cannot be done by justiteratively applying interpolation as a blackbox process [20, 18]).
The key ideas in our approach are to 1.) maintain as samples conjunctive
recursion-free Horn-clause constraint that only contain clauses whose formula
part is a conjunction of atoms, 2.) infer a simple solution to the samples via
a novel decompositional approach (cf. Sections 3.1–3.3), and 3.) check if thesolution inferred for the samples is also a solution for the whole, and if not,obtain a new sample as a counterexample and repeat the process. Finally, 4.)instead of computing a concrete solution for each subproblem, we compute an
abstract solution space representing a possibly infinite set of solutions, thereby
making the process more likely to be able to find a simple solution for the whole.
Related Work. Besides the above sampling-based approaches to inferring simple interpolants that inspired this work, previous research has proposed to infer
simple interpolants by post-processing the proof (of |= φ1 ⇒ φ2 ) in a proof-based
interpolation [8].
To our knowledge, this paper is the first work on inferring simple solutions torecursion-free Horn-clause constraints. Existing approaches to solving recursionfree Horn-clause constraints can be classified into two types: the iterative approach that uses interpolation as a blackbox process to solve the constraints one
predicate variable at a time [20, 18], and the constraint-expansion approach that
reduces the problem to tree interpolation (equivalently, solving “tree-like” constraints) [11, 13, 14]. As remarked above, the iterative approach is unsuited for
inferring simple solutions because a solution inferred for one predicate variable
can affect the rest and block the discovery of a simple solution for the whole.
The constraint-expansion approach is also unsuited for inferring simple solutions
because it makes exponentially many copies of predicate variables whose solutions are conjuncted to form the solution for the original, thereby resulting in acomplex solution (see also the discussion in Section 3.1).
Paper Organization. The rest of the paper is organized as follows. Section 2
presents preliminary definitions. Section 3 and its subsections describe the new
constraint solving algorithm in a top-down manner. We first present the top3

Interpolation between φ1 and φ2 is equivalent to solving the Horn-clause constraint{P (ex) ⇐ φ1 , ⊥ ⇐ P (ex) ∧ ¬φ2 } where {ex} = fvs(φ1 ) ∩ fvs(φ2 ).

level process in Section 3. Section 3.1 describes the sub-algorithm for inferring
simple solutions for samples. As we explain there in more detail, inferring simple
solutions to samples requires its own innovations as simply applying the existing approaches can produce complex solutions. To this end, we present a novel
approach where the problem is decomposed into smaller subproblems for whichsimple solutions can be found easily and combined to form a simple solution for
the whole sample set. We describe the approach in detail in Sections 3.1–3.3. We
report on a preliminary implementation and experiment results in Section 4, andconclude the paper in Section 5. Appendix contains extra materials and proofs
omitted from the main body of the paper.

2

Preliminaries

A formula φ in the signature of quantifier-free linear rational arithmetic (QFLRA)
is a Boolean combination of atoms. An atom (or literal) p is an inequality of theform t1 ≥ t2 or t1 > t2 where ti are terms. A term t is either a variable x, a
rational constant r, a multiplication of a term by a rational constant r · t, or asummation of terms t1 + t2 . We write ⊥ and ⊤ respectively for contradiction
and tautology. A predicate variable application a is of the form P (et) where P isa predicate variable of the arity |et|. We write ar(P ) for the arity of P .
A Horn clause (or simply clause) hc is defined to be of the form a0 ⇐ a1 ∧· · · ∧ an ∧ φ. We call a0 (resp. a1 ∧ · · · ∧ an ∧ φ) the head (resp. body) of hc.
We write fvs(hc) (resp. fvs(φ)) for the set of term variables in hc (resp. φ). We
write pvL(hc) for the predicate variable occurring on the left hand side of ⇐and pvsR(hc) for the set of predicate variables occurring in the right hand sideof ⇐. We write pvs(hc) for the set of predicate variables occurring in hc (i.e.,
pvs(hc) = {pvL(hc)} ∪ pvsR(hc)).
We define a Horn clause constraint set (HCCS) to be a pair (H, P⊥ ) where
H is a finite set of clauses and P⊥ is a predicate variable in H with ar(P⊥ ) =0 (intuitively, S
P⊥ is implicitly constrained by the S
clause ⊥ ⇐ P⊥ ()). We define fvs(H) = hc∈H fvs(hc). We
definepvs(H)=
hc∈H pvs(hc), pvsL(H) =S{pvL(hc) | hc ∈ H}, pvsR(H) = hc∈H pvsR(hc), roots(H) = pvsL(H)\pvsR(H),inters(H) = pvsL(H) ∩ pvsR(H), and leaves(H) = pvsR(H) \ pvsL(H). We saythat H is single-root if roots(H) is singleton, and write root(H) for P such that
{P } = roots(H).
Concrete and Abstract Solutions. A predicate substitution θ is a finite map
from predicate variables P to predicates of the form λ(x1 , . . . , xar(P ) ).φ such thatfvs(φ) ⊆ {x1 , . . . , xar(P ) }. Given an HCCS (H, P⊥ ), a predicate substitution θwith pvs(H) ⊆ dom(θ) is called a solution of H if |= θ(hc) for each hc ∈ H and|= ⊥ ⇐ θ(P⊥ )(). We write θ |= (H, P⊥ ) when θ is a solution of (H, P⊥ ).
We define abstract solution space that represents a possibly infinite set ofsolutions. To this end, we define formula template ψ to be a formula but withthe grammar extended to include terms of the form c · t where c is an unknown
coefficient variable. We define an abstract solution space S to be a pair (Θ, φ)
where Θ is a finite map from predicate variables P to predicate templates ofthe form λ(x1 , . . . , xar(P ) ).ψ and φ is a (non-template) QFLRA formula overunknowns. For S = (Θ, φ) and P ∈ dom(Θ), we write S(P ) for Θ(P ). We
say that a concrete solution θ is an instance of an abstract solution space (Θ, φ),written θ  (Θ, φ), if dom(θ) = dom(Θ) and there exists a map σ from unknowns
to rationals such that |= σ(φ) and for all P ∈ dom(θ), θ(P ) = σ(Θ(P )). We write
S ′  S if for all θ, θ  S ′ implies θ  S. We write S ′ P S if S ′  S and S ′ (P )contains no unknowns.
Horn Clause Constraint Kinds. The dependency relation ⊳H is defined to bet1 ) ⇐ a ∧ · · · ∧the relation that, for all P, Q ∈ pvs(H), Q ⊳H P if and only if Q(eP (et2 ) ∧ · · · ∧ φ ∈ H. We write ⊳∗H for the reflexive transitive closure of ⊳H and ⊳+H
for the transitive closure of ⊳H . We say that P is recursive if P ⊳+H P . We say that
P is head-joining (resp. body-joining) if P occurs more than once in the left (resp.
right) hand sides of clauses in H. We write recpvs(H), hjnpvs(H), and bjnpvs(H)respectively for the set of recursive, head-joining, and body-joining predicate
variables in H. We say that H is recursion-free if recpvs(H) = ∅, is body-disjoint
if bjnpvs(H) = ∅, and is head-disjoint if hjnpvs(H) = ∅.4 We say that H isconjunctive if for each hc ∈ H, the formula part of hc is a conjunction of literals.
We say that a single-root H is connected if for any P ∈ pvs(H), root(H) ⊳∗H P . We
extend the notions to HCCSs in the obvious way (e.g., (H, P⊥ ) is recursion-free
if H is recursion-free).
Any Horn clause set in this paper will be recursion-free. Therefore, in what
follows, we restrict ourselves to recursion-free Horn clause sets and HCCSs andomit the redundant qualifier “recursion-free”.
Example 1. Consider the HCCS (Hex 1 , P⊥ ) where Hex 1 is the set of clauses
below.
P (x, y, z) ⇐ x ≥ z ∧ y ≥ 2 − z
Q(x, y) ⇐ P (x, y, z) ∧ (z = 0 ∨ z = 1 ∨ z = 2)
P⊥ () ⇐ Q(x, y) ∧ Q(−x, −y)We have recpvs(Hex 1 ) = ∅, hjnpvs(Hex 1 ) = ∅, and bjnpvs(Hex 1 ) = {Q}, and so
the HCCS is recursion-free and head-disjoint but neither conjunctive nor bodydisjoint. (An equality t1 = t2 is t1 ≥ t2 ∧ t2 ≥ t1 .)A solution for the HCCS, θex 1 , and an abstract solution space for the HCCS,(Θex 1 , φex 1 ) are shown below. Note that θex 1  (Θex 1 , φex 1 ).
θex 1 (P ) = λ(x, y, z).x + y ≥ 2
θex 1 (Q) = λ(x, y).x + y ≥ 1
θex 1 (P⊥ ) = λ().⊥3

Θex 1 (P ) = λ(x, y, z).c0 + c1 · x + c2 · y ≥ 0
Θex 1 (Q) = λ(x, y).x + y ≥ 1
Θex 1 (P⊥ ) = λ().⊥φex 1 ≡ 0 < c1 = c2 ≤ −co ≤ 2 · c1

The Top-Level Procedure

Figure 1 shows the top-level procedure of the constraint solving algorithm Asolve
which takes as input an HCCS (H, P⊥ ) and returns its solution or detects that it
4

The terminologies are adopted from [14, 13].

is unsolvable. As remarked in Section 1, the algorithm looks for a simple solutionof the given HCCS by lazy sampling. Asolve initializes the sample set Samples to∅ (line 2), and repeats the loop (lines 3-12) until convergence. The loop first calls
the sub-algorithm Asamp on the HCCS (Samples, P⊥ ) to find an abstract space ofsolutions to the current sample set. If no solution is found for the samples, thenno solution exists for the whole constraint set (H, P⊥ ) either, and we exit theloop (line 5). Otherwise, an abstract solution space S for the samples is inferred,
and we pick a concrete instance θ of S (line 7) as the candidate solution. If θ
is a solution for the whole then we return it V
as the inferred solution (line 8).
a ∧ φ, that is unsatisfied and a
Otherwise, there is a clause in H, say P (et) ⇐ emodel σ in which the clause isVinvalid
with
θ.
From
the clause and σ, we obtainV
a ∧ C(φ, σ) as the new sample to be added tothe conjunctive clause P (et) ⇐ ethe sample set (line 12). Here, C(φ, σ) is the set of atoms representing the partof φ where σ holds true, and is defined as follows.
C(φ, σ) = {p | p occurs in φ and σ |= p} ∪ {¬p | p occurs in φ and σ |= ¬p}
Intuitively, the added sample clause represents a portion of the input HCCS thatis not yet covered by the solution found for the current sample set.
By construction, the sam- 01: A
solve ((H, P⊥ )) =ple HCCS (Samples, P⊥ ) is al- 02: Samples := ∅;ways conjunctive. The sub- 03: while true doalgorithm Asamp , whose de- 04: match Asamp ((Samples, P⊥ )) with
tails are deferred to Sec- 05:
NoSol → return NoSol| Sol(S) →tion 3.1, takes the conjunctive 06:
let θ  S in
HCCS (Samples, P⊥ ) and in- 07:
08:
if θ |= (H, P⊥ ) thenfers an abstract space of so09:
return Sol(θ)
lutions for it. Next, we show10:else
the correctness of Asolve , asV
a∧φ∈H
11:
let σ, P (et) ⇐ eVsuming that Asamp works corwhere σ 6|= θ( ea ∧ φ ⇒ P (et)) inrectly (i.e., it returns a non12:
Samples :=VV
empty abstract solution space
Samples ∪ {P (et) ⇐ ea ∧ C(φ, σ)}to the input conjunctive HCCS
if it is solvable and otherwise
Fig. 1. The Top-Level Procedure
returns NoSol). Let D(φ) ={C(φ, σ) | σ |= φ}. Let
by replacV (D(H), P⊥ ) be the conjunctive HCCS
V obtainedV
ing each clause a ⇐ e
a ∧ φ in H with the clauses {a ⇐ e
a ∧ C | C ∈ D(φ)}.
Note that, because D(φ) is finite, D(H) is also finite and (D(H),an HCCS.
W P⊥ ) is V
Also, the following can be shown from the fact that |= φ ⇔ C∈D(φ) C.

Lemma 1. θ is a solution of (H, P⊥ ) if and only if it is a solution of (D(H), P⊥ ).
We can also show that, in each loop iteration, the added sample is not in thecurrent sample set, and therefore the sample set grows monotonically as the loop
progresses, as stated in the following lemma.
V
Lemma 2. Suppose
θ(ea) ∧ φ, and σ 6|= θ(P )(et).
V θ |= (Samples, P⊥ ), σ |=Then, P (et) ⇐ ea ∧ C(φ, σ) ∈/ Samples.

From the lemmas, we show the correctness of Asolve , stated in the theorem below.
Theorem 1 (Correctness of Asolve ). Given an HCCS (H, P⊥ ), Asolve ((H, P⊥ ))returns a solution of (H, P⊥ ) if (H, P⊥ ) is solvable, and otherwise returns NoSol.
A reader may wonder why Asolve does not directly check if there exists asolution to the input HCCS from the entire abstract solution space S returned by
Asamp (i.e., check ∃θ  S.θ |= (H, P⊥ )) and infer new samples by using the entire
S if not. We opt against the approach because checking ∃θ  S.θ |= (H, P⊥ )requires an expensive non-linear constraint solving. Instead, we let Asolve choose
a concrete solution from S to be used as a candidate.5
Example 2. Consider running Asolve on the HCCS (Hex 1 , P⊥ ) from Example 1.
Suppose that at some iteration, Samples = {P (x, y, z) ⇐ x ≥ z ∧ y ≥ 2 −z, Q(x, y) ⇐ P (x, y, z)∧z = 0, P⊥ () ⇐ Q(x, y)∧Q(−x, −y)}, and Asamp returned
some abstract solution space S given (Samples, P⊥ ).
Let θ  S be the candidate solution chosen at line 7 where θ = {P 7→
λ(x, y, z).y ≥ 2 − z, Q 7→ λ(x, y).y ≥ 2, P⊥ 7→ λ().⊥}. Because θ 6|= (Hex 1 , P⊥ ),we obtain a new sample. A possible sample obtained here is Q(x, y) ⇐ P (x, y, z)∧z = 2. Adding the new sample to Samples, in the next loop iteration, as we shalldetail in Example 3, Asamp returns an abstract solution space containing thesolution θex 1 shown in Example 1.
N
3.1

The Sub-Algorithm Asamp

Asamp takes as input a
conjunctive HCCS, and re- 01: Asamp ((H, P⊥ )) =x.⊤ | P ∈ Q}, ⊤)turns a non-empty ab- 02: S := ({P⊥ 7→ λ().⊥} ∪ {P 7→ λewhere Q = roots(H) \ {P⊥ };stract space of its solutions if it is solvable and 03: WorkSet := initWS(H);04: while WorkSet 6= ∅ dootherwise returns NoSol.
05:
let H′ ∈ WorkSet S
As remarked before, Asamp
pvsR(H) in
where root(H′ ) ∈/looks for simple solutions 06: WorkSet := WorkSetH∈WorkSet\ {H′ };
that are likely to generalize 07: let S ′ root(H′ ) S in S := S ′ ;when given to the upper- 08: let C,LMap = MkCnsts(H′ , S, H) inprocedure Asolve to be used 09: for each (H′′ , P⊥′ ) ∈ C domatch Ahj ((H′′ , P⊥′ )) withas a candidate solution for 10:
11:
NoSol → return NoSol
the whole.
| Sol(S ′ ) →The internal workings 12:
S := combSol∧ (S ′ , S, LMap)of Asamp are quite intri- 13:
cate. The subtlety comes 14: return Sol(S)from body-joining prediFig. 2. The Sub-Algorithm Asampcate variables and headjoining predicate variables. Indeed, as we shall show in Section 3.3, inferring
5

Perhaps a somewhat subtle aspect of Asolve is that it is guaranteed to terminate andreturn a correct result despite only considering one concrete solution from the set ofsolutions returned by Asamp in each iteration.

a simple solution to a conjunctive body-and-head-disjoint HCCS is easy in thatsuch an HCCS has either no solution or a simple solution where each predicate
contains just one atom. Asamp decomposes the problem into easily solvable partsand combines their solutions to obtain a simple solution for the whole. The key
to the success is to do a coarse decomposition so that there are few subproblems
to be solved and the solutions to be combined, thereby resulting in a simple
solution for the whole sample set.
Figure 2 shows the overview of Asamp . Given the input conjunctive HCCS
(H, P⊥ ), we initialize the abstract solution space S to map P⊥ to λ().⊥ andthe other root predicate variables P ∈ roots(H) \ {P⊥ } to λ(x1 , . . . , xar(P ) ).⊤(line 2), and initialize the work set WorkSet to initWS(H) which is the coarsest
connected sets of clauses that partition H and are body-joined only at the roots
and the leaves (informally, initWS(H) partitions H into body-disjoint “trees”).
Formally, initWS(H) = {{hc ∈ H | P ◭∗(H,R\{P }) pvL(hc)} | P ∈ R} where R =(bjnpvs(H) ∩ pvsL(H)) ∪ roots(H), and Q ◭(H,R′ ) R if and only if Q ⊳H R andQ 6∈ R′ . As we show in the lemma below, initWS(H) is indeed the coarsest
connected partition of H that is body-joined only at the roots and the leaves.
S
Lemma 3. initWS(H) is the smallest set X that satisfies: 1. H =X, 2.
∀H1 , H2 ∈ X.H1 ∩ H2 = ∅, 3. ∀H′ ∈ X. H′ is connected, and 4. ∀H′ ∈X. bjnpvs(H) ∩ inters(H′ ) = ∅.
Then, we solve each element of WorkSet by calling Ahj , starting from theroot-most one that contains P⊥ , and recording the inferred solutions in S (lines 413). Ahj is a sub-algorithm that, given a conjunctive body-disjoint (but possibly
head-joined) HCCS, infers its solution if it is solvable and otherwise returns
NoSol. The detailed description of Ahj is deferred to Section 3.2.
To invoke Ahj on an element H′ ∈ WorkSet, Asamp first partially concretizes
the current abstract solution space S so that it maps root(H′ ) to a concrete
predicate (line 7), and then uses MkCnsts to convert H′ into the set of the
conjunctive body-disjoint HCCSs C (line 8). MkCnsts also returns LMap thatmaps the copied leaf predicate variables in C to the originals in H′ . Formally,′
MkCnsts(H′ , S, H) constructs C and LMap as follows. Let Hlcpy
be H′ witheach leaf predicate variable application P (et) replaced by Pcpy (et) for a fresh
predicate variable Pcpy . LMap is the map from the fresh predicate variable
Pcpy W
to the original P that it replaced. Let Prt = root(H′ ) and S(Prt ) =nλex.¬ i=1 φi where each φi is a conjunction of literals. Then, C is the set of′
HCCSs {(Hlcpy∪ Hlcsts ∪ {P⊥′ () ⇐ Prt (ex) ∧ φi }, P⊥′ ) | i ∈ {1, . . . , n}} where P⊥′
is a fresh predicate variable and Hlcsts is the set of clauses below.
{P (ex) ⇐ φi | P ∈ dom(LMap)Wmlsol(H, LMap(P )) = λex. i=1 φi where each φi is conjunction of literals}

Here, lsol(H, P ) is the predicate expressing the “lower-bound” solution of P thatis implied by H, and it is defined recursively as follows.
VmWVmti ) ∈ Hti ) | P (ex) ⇐ φ ∧ i=1 Ri (elsol(H, P ) = λex.
φ ∧ i=1 lsol(H, Ri )(eIntuitively, MkCnsts(H′ , S, H) substitutes the solution S(root(H′ )) for root(H′ )in H′ , adds the constraints required for the leaf predicate variables, and expands
the constraint so that the result is a set of conjunctive body-disjoint HCCSs.
The solution inferred for each constraint in C is combined and recorded in
the abstract solution space S (line 12). The solution combination operation
combSol∧ combines the abstract solutions by conjuncting the constraints overthe unknowns and conjuncting the predicate templates point-wise, using LMap
to conjunct the solutions for the copied leaf predicates into the original. Formally,
combSol∧ ((Θ, ψ), (Θ′ , ψ ′ ), LMap) = (combL(Θ, LMap) ∧ Θ′ , ψ ∧ ψ ′ ) wherecombL(Θ, LMap) = {P 7→ Θ(P/ ran(LMap)}
V )|P ∈∪{P 7→ LMap(P ′ )=P Θ(P ′ ) | P ∈ ran(LMap)}
We show the correctness of Asamp assuming that Ahj works correctly (i.e.,
it returns a non-empty abstract solution space to the input conjunctive bodydisjoint HCCS if it is solvable and otherwise returns NoSol).
Theorem 2 (Correctness of Asamp ). Given a conjunctive HCCS (H, P⊥ ),Asamp ((H, P⊥ )) returns a non-empty abstract solution space of (H, P⊥ ) if (H, P⊥ )is solvable, and otherwise it returns NoSol.
We note that it is possible to solve a conjunctive (or non-conjunctive) HCCS
more directly by expanding the HCCS to eliminate body-joining and headjoining predicate variables so that it is reduced to a tree-like form [11, 13, 14].
However, the approach makes exponentially many copies of predicate variables
whose solutions are conjuncted to form the solution of the original, which often results in complex solutions. Asamp avoids complicating the solution by only
making linearly many copies of predicate variables and only copying body-joining
predicate variables (assuming that simple solutions are inferred for the rootand body-joining predicate variables), and is therefore more likely to infer simple solutions for the whole.6 In Section 4, we compare our approach with theconstraint-expansion approach and show that our approach infers simpler solutions that aid the verification process.7
Also, in the implementation, we optimize the solution combination operation combSol∧ so that instead of always taking the conjunction of the inferredsolutions as described above, we eagerly apply constraint solving to reduce thenumber of atoms in the combined abstract solution space whenever possible(cf. Example 3).
Example 3. Let (Hex 2 , P⊥ ) be the HCCS (Samples, P⊥ ) given to Asamp in thelast iteration of Asolve in Example 2. S is initialized to ({P⊥ 7→ λ().⊥}, ⊤).
6

Our approach still exponentially expands the constraints, due to lsol(·). It only avoids(always) making exponentially many copies of the predicate variables.
7
The comparison is with Asolve for solving the whole HCCS and not with Asamp thatis just used to solve a sample set.

Because, bjnpvs(Hex 2 ) = {P, Q}, initWS(Hex 2 ) = {H1 , H2 , H3 } where
H1 = {P⊥ () ⇐ Q(x, y) ∧ Q(−x, −y)}H2 = {Q(x, y) ⇐ P (x, y, z) ∧ z = 0, Q(x, y) ⇐ P (x, y, z) ∧ z = 2}H3 = {P (x, y, z) ⇐ x ≥ z ∧ y ≥ 2 − z}
H1 is chosen as the first element to be solved from the workset, and we have
MkCnsts(H1 , S, H) = ({(Hex 3 , P⊥′ )}, LMap) where LMap = {Q1 7→ Q, Q2 7→ Q}
and Hex 3 is the set of clauses below.
{Qi (x, y) ⇐ x ≥ 0 ∧ y ≥ 2, Qi (x, y) ⇐ x ≥ 2 ∧ y ≥ 0 | i = 1, 2}∪{P⊥ () ⇐ Q1 (x, y) ∧ Q2 (−x, −y), P⊥′ ⇐ P⊥ () ∧ ¬⊥}Asamp then applies Ahj to (Hex 3 , P⊥′ ) and obtains an abstract solution space
S1 = (Θex 3 , φex 3 ) (see Example 4 for details) where{Qi 7→ λ(x, y).ci,0 + ci,1 · x + ci,2 · y ≥ 0 | i = 1, 2}∪{P⊥ 7→ λ().⊥, P⊥′ 7→ λ().⊥}
c + c2,0 < 0 ∧ c1,1 = c2,1 ≥ 0 ∧ c1,2 = c2,2 ≥ 0∧
φex 3 ≡ V1,0
i=1,2 (ci,0 ≥ −2 · ci,2 ∧ ci,0 ≥ −2 · ci,1 )Θex 3 =

Asamp then combines the solution space to update S to combSol∧ (S1 , S, LMap) =({P⊥ 7→ λ().⊥, Q 7→ λ(x, y).c1,0 + c1,1 · x + c1,2 · y ≥ 0 ∧ c2,0 + c2,1 · x + c2,2 · y ≥0}, φex 3 ). In the implementation, we eagerly apply constraint solving to reduce
the number of atoms in the combined solution space. In this example, we check if
σuni (φex 3 ) is satisfiable where σuni = {c2,i 7→ c1,i | i = 0, 1, 2}, and if so updates
S to ({P⊥ 7→ λ().⊥, Q 7→ λ(x, y).c1,0 + c1,1 · x + c1,2 · y ≥ 0}, σuni (φex 3 )) instead.
Here, σuni (φex 3 ) = c1,0 < 0 ∧ c1,1 ≥ 0 ∧ c1,2 ≥ 0 ∧ c1,0 ≥ −2 · c1,2 ∧ c1,0 ≥ −2 · c1,1
which is satisfiable.
Next, Asamp chooses H2 to solve. It updates the space S so that S(Q) is
concrete. For example, S(Q) = λ(x, y).x + y ≥ 1. Then, it solves H2 and updates
S by proceeding similarly to the case for H1 . Lastly, H3 is solved, and Asamp
returns the solution space (θex 1 , ⊤) from Example 1.
N
3.2

The Sub-Algorithm Ahj

Ahj takes as input a conjunctive body-disjoint (but possibly head-joined) HCCS.
To infer simple solutions to the given HCCS, Ahj first checks if the given HCCS
has a solution in the simplest space that maps each predicate variable to a predicate consisting of a single atom, that we call an atomic solution, and decomposing
the HCCS into smaller subparts containing less head-joining predicate variables
if no atomic solution is found. Ahj calls itself recursively to do the decomposition
until a solution is found, and the solution spaces of the decomposed subparts are
combined to form the solution space for the whole. The key observation here isthat, as we shall show in Lemma 4, a conjunctive body-disjoint HCCS with nohead-joining predicate variable (i.e., is head-disjoint) is guaranteed to either has
an atomic solution or no solution at all. Therefore, the decomposition process isguaranteed to converge to either find a solution or detect that the input HCCS
is unsolvable.

Figure 3 shows the 01: Ahj ((H, P⊥ )) =overview of Ahj . Ahj first 02: match Aatom ((H, P⊥ )) withcalls Aatom , whose de- 03:
Sol(S) → return Sol(S)| NoSol →tails are deferred to Sec- 04:
if hjnpvs(H) = ∅ thention 3.3, to check if there 05:
return NoSol
exists an atomic solution 06:
07:
else
to the given HCCS. If so,let H1 , H2 = Decomp(H) in
then it returns the in- 08:
09:
match Ahj ((H1 , P⊥ )), Ahj ((H2 , P⊥ )) withferred space of atomic so10:
NoSol, | , NoSol → return NoSol
lutions (line 3). Other- 11:| Sol(S1 ), Sol(S2 ) → Sol(combSol∨ (S1 , S2 ))wise, it checks if the given
HCCS is head-disjoint. If
Fig. 3. The Sub-Algorithm Ahj
so, then there can be no
solution to the given HCCS, and we return NoSol (line 6). Otherwise, we picka head-joining predicate variable, say P , and decompose the H into H1 and H2such that H1 and H2 split the clauses in H whose head is P (along with their“subtree” clauses). (The details of the decomposition is quite intricate and deferred to later in the section.) Then, we call Ahj recursively to infer the solutions
for the subparts H1 and H2 . If either part is found to be unsolvable, then we
return NoSol (line 10). Otherwise, we combine the returned solution spaces forthe subparts to obtain the solution space for the whole (line 11). The combination operation combSol∨ is analogous to combSol∧ used in Asamp except that wetake a point-wise disjunction of the solutions as opposed to taking a conjunction (and that there is no management of the copied leaf predicate variables).
More formally, combSol∨ ((Θ, ψ), (Θ′ , ψ ′ )) = (Θ ∨ Θ′ , ψ ∧ ψ ′ ) where Θ ∨ Θ′ is thepoint-wise disjunction of Θ and Θ′ . As with combSol∧ , in the implementation, weeagerly apply constraint solving to reduce the number of atoms in the combined
solution space instead of always taking the disjunction.
We describe the details of the decomposition operation Decomp. As remarked
above, the role of Decomp is to decompose the input HCCS into parts that
contain fewer clauses that are head-joined. This is done by selecting some headjoining predicate variable and making two copies of the original that split the
portion of the subtrees reachable from the selected predicate variable. Moreformally, given a non-head-disjoint H, Decomp(H) returns (H1 , H2 ) as follows.
We pick some head-joining predicate variable P ∈ hjnpvs(H). Let HP be the setof clauses in H having P as the head. We partition HP into non-empty disjoint
subsets H1′ and H2′ . For each Hi′ (i ∈ {1, 2}), let Hi′′ be the set of clauses in H
whose head is Q where R ⊳∗H Q for some predicate variable R that appears inthe body of a clause in Hi′ . Then, we set Hi = H \ (Hi′ ∪ Hi′′ ).
We show the correctness of Ahj , assuming that the sub-algorithm Aatom
works correctly. As we show in Section 3.3, Aatom checks if there exists an atomic
solution to the conjunctive body-disjoint (but possibly head-joined) HCCS given
as the input, and it is guaranteed to return a non-empty abstract solution space
if the given HCCS is solvable and head-disjoint. Then, the following theorem
follows from the property of Decomp and combSol∨ and the fact that the recursive

decompositions may happen only as many times as the number of head-joined
clauses in the input HCCS.
Theorem 3 (Correctness of Ahj ). Given a conjunctive body-disjoint HCCS
(H, P⊥ ), Ahj ((H, P⊥ )) returns a non-empty abstract solution space of (H, P⊥ )if (H, P⊥ ) is solvable, and otherwise it returns NoSol.
The above description of Decomp leaves freedom on how to actually do thedecomposition, that is, which head-joining predicate variable to select and how
to split the subtrees reachable from the selected predicate variable. While Theorem 3 holds true regardless of how the decomposition is done, choosing a coarse
decomposition is important for inferring a simple solution. To this end, in theimplementation described in Section 4, we choose the decomposition by analyzing the reason for Aatom ’s failure on finding an atomic solution (cf. line 2) whichis returned as an unsatisfiable core of the constraints that Aatom attempted tosolve. In addition, instead of doing the recursive decompositions independently
for the parts H1 and H2 as in Figure 3, we synchronize the decompositions in
the recursive call branches to minimize the unnecessary decompositions.8
Example 4. Recall (Hex 3 , P⊥′ ) from Example 3. (Hex 3 , P⊥′ ) has an atomic solution, and therefore, the first call to Aatom by Ahj (line 3) immediately succeeds
and returns an abstract solution space. Here, the returned abstraction solution
space is (Hex 3 , P⊥′ ) from Example 3 (see Example 5 for details).
3.3

The Sub-Algorithm Aatom

As remarked in Section 3.2, Aatom decides if there exists an atomic solution to
the given conjunctive body-disjoint HCCS, and returns a non-empty abstract
solution space of atomic solutions if so. Given the input HCCS (H, P⊥ ), Aatom
prepares the atomic solution template ΘH that maps each predicate variablear(P )P ∈ pvs(H) to the formula template of the form λ(x1 , . . . , xar(P ) ).c0 + Σi=1 ci ·9xi ≥ 0 where ci ’s are fresh unknowns.
Then, it generates the constraint φH =V
constr(ΘH , (H, P⊥ )) = c < 0 ∧ hc∈H constr(ΘH , hc) where ΘH (P⊥ ) = λ().c ≥ 0VℓVqand constr(ΘH , hc) is defined as follows; for hc = a0 ⇐ i=1 ai ∧ i=1 pi withfvs(hc) = {x1 , . . . , xm },
Vq
Vm
Pℓ
Pq
constr(ΘH , hc) = i=1 αi ≥ 0 ∧ j=0 t0,j = ( i=1 ti,j ) + ( i=1 αi · ri,j )where
Pm α1 , . . . , αq are fresh unknowns, and ΘH (ai ) andPmpi are respectively ti,0 +
t
·
x
≥
0
(for
i
∈
{0,
.
.
.
,
ℓ})
and
r
+
j
i,0
j=1 i,j
j=1 ri,j · xj ≥ 0 (for i ∈{1, . . . , q}) for some linear terms over unknowns ti,j and rational constants ri,j .
Note that φH is a QFLRA formula over unknowns (i.e., it contains no variableor product of unknowns).
89Decomp is similar in spirit to the sample set “split” operation from [1].
For simplicity, in this section, we only consider non-strict inequality atoms. Strict
inequalities can be handled similarly by using the Motzkin’s transposition theorem
instead of the Farkas’ lemma (cf. Appendix A).

Then, Aatom checks if φH is satisfiable, that is, if there exists an assignment σ
to the unknowns such that |= σ(φH ), and if so, returns (ΘH , φH ) as the abstract
solution space. Otherwise, it detects that (H, P⊥ ) has no atomic solution andreturns NoSol. We state and prove the correctness of Aatom .
Theorem 4 (Correctness of Aatom ). Given a conjunctive body-disjoint HCCS
(H, P⊥ ), Aatom ((H, P⊥ )) returns a non-empty abstract atomic solution space Sof (H, P⊥ ) if (H, P⊥ ) has an atomic solution, and otherwise returns NoSol.
Also, the following holds by the Farkas’ lemma [16].
Lemma 4. A conjunctive body-disjoint and head-disjoint HCCS either has an
atomic solution or no solution.
Therefore, Aatom completely decides the solvability of a conjunctive body-disjoint
head-disjoint HCCS. In general, a solvable conjunctive body-disjoint (but nothead-disjoint) HCCS may not be atomically solvable. For example, (H, P⊥ )where H = {P (x, y) ⇐ x ≤ 0 ∧ y ≤ 1, P (x, y) ⇐ x ≤ 1 ∧ y ≤ 0, P⊥ () ⇐ P (x, y) ∧x > 0 ∧ y > 0} is solvable but has no atomic solution. Thus, when Aatom fails
to find an atomic solution to such an HCCS, the information is propagated backto Ahj to decompose some head-joined clauses.
Example 5. Consider the HCCS (Hex 3 , P⊥′ ) from Example 3 (note that it ishead-disjoint). Aatom prepares the atomic solution template ΘHex 3 = {Qi 7→
λ(x, y).ci,0 + ci,1 · x + ci,2 · y ≥ 0 | i = 1, 2} ∪ {P⊥ 7→ λ().c3,0 ≥ 0, P⊥′ 7→ λ().c4,0 ≥0} and generates the constraint constr(ΘHex 3 , (Hex 3 , P⊥′ )):c4,0 < 0 ∧ α1 , α2 ≥ 0 ∧ c4,0 = c3,0 + α1 ∧ c3,0 = c1,0 + c2,0 + α2 ∧0 = c1,1− c2,1 ∧ 0 = c1,2 − c2,2 ∧V
αi,1 , αi,2 , αi,3 ≥ 0 ∧ ci,0 = −2 · αi,2 + αi,3 ∧ ci,1 = αi,1 ∧ ci,2 = αi,2 ∧
i=1,2
αi,4 , αi,5 , αi,6 ≥ 0 ∧ ci,0 = −2 · αi,4 + αi,6 ∧ ci,1 = αi,4 ∧ ci,2 = αi,5In the constraint generation, we add the tautology 1 ≥ 0 to the body of eachclause. This often widens the obtained solution space. After satisfiability checking
and simplification, Aatom returns the abstract solution space (Θex 3 , φex 3 ) given
in Example 3.
N

4

Implementation and Experiments

We have implemented a prototype of the new constraint solving algorithm Asolve .
We use the linear programming tool GLPK (http://www.gnu.org/software/glpk) for the linear constraint solving that is used to operate on abstract solution
spaces, and Z3 (http://z3.codeplex.com) for the unsat core generation in Ahj
and for checking the candidate solution against the whole HCCS in Asolve . We
use the objective function in linear programming to find a model with small
valuations to further bias towards simple solutions.
We use the constraint solver as the backend of the MoCHi software model
checker [9]. MoCHi verifies assertion safety of OCaml programs via predicate abstraction, higher-order model checking, and CEGAR. MoCHi is a good platform

100

10

10

1

1

Aiter

Aexpand

100

0.1

0.01

0.1

0.01

0.001
0.001

0.01

0.1

1

10

100

0.001
0.001

0.01

Asolve1

10100Asolve
4096

512

512

Aexpand

4096

Aiter

0.1

64

64

8

8

1

1
1

8

64

Asolve

512

4096

1

8

64

512

4096

AsolveFig. 4. Run time (upper) and solution size (lower) comparisons of the HCCS solving
algorithms on benchmarks HCCSs

for experimenting with the constraint solver because the Horn-clause constraints
solved there often have a complex structure. (Intuitively, this is because the constraints express the flow of data in the program to be verified, and data often
flow in a complex way in a functional program, e.g., passed to and returned fromrecursive functions, captured in closures, etc.)
We compare the new algorithm Asolve with two other algorithms, Aiterand Aexpand . Aiter is an implementation of the iterative approach to solving
HCCS [20, 18], and is also used in the previous work on MoCHi [9, 15, 22, 10].
Aexpand is an implementation of the constraint-expansion approach [4, 14] inwhich the given HCCS is first expanded into a body-disjoint head-disjoint HCCS
and the iterative algorithm is used to solve the resulting HCCS. (See also Related Work in Section 1.)
We have ran the three algorithms on 327 HCCSs generated by running
MoCHi with Asolve on 139 benchmark programs, most of which are taken fromthe previous work on MoCHi [9, 15, 22, 10]. We measured the time spent on solving each HCCS by each algorithm as well as the size of the inferred solution(the sum of the syntactic sizes of the predicates). We also compare the overall

100

10

10

1

1

Aiter

Aexpand

100

0.1

0.01

0.1

0.01

0.001
0.001

0.01

0.1

Asolve

1

10

100

0.001
0.001

0.01

0.1

1

10

100

AsolveFig. 5. Run time comparison of the HCCS solving algorithms on benchmarks programs

verification speed of MoCHi when using the three algorithms on the 139 benchmark programs. The experiments were conducted on a machine with 2.69 GHz
i7-4600U processor with 16 GB of RAM, with the time limit of 100 seconds.
The benchmark programs, the benchmark HCCSs and the experiment results
are available online [21].
Figure 4 shows the scatter plots that compare the run times and the solution
sizes of Asolve , Aiter , and Aexpand on each of the 318 benchmark HCCSs. The runtime plots show that, on most instances, Asolve is slower than Aiter and Aexpand
due to the additional effort to find a simple solution. The plots also show that
Asolve is sometimes faster than the other two. The behavior is attributed to thefact that Asolve is sometimes able to find a solution for the whole by samplinga very small fraction of the given HCCS, and the fact that Aiter and Aexpand(after the expansion) uses the iterative approach which can be sometimes slow
on large instances. The solution size plots show that Asolve is able to computesmaller solutions than the other two on most instances.
Figure 5 shows the plots comparing the run times of the overall verification
process on each of the 139 benchmark programs for each constraint solving
algorithm. The plots show that, with the new algorithm Asolve , MoCHi is able toverify significantly more programs within the time limit than with the other twoalgorithms. The plots also show that the heavier cost of constraint solving in the
new algorithm is often compensated by the better predicates inferred, thereby
allowing the overall verification speed to match those of the other algorithms
even on instances that the other algorithms were able to verify in time.

5

Conclusion

We have presented a new approach to solving recursion-free Horn-clause constraints. Our approach is inspired by the sampling-based approach to inferring
simple interpolants [17, 1] and is geared toward inferring simple solutions. Wehave shown that the new approach is effective at inferring simple solutions thatare useful to program verification.

References
1. A. Albarghouthi and K. L. McMillan. Beautiful interpolants. In CAV, pages
313–329, 2013.
2. N. Bjørner, K. L. McMillan, and A. Rybalchenko. On solving universally quantified
horn clauses. In SAS, pages 105–125, 2013.
3. W. Craig. Linear reasoning. a new form of the herbrand-gentzen theorem. The
Journal of Symbolic Logic, 22(03):250–268, 1957.
4. S. Grebenshchikov, N. P. Lopes, C. Popeea, and A. Rybalchenko. Synthesizing
software verifiers from proof rules. In PLDI, pages 405–416, 2012.
5. A. Gupta, C. Popeea, and A. Rybalchenko. Predicate abstraction and refinement
for verifying multi-threaded programs. In POPL, pages 331–344, 2011.
6. A. Gupta, C. Popeea, and A. Rybalchenko. Solving recursion-free horn clauses
over LI+UIF. In APLAS, pages 188–203, 2011.
7. T. A. Henzinger, R. Jhala, R. Majumdar, and K. L. McMillan. Abstractions fromproofs. In POPL, pages 232–244, 2004.
8. K. Hoder, L. Kovács, and A. Voronkov. Playing in the grey area of proofs. In
POPL, pages 259–272, 2012.
9. N. Kobayashi, R. Sato, and H. Unno. Predicate abstraction and CEGAR for
higher-order model checking. In PLDI, pages 222–233. ACM, 2011.
10. T. Kuwahara, T. Terauchi, H. Unno, and N. Kobayashi. Automatic termination
verification for higher-order functional programs. In ESOP, pages 392–411, 2014.
11. K. McMillan and A. Rybalchenko. Computing relational fixed points using interpolation. Technical Report MSR-TR-2013-6, January 2013.
12. K. L. McMillan. Lazy abstraction with interpolants. In CAV, pages 123–136, 2006.
13. P. Rümmer, H. Hojjat, and V. Kuncak. Classifying and solving horn clauses forverification. In VSTTE, pages 1–21, 2013.
14. P. Rümmer, H. Hojjat, and V. Kuncak. Disjunctive interpolants for horn-clauseverification. In CAV, pages 347–363, 2013.
15. R. Sato, H. Unno, and N. Kobayashi. Towards a scalable software model checker
for higher-order programs. In PEPM, pages 53–62. ACM, 2013.
16. A. Schrijver. Theory of linear and integer programming. Wiley, 1998.
17. R. Sharma, A. V. Nori, and A. Aiken. Interpolants as classifiers. In CAV, pages
71–87, 2012.
18. T. Terauchi. Dependent types from counterexamples. In POPL, pages 119–130,
2010.
19. T. Terauchi and H. Unno. Relaxed stratification: A new approach to practicalcomplete predicate refinement. In ESOP, 2015. To appear.
20. H. Unno and N. Kobayashi. Dependent type inference with interpolants. In PPDP,
pages 277–288, 2009.
21. H. Unno and T. Terauchi. Inferring simple solutions to recursion-free horn clauses
via sampling. 2015. http://www.cs.tsukuba.ac.jp/~uhiro.
22. H. Unno, T. Terauchi, and N. Kobayashi. Automating relatively complete verification of higher-order functional programs. In POPL, pages 75–86, 2013.

A

Extending Aatom to support strict inequalities

For convenience, we extend the grammar of QFLRA formulas with formulas of
the form ite(φ0 , φ1 , φ2 ), which is used as a shorthand for (φ0 ⇒ φ1 )∧(¬φ0 ⇒ φ2 ).
Let (H, P⊥ ) be the HCCS given as the input to Aatom . For each P ∈ pvs(H),we prepare a fresh unknown cst
P . We prepare the solution template ΘH so thatfor each P ∈ pvs(H)ΘH (P ) = λ(x1 , . . . , xar(P ) ).ite(cstP = 1, φstrict , φnonstrict )ar(P )

ar(P )

where φstrict = c0 + Σi=1 ci · xi > 0, φnonstrict = c0 + Σi=1 ci · xi ≥ 0, and ci ’s
are fresh unknowns.
Then, we generate the constraint φH below.
^
φH = ite(cstconstr(ΘH , hc)
P⊥ = 1, c ≤ 0, c < 0) ∧hc∈HVℓHere, ΘH (P⊥ ) = λ().ite(cstP⊥ = 1, c > 0, c ≥ 0). And, for hc = a0 ⇐ i=1 ai ∧
′
Vq
Vq
′
′
i=1 pi where fvs(hc) = {x1 , . . . , xm } and each pi (resp. pi ) a noni=1 pi ∧strict (resp. strict) inequality, constr(ΘH , hc) is defined to be the formulaVqVq′βi ≥ 0∧i=1 αi ≥ 0 ∧VmPℓ i=1
Pq
Pq ′
′
t
=
(
t
i=1 βi · ri,j )∧j=0 0,ji=1 i,j ) + (i=1 αi · ri,j ) + (
′
V
Vℓ
q
st
st
ite( i=1 cst
Pi = 0 ∧i=1 βi = 0, cP0 = 0, cP0 = 1)′,
where, for some linear terms over unknowns ti,j and rational constants ri,j , ri,j

– α1 , . . . , αq , β1 , . . . , βq′ are fresh unknowns;– ai is of the Pform Pi ( ) (for i ∈ {0, . . . , ℓ});m
– pi = ri,0 + j=1 ri,j · xj ≥ 0 (for i ∈ {1, . . . , q});Pm ′′′– pi = ri,0 + j=1 ri,j · xj ≥ 0 (for i ∈ {1, . . . , q ′ }); andPm
Pm– ΘH (ai ) = ite(cst
Pi = 1, ti,0 +j=1 ti,j · xj > 0, ti,0 +j=1 ti,j · xj ≥ 0) (fori ∈ {0, . . . , ℓ}).
Note that φH is a QFLRA formula over unknowns (i.e., it contains no variableor multiplication of an unknown with an unknown).
Then, Aatom checks if φH is satisfiable, and if so returns (ΘH , φH ) as theabstract solution space, and otherwise returns NoSol. The correctness of theextended algorithm follows from the Motzkin’s transposition theorem [16].

B

ProofsB.1

Proof of Theorem 1

We first show Lemmas 1 and 2, from which Theorem 1 follows immediately.

Lemma 1 θ is a solution of (H, P⊥ ) if and only if it is a solution of (D(H), P⊥ ).
V
V
⇐ e
a∧
Proof. Because θ is a solution
V of ({aW
V C | C ∈ D(φ)}, P⊥ ) if and onlya ∧ C∈D(φ) C}, P⊥ ), it suffices to show that
if it is an solution of ({a ⇐ e
WV|= φ ⇔ C∈D(φ) C.
V(⇒) Suppose that σ |= φ. By the definition
W of C(φ,Vσ), we have σ |= C(φ, σ).
Because C(φ, σ) ∈ D(φ), we get σ |= C∈D(φ) C.
V(⇐) Is suffices to show that for all σ1 , σ2 , if σ1 |= φ and σ2 |=C(φ, σ1 ),
then
σ
|=
φ.
We
prove
this
by
contradiction.
Suppose
σ
|=
φ
and
σ2 |=
2
1
V
C(φ, σ1 ) but σ2 6|= φ. Then, there must exist some p that occurs in φ suchthat either (a) σ1 |= p and σ2 |= ¬p, or (b) σ1 |= ¬p and σ2 |= Vp holds. In
the former case (a), we have p ∈ C(φ, σ1 ), which implies σ2 6|= C(φ, σ1 ).
Thus we have a contradiction. The latter case (b) is similar.
⊓⊔
V
Lemma 2 V
Suppose θ |= (Samples, P⊥ ), σ |= θ(ea)∧φ, and σ 6|= θ(P )(et). Then,P (et) ⇐ ea ∧ C(φ, σ) ∈/ Samples.
V
Proof. We prove thisVby contradiction.
Suppose that P (et) ⇐ ea ∧ C(φ, σ) ∈V′′eSamples.
Then, σ ′ |= θ(eVVa) ∧ C(φ, σ) implies σ |= θ(P )(t)Vfor all σV. By σ |=θ(ea) ∧ φ, we have σ |= θ(ea) and σ |= φ. We then get σ |= θ(ea) ∧ C(φ, σ).
Therefore, we obtain σ |= θ(P )(et). Thus, we get a contradiction.
⊓⊔
From the lemmas, we now prove the correctness of Asolve .

Theorem 1 (Correctness of Asolve ) Given an HCCS (H, P⊥ ), Asolve ((H, P⊥ ))returns a solution of (H, P⊥ ) if (H, P⊥ ) is solvable, and otherwise it returns
NoSol.
Proof. Samples ⊆ D(H) is an invariant of Asolve . By the correctness of Asamp(see Theorem 2), Asolve returns NoSol (line 5) if (H, P⊥ ) has no solution, andotherwise it returns Sol(θ) (line 9)Vsuch that θ |= (H, P⊥ ). In the line
V 11, therea ∧ φ ∈ H such that σ 6|= θ( ea∧φ ⇒always exist some σ and P (et) ⇐ eP (et)) because in the else branch (lines 10-12), Samples 6= D(H) follows from
Lemma 1. Therefore, by Lemma 2, Samples grows monotonically (line 12) as theloop progresses. Because Samples ⊆ D(H) is an invariant and D(H) is a finite
set, the loop eventually terminates.
⊓⊔
B.2

Proof of Theorem 2

We first prove Lemma 3.
S
Lemma 3 initWS(H) is the smallest set X that satisfies: 1. H =X, 2.
∀H1 , H2 ∈ X.H1 ∩ H2 = ∅, 3. ∀H′ ∈ X. H′ is connected, and 4. ∀H′ ∈X. bjnpvs(H) ∩ inters(H′ ) = ∅.
Proof. For all X and R, the following two conditions are equivalent:1. X = {{hc ∈ H | P ◭∗(H,R\{P }) pvL(hc)} | P ∈ R}, and roots(H) ⊆ R.
2. X satisfies the conditions 1–3, and ∀H′ ∈ X.R ∩ inters(H′ ) = ∅, R ={root(H) | H ∈ X}, and ∀H1 , H2 ∈ X.root(H1 ) = root(H2 ) ⇒ H1 = H2 .
Recall that initWS(H) = {{hc ∈ H | P ◭∗(H,R0 \{P }) pvL(hc)} | P ∈ R0 }, whereR0 = (bjnpvs(H)∩pvsL(H))∪roots(H). Because roots(H) ⊆ R0 and (bjnpvs(H)∩pvsL(H)) ⊆ R0 , we get– initWS(H) satisfies all the conditions 1–4,
– R0 = {root(H) | H ∈ initWS(H)}, and– ∀H1 , H2 ∈ initWS(H).root(H1 ) = root(H2 ) ⇒ H1 = H2 .
We now prove the minimality of X. Let Y be a set that satisfies the conditions
1–4. Then, (bjnpvs(H) ∩ pvsL(H)) ⊆ {root(H) | H ∈ Y } and there exists Y ′ suchthat
– {root(H) | H ∈ Y ′ } ⊆ {root(H) | H ∈ Y },– ∀H′ ∈ Y ′ .{root(H) | H ∈ Y ′ } ∩ inters(H′ ) = ∅, and– ∀H1 , H2 ∈ Y ′ .root(H1 ) = root(H2 ) ⇒ H1 = H2 .
In fact, such a Y ′ can be constructed from Y by moving clauses that arereachable from P ∈ {root(H) | H ∈ Y } ∩ inters(Hsrc ) for some Hsrc ∈ Y to
Hdst ∈ Y with root(Hdst ) = P . We then get (bjnpvs(H) ∩ pvsL(H)) ∪ roots(H) ⊆{root(H) | H ∈ Y ′ }. Therefore,{root(H) | H ∈ initWS(H)} = R0 ⊆ {root(H) | H ∈ Y }Thus, we get |initWS(H)| = |{root(H) | H ∈ initWS(H)}| ≤ |Y |.

⊓⊔Theorem 2 (Correctness of Asamp ) Given a conjunctive HCCS (H, P⊥ ),Asamp ((H, P⊥ )) returns a non-empty abstract solution space of (H, P⊥ ) if (H, P⊥ )is solvable, and otherwise it returns NoSol.
Proof. This follows from the correctness of Ahj (see Theorem 2), Lemma 3, andthe definitions of MkCnsts and combSol∧ . Note that Ahj is terminating because
the size of WorkSet strictly decreases as the loop iterates.
⊓⊔
B.3

Proof of Theorem 3

Lemma 5. Let H0 , H1 = Decomp(H) and S0 (resp. S1 ) be a non-empty solution
space of H0 (resp. H1 ). Then, combSol∨ (S0 , S1 ) is a non-empty solution spaceof H.
Proof. This follows from the definitions of Decomp(H) and combSol∨ (S0 , S1 ).
⊓⊔Theorem 3 (Correctness of Ahj ) Given a conjunctive body-disjoint HCCS
(H, P⊥ ), Ahj ((H, P⊥ )) returns a non-empty abstract solution space of (H, P⊥ )if (H, P⊥ ) is solvable, and otherwise it returns NoSol.

Proof. We prove the theorem by induction on the number of head-joined clausesof H, written hjcs(H).
Case hjcs(H) = 0
In this case, H is also head-disjoint, and by the correctness of Aatom (seeLemma 4), Ahj returns a non-empty abstract solution space of (H, P⊥ ) (line6) if (H, P⊥ ) is solvable, and otherwise it returns NoSol (line 3).
Case hjcs(H) = k:
By the correctness of Aatom (see Theorem 4), Ahj returns a non-empty abstract solution space of (H, P⊥ ) (line 3) if (H, P⊥ ) has an atomic solution.
Otherwise, Ahj decomposes H into H1 ⊆ H and H2 ⊆ H. By the definitionof Decomp(H), we get hjcs(H1 ) < k and hjcs(H2 ) < k. Suppose that either
Ahj ((H0 , P⊥ )) or Ahj ((H1 , P⊥ )) returns NoSol (line 10). Then, by induction
hypothesis, either (H0 , P⊥ ) or (H1 , P⊥ ) has no solution. This implies that
(H, P⊥ ) has no solution. Ahj ((H, P⊥ )) then correctly returns NoSol (line10). Otherwise, Ahj ((H, P⊥ )) returns combSol∨ (S0 , S1 ) (line 11). Therefore,
the result follows from Lemma 5 and induction hypothesis,⊓⊔
B.4

Proof of Theorem 4

Theorem 4 (Correctness of Aatom ) Given a conjunctive body-disjoint HCCS
(H, P⊥ ), Aatom ((H, P⊥ )) returns a non-empty abstract atomic solution space Sof (H, P⊥ ) if (H, P⊥ ) has an atomic solution, and otherwise returns NoSol.
Proof. It is immediate from the definition of Aatom that if Aatom ((H, P⊥ )) returns an abstract solution space S then S only contains atomic solutions of(H, P⊥ ). Therefore, it suffices to show that if (H, P⊥ ) has an atomic solution
then Aatom ((H, P⊥ )) returns a non-empty
abstract solution space.
V
Let us write constr(ΘH , H) for hc∈H constr(ΘH , hc). Then, the constraint
φH that Aatom ((H, P⊥ )) generates can be written c < 0 ∧ constr(ΘH , H) whereΘH (P⊥ ) = λ().c ≥ 0.
V
We define the Farkas constraint constrF (ΘH , H) to be hc∈H constrF (ΘH , hc)
VℓVqwhere constrF (ΘH , hc) is defined as follows. For hc = a0 ⇐ i=1 ai ∧ i=1 pi withfvs(hc) = {x1 , . . . , xm }, we define
constrF (ΘH , hc) =
Pq
Pℓ
Vm
Vq
Vℓ
i=1 αi · ri,j )i=1 βi · ti,j ) + (j=0 t0,j = (i=1 αi ≥ 0 ∧i=1 βi ≥ 0 ∧where α1 , . . . , αqPand β1 , . . . , βℓ are fresh unknowns, and ΘH (aPi ) and pi are remmspectively ti,0 + j=1 ti,j · xj ≥ 0 (for i ∈ {0, . . . , ℓ}) and ri,0 + j=1 ri,j · xj ≥ 0(for i ∈ {1, . . . , q}) for some linear terms over unknowns ti,j and rational constants ri,j . Note that constrF (ΘH , hc) is constr(ΘH , hc) but with the additional(non-linear) factors βi ’s.
For a satisfying assignment σ of constr(ΘH , H) (i.e., σ |= constr(ΘH , H)), wewrite sol(σ) for the map θ such that θ(P ) = σ(ΘH (P )) for all P ∈ pvs(H). Thatis, sol(σ) is the “solution” of H determined by σ disregarding the implicit goal

clause ⊥ ⇐ P⊥ . We define sol(σ) analogously when σ is a satisfying assignmentof constrF (ΘH , H).
The Farkas’ lemma [16] implies that for any atomic solution θ of H (disregarding the implicit goal clause) there exists σ satisfying constrF (ΘH , H) suchthat sol(σ) = θ. Because the goal clause only constrains the solution of the root
predicate variable, it suffices to show the following lemma to prove the theorem.
Lemma 6. Suppose σ |= constrF (ΘH , H) and r ≥ 0. Then, there exists σ ′ suchthat σ ′ |= constr(ΘH , H) and sol(σ ′ )(root(H)) = r · sol(σ)(root(H)).
(The extra factor r is needed for the inductive case.) We prove the lemma by
induction on the depth of H, written depth(H), which is defined to be the longest⊳H path. For convenience, we write subhcsH (P ) for the subset of H reachable
from P , that is, subhcsH (P ) = {hc ∈ H | P ⊳∗H pvL(hc)}. We overload subhcsH
to predicate variable applications so that subhcsH (P ( )) = subhcsH (P ).
Case depth(H) = 0
In this case, constrF (ΘH , H) = constr(ΘH , H). Therefore, it suffices to choose
σ ′ such that σ ′ (c) = r ·σ(c) for the unknowns c appearing in constrF (ΘH , H).
Case depth(H) = k:
Let {hc 1 , . . . , hc n } = {hc ∈ H | pvL(hc) = root(H)}. For each i ∈ {1, . . . , n},Vqi
V ℓipi,j . Then, for each i ∈ {0, . . . , n} and j ∈ai,j ∧ j=1
let hc i = ai,0 ⇐ j=1{1, . . . , ℓi }, depth(subhcsH (ai,j )) < k. Also, because (H, P⊥ ) is body-disjoint,
pvs(subhcsH (ai,j ))’s are mutually
By construction, constr(ΘH , H) =V
Vndisjoint.
n
F
F
φ
and
constr
(Θ
,
H)
=
φ
where
i
H
i=1
i=1 i
V ℓi
i,j
i
constr(ΘH, subhcsH (ai,j )), hc i ) ∧ j=1
φi = constr(ΘH
V
ℓi
i,j
F
F
i
(Θ
constrφF=
constr
(Θ
,
hc
)
∧
i
i
H
H , subhcsH (ai,j ))
j=1

S ℓi
i,j
i,j
i
where ΘH
is the restriction of ΘH to pvs(subhcsH (ai,j )), and ΘH
= j=1
ΘH
.
F
Let σ be a satisfying assignment for constr (ΘH , H). Let σi,j be the rei,jstriction of σ to the unknowns in constrF (ΘH, subhcsH (ai,j )), and σhc i be theFirestriction of σ to the unknowns in constr (ΘH, hc i ). Let Pi,j be the predicate variable being applied in ai,j . Let βi,j be the non-linear unknown factor
corresponding to ai,j in constrF (ΘH , hc). By induction hypothesis, there exi,j′′′)(Pi,j ) =ists σi,jsuch that σi,j|= constr(ΘH, subhcsH (ai,j )) and sol(σi,j′′r · σ(βi,j ) · sol(σi,j )(Pi,j ). Let σhc i be such that σhc i (c) = r · σhc i (c) forS ℓi′′
the unknowns c ∈ dom(σhc i ) \ {βi,1 , . . . , βi,ℓi }. Let σi′ = σhc
σi,j
∪ j=1
,
i
S
n
′
′
′
′
and let σ = i=1 σi . As each σhc i and σi,j ’s are over mutually disjoint domains, it follows that σ ′ is a satisfying assignment for constr(ΘH , H) andsol(σ ′ )(root(H)) = r · sol(σ)(root(H)).
⊓⊔
We note that the above proof would fail if the input HCCS (H, P⊥ ) was not
body-disjoint, because the subtrees subhcsH (ai,j )’s in the proof of Lemma 6
may not be mutually disjoint. Indeed, Aatom may fail to find an atomic solution
if it was applied to an atomically solvable body-joined HCCS. (Modifying Aatomto solve the constraint c < 0 ∧ constrF (ΘH , H) instead of c < 0 ∧ constr(ΘH , H)
would make it complete for deciding atomic solvability for body-joined HCCSs
also, at the cost of non-linear constraint solving.)
B.5

Proof of Lemma 4

Lemma 4 A conjunctive body-disjoint and head-disjoint HCCS (H, P⊥ ) either
has an atomic solution or no solution.
Proof. Because (H, P⊥ ) is body-disjoint and head-disjoint, it follows that eachpredicate variable P occurs at most once in the head and once in the body ofsome clauses in H. Therefore, we can, without loss of generality, assume that:– for all P , its (at most two occurrences of) applications in H are of the same
form P (xffP ) with |x
P | = ar(P ),– for all P, Q, {xffP } ∩ {xQ } = ∅, andS– for all term variable x ∈ fvs(H) \ P {xfP }, if x ∈ fvs(hc 1 ) and x ∈ fvs(hc 2 ),then hc 1 = hc 2 .
By construction, (H, P⊥ ) has a solution if and only if |= ¬ lsol(H, P⊥ )(). Notethat lsol(H, P⊥ )() is a conjunction of literals t1 ≥ 0 ∧ · · · ∧ tn ≥ 0 because(H, P⊥ ) is conjunctive and head-disjoint. Suppose that |= ¬ lsol(H, P⊥ )() holds(i.e., (H, P⊥ ) has a solution). By the Farkas’ lemma [16], there are rational constants r1 , . . . , rn ≥ 0 such that r1 · t1 + · · · + rn · tn ≥ 0 can be equivalently transformed to r+0·x1 +· · ·+0·xm ≥ 0 for some r < 0. From the constants r1 , . . . , rn ,we can construct an atomic solution for (H, P⊥ ) as follows. Let P be a predicate
variable of H. Let {tP,1 ≥ 0, . . . , tP,ℓP ≥ 0} ⊆ {t1 ≥ 0, . . . , tn ≥ 0} be the literals
that occur in the subtree reachable from P . An atomic solution for (H, P⊥ ) isthen expressed by {P 7→ λxf
P .rP,1 · tP,1 + · · · + rP,ℓP · tP,ℓP ≥ 0 | P ∈ pvs(H)}.
⊓⊔