Probabilistic Inference for Predicate Constraint Satisfaction
Yuki Satake,1 Hiroshi Unno,1,2 Hinata Yanagi1
1

University of Tsukuba, 2 RIKEN AIP{satake,uhiro,hinata}@logic.cs.tsukuba.ac.jp

Abstract
In this paper, we present a novel constraint solving method fora class of predicate Constraint Satisfaction Problems (pCSP)
where each constraint is represented by an arbitrary clauseof first-order predicate logic over predicate variables. The
class of pCSP properly subsumes the well-studied class ofConstrained Horn Clauses (CHCs) where each constraint isrestricted to a Horn clause. The class of CHCs has been
widely applied to verification of linear-time safety properties of programs in different paradigms. In this paper, weshow that pCSP further widens the applicability to verification of branching-time safety properties of programs thatexhibit finitely-branching non-determinism. Solving pCSP
(and CHCs) however is challenging because the search
space of solutions is often very large (or unbounded), highdimensional, and non-smooth. To address these challenges,
our method naturally combines techniques studied separately
in different literatures: counterexample guided inductive synthesis (CEGIS) and probabilistic inference in graphical models. We have implemented the presented method and obtained
promising results on existing benchmarks as well as new ones
that are beyond the scope of existing CHC solvers.

1

Introduction

Constrained Horn Clauses (CHCs) (Grebenshchikov et al.
2012; Bjørner et al. 2015) is a class of constraint satisfaction problems where each constraint is represented by aHorn clause of first-order predicate logic with free predicate variables over a background theory such as quantifier
free linear integer arithmetic (QFLIA). Thanks to its expressiveness, the class has been widely adopted as a verification intermediate language to encode various verification problems of deciding whether the given linear-timesafety properties are satisfied by the given programs in different paradigms such as functional (Unno and Kobayashi2009), multi-threaded (Popeea and Rybalchenko 2012), imperative (Gurfinkel et al. 2015), and object-oriented programming (Kahsai et al. 2016). Accordingly, highly efficient CHC solvers like S PACER (Komuravelli, Gurfinkel,
and Chaki 2014), E LDARICA (Hojjat and Rümmer 2018),
and H O I CE (Champion et al. 2018) have been developed.
Copyright c 2020, Association for the Advancement of Artificial
Intelligence (www.aaai.org). All rights reserved.

This paper studies a generalization of CHCs called predicate Constraint Satisfaction Problems (pCSP) where eachconstraint is represented by an arbitrary (i.e., possibly
non-Horn) clause. We show that this generalization further
widens the applicability to verification of branching-timesafety properties of programs that exhibit finitely branching
non-determinism. In other words, this paves the way to use
pCSP as a common intermediate language for verificationof branching-time safety properties in place of CHCs thatis limited to a strict subclass (i.e., linear-time safety properties).1 One of the notable instances of branching-time safety
verification is non-termination verification where the goal is
to check whether there is a non-terminating execution of thegiven program (Gupta et al. 2008). For example, consider
the following program cnt :while (x ≥ 0) do
if * then x := x - 1 else x := x + 1
The program repeatedly and non-deterministically (indicated by *) decrements or increments the integer variable x
by 1 while the condition x ≥ 0 is satisfied. Suppose wewould like to verify that there is a non-terminating execution of the program under the precondition that the initialvalue of x is non-negative. The property actually holds because we can always take the else branch to avoid termination. The non-termination verification problem is reduced to
the following pCSP Cnt :!
x ≥ 0 ⇒ I(x),(I(x) ∧ x ≥ 0) ⇒ (I(x − 1) ∨ I(x + 1)) ,(I(x) ∧ x < 0) ⇒ ⊥Here, the predicate variable I represents a kind of loop
invariant (called a recurrent set in (Gupta et al. 2008;
Chen et al. 2014)) of the while loop and ⊥ represents thecontradiction. The first clause requires that I is satisfied by
all the initial valuation conforming to the precondition. The
1

The generalization however is still not sufficient for capturing programs with infinitely branching non-determinism and thefull class of properties (in particular, liveness ones) expressible bybranching-time temporal logics such as CTL, CTL*, and modal-mu
calculus. This restriction can be easily overcome by further extending pCSP with well-foundedness constraints, though the extended
class is out of the scope of this paper for simplicity of exposition.

second clause requires that I is preserved by either of thenon-deterministic branches. Note here that the use of nonHorn clause is essential to capture the existential or disjunctive nature of the non-termination property. The third clauseensures that if I is satisfied, the execution never exits thewhile loop. The problem has a solution (i.e., a satisfying assignment for the free predicate variable I) ρnt (I)(x) , x ≥0 and consequently the program is proved to have a diverging execution for any non-negative initial value of x.
Solving pCSP (and CHCs), however, is undecidable ingeneral. Developing an incomplete but practical method isstill challenging because the search space of solutions isoften (1) very large (or unbounded), (2) high-dimensional,and (3) non-smooth. To address these challenges, there havebeen proposed data-driven approaches to solving subclassesof CHCs based on counterexample guided inductive synthesis (CEGIS) (Solar-Lezama et al. 2006) combined with
template-based synthesis via SMT solvers (Sharma et al.
2013a; Garg et al. 2014), greedy set covering with logic
minimization (Sharma et al. 2013b; Padhi, Sharma, andMillstein 2016), decision tree learning (Garg et al. 2016;
Champion et al. 2018), randomized search (Sharma andAiken 2016), and reinforcement learning (Si et al. 2018).
Here, CEGIS is an iterative method that accumulates andexploits example instances E of the original constraint set C
in order to address the challenge (1), and has been widely
applied to formal verification and synthesis. Each iterationof CEGIS consists of a synthesis phase that attempts toguess candidate solutions (represented as predicate assignments ρ1 , . . . , ρm ) and a validation phase, where an SMT
solver is used to check whether C is satisfied by some candidate ρi . As soon as an iteration is reached where ρi satisfies C, we can conclude that C is satisfiable. The above
existing methods vary mainly in the synthesis phase.
In this paper, we present a novel constraint solving
method for the full class of pCSP (and obviously CHCs) thatcombines CEGIS with probabilistic inference in graphicalmodels, which has been studied in statistical machine learning and statistical physics literatures, for guessing candidate
solutions in the synthesis phase. In particular, we here adopt
survey propagation (SP) (Braunstein, Mézard, and Zecchina
2005; Kroc, Sabharwal, and Selman 2007; Maneva, Mossel,
and Wainwright 2007) in factor graphs (Kschischang, Frey,
and Loeliger 2001), which has been shown effective forsolving boolean Constraint Satisfaction Problems (bCSP)
where solutions (i.e., satisfying boolean assignments) arescattered among small clusters in the search space of solutions (Kroc, Sabharwal, and Selman 2007) (i.e., SP addresses the challenges (2) and (3) residing in bCSP as well).
To fill the gap between pCSP and bCSP, for each iteration of CEGIS, we apply predicate abstraction to the example instances E of the original constraint set C to obtain aboolean abstraction B of E, which is a bCSP. We then enumerate solutions of B by SP, concretize them back to solutions ρ1 , . . . , ρm of E, and return them as candidate solutionsof C. Here, thanks to the use of SP, our method tends to obtain simpler (per Occam’s razor) and different solutions (belonging to different clusters) for E, which tend to result in a
faster convergence of CEGIS in our method. We have imple-

mented the presented method and obtained promising results
on existing benchmark sets from SyGuS-Comp 2017 and2018 (Invariant Synthesis Track), and CHC-COMP 2019
(LIA-nonlin Track) as well as a new benchmark set consisting of pCSP that goes beyond the scope of existing CHC and
SyGuS solvers.
The rest of the paper is organized as follows. § 2 formalizes pCSP and § 3 discusses its application to branching-timesafety verification of programs with finitely branching nondeterminism. We then present our constraint solving method
for pCSP in § 4 and report on the implementation and experimental evaluation in § 5. We discuss related work in § 6 andconclude the paper in § 7.

2

Predicate Constraint Satisfaction Problems

This section defines the class of Predicate Constraint Satisfaction Problems (pCSP). For simplicity, we fix the background first-order theory of our predicate logic to quantifier
free linear integer arithmetic (QFLIA). We use φ and ψ asmeta-variables ranging over formulas of the logic. We assume that φ does not contain predicate variables, while ψ
may. We also use n as a meta-variable ranging over integer
constants. We write ftv (φ) for the set of free term variables
occurring in φ. A pCSP C is a finite set of clauses of the form
!
!
`
m
_
_
φ∨
Pi (e
xi ) ∨¬Pi (exi ) .
i=1i=`+1Here, x and P are meta-variables ranging over term andpredicate variables, respectively. We write xe for a sequenceof term variables, |ex| for its length, and ar(P ) for the arityof P . We write ftv (c) (resp. ftv (C)) for the set of free term
variables in the clause c (resp. in the pCSP C). We regard thevariables in ftv (c) as universally quantified implicitly. We
write fpv (C) for the set of free predicate variables occurring in C and atms(C) for the set { Pi (exi ) | i = 1, . . . , m }of predicate variable applications in C. A pCSP C is called
CHCs if ` ≤ 1 for all clauses c ∈ C. A CHCs C is called
linear CHCs if m − ` ≤ 1 for all c ∈ C. A predicate assignment ρ is a finite map from predicate variables P to closed
predicates of the form λx1 , . . . , xar(P ) .φ (i.e., a function thattakes integer arguments x1 , . . . , xar(P ) and returns whether
φ holds). We write ρ(C) for the application of ρ to C anddom(ρ) for the domain of ρ. We call ρ a solution (i.e., a satisfying predicate assignment) for C if V
fpv (C) ⊆ dom(ρ) andall clauses in ρ(C) are valid (i.e., |= ρ(C)). For example,
the predicate assignment ρnt is a solution of the pCSP Cnt
in § 1. A boolean Constraint Satisfiability Problem (bCSP)
B is defined as a pCSP that satisfies ar(P ) = 0 for all
P ∈ fpv (B). Note that a SAT solver can be used to decide
whether the given bCSP has a solution.

3 Application to Verification of
Branching-Time Safety Properties
In this section, we show that pCSP is expressible enoughto encode verification problems of branching-time safety
properties of looping programs with finitely branching non-determinism. The syntax of programs are defined as follows:(programs) c ::= x := a | c1 ; c2 | if b then c1 else c2| while b do c | assume b | assert b| if ∗q then c1 else c2(bool. exps.) b ::= > | ⊥ | a1 ≤ a2 | ¬b | b1 ∧ b2 | b1 ∨ b2
(arith. exps.) a ::= n | x | −a | a1 + a2 | a1 × a2
The one-step reduction relation −→ over program configurations (c, σ) is defined as usual (Winskel 1993). Informally, assert b aborts if b evaluates to ⊥ and does nothingotherwise. if ∗q then c1 else c2 non-deterministicallybranches to c1 or c2 , where q is either ∀ or ∃ indicating demonic or angelic non-determinism, respectively. A
branching-time safety verification problem of the given program c is that of deciding whether safe(c, σ) holds for any
valuations σ of the variables in c where safe(c, σ) is coinductively defined by: safe(c, σ) implies the following• c 6= assert ⊥,• if c = if ∗∃ then c1 else c2 , then there exists (c0 , σ 0 )such that (c, σ) −→ (c0 , σ 0 ) and safe(c0 , σ 0 ) holds, and• otherwise, for all (c0 , σ 0 ) such that (c, σ) −→ (c0 , σ 0 ),safe(c0 , σ 0 ) holds.
We next explain how to encode the given branching-timesafety verification problem as a pCSP. To this end, we extend Dijkstra’s predicate transformer (Winskel 1993) to ourtarget programs as follows:
wp(x := a, ψ) , [a/x]ψ
wp(c1 ; c2 , ψ) , wp(c1 , wp(c2 , ψ))wp(if b then c1 else c2 , ψ) , (b ⇒ wp(c1 , ψ)) ∧(¬b ⇒ wp(c2 , ψ))wp(while b do c, ψ) , I(e
x) ∧
[e
x1 /e
x](I(ex) ∧ b ⇒ wp(c, I(e
x)))
∧ [e
x2 /e
x](I(ex) ∧ ¬b ⇒ ψ)
wp(assume b, ψ) , b ⇒ ψ
wp(assert b, ψ) , b ∧ ψ
wp(if∗∀ then c1 else c2 , ψ) , wp(c1 , ψ)∧wp(c2 , ψ)wp(if∗∃ then c1 else c2 , ψ) , wp(c1 , ψ)∨wp(c2 , ψ)Here, [a/x]ψ is the formula obtained from ψ by replacing
the free occurrences of x with a. I represents a fresh predicate variable which is unique to the while loop, xe represents the sequence of the program variables (i.e., {ex} =ftv (b) ∪ ftv (c)), and x
e1 and x
e2 are fresh program variables
such that |ex| = |ex1 | = |ex2 |.
Example 3.1. For the running example cnt in § 1, we get2

The branching-time safety verification problem of thegiven program c is thus reduced to wp(c, >). Formally, we
can show the correctness of the reduction as follows.
Theorem 3.1. safe(c, σ) holds for all σ with ftv (c) ⊆dom(σ) if the pCSP wp(c, >) has a solution.3

3.1

Non-Termination Verification

As explained in § 1, the goal of non-termination verification is to check whether there is a non-terminating
execution of the given program. Non-termination verification can be considered as an instance of branchingtime safety verification. More specifically, given a program c, we assume that q = ∃ for every occurrenceof if ∗q then c1 else c2 in c and assert b does
not occur in c. Then, the non-termination verification problem with the precondition φ can be reduced to the pCSP
wp(assume φ; c; assert ⊥, >). Note that for the running
example cnt , wp(assume (x ≥ 0); cnt ; assert ⊥, >)coincides with the pCSP Cnt in § 1 (modulo α-conversion).

3.2

Extension to Recursive Functions

We can extend our encoding to support recursive functions.
We informally describe the extension using the following example recursive program cntrec (written in OCaml syntax):
let rec loop x =if x >= 0 thenif ∗∃ then loop(x-1) else loop(x+1)
else xlet main x =assume (x >= 0); loop x; assert ⊥This program behaves similarly to cnt in § 1. The nontermination verification problem of the recursive program is
reduced to the following pCSP Cntrec :(x < 0 ∧ x = y) ⇒ P (x, y), (x ≥ 0 ∧ P (x − 1, y1 ) ∧ P (x + 1, y2 )) ⇒ (P (x, y1 ) ∨ P (x, y2 )),(x ≥ 0 ∧ P (x, y)) ⇒ ⊥Here, the predicate variable P represents a postcondition of
the loop function relating the input x and the output y. The
first and the second clauses are respectively generated fromthe else- and then-branches of the if-expression in the loop
function. The third clause is generated from the main function. The non-deterministic behavior of the program is encoded in the second (non-Horn) clause. The problem hasa solution ρntrec (P )(x, y) , x < 0 and consequently
the loop function is proved to have a diverging execution
for any non-negative argument x .

4

Our Constraint Solving Method for pCSP

Note that this can be regarded as a pCSP.

This section describes our CEGIS-based method for finding
a solution of the given pCSP C. Our method iteratively accumulates example instances of C, from which we generatea sequence of candidate solutions for C until a genuine solution is found. We write E (i) for the set of example instances2
We here assume that ∗ in cnt is appropriately annotated with ∃(see § 3.1 for an explanation).

3
The converse also holds if we adopt the set-theoretic notion ofsolutions instead of the formula-definable ones.

wp(cnt , ψ) = I(x) ∧(I(x1 ) ∧ x1 ≥ 0) ⇒ (I(x1 − 1) ∨ I(x1 + 1))∧ (I(x2 ) ∧ x2 < 0) ⇒ [x2 /x]ψ)accumulated before the iteration i. Starting from E (1) = ∅,for each iteration i ≥ 1, we perform the following:

We then abstract each clause c ∈ E of the form5
(

(i)
(i)
ρ1 , . . . , ρ m(i)

1. Synthesis Phase: Find solutions(i)(i)
dom(ρ1 ) = · · · = dom(ρm ) = fpv (C)) for E
will be used as candidate solutions for C.
2.

(with
, which(i)each clause c ∈ C not satisfied by some ρj , we obtain a counterexample, i.e., an integer assignment σc such(i)that dom(σc ) = ftv (c) and 6|= σc (ρj (c)). We then up-

Pi (eni )) ∨ (i=1

In the synthesis phase, we apply predicate abstraction
and survey inspired decimation for enumerating solutionsof E (i) , which are respectively explained in § 4.1 and § 4.2.
The above CEGIS method is not guaranteed to terminate
due to the undecidability of pCSP but satisfies the so called
progress property: any counterexample σc found in an iteration i is never generated again in the succeeding iterations.
Example 4.1. Recall the running example Cnt in § 1. For
the first iteration, our implementation reported in § 5 obtains(1)
a candidate solution ρ1 (I)(x) , > from the initial set ofexample instances E (1) , ∅ in the synthesis phase. In thevalidation phase, we obtain a counterexample {x 7→ −1} forthe third clause, from which we obtain the updated example
instances E (2) , {¬I(−1)}. In the second iteration, we get(1)
a candidate solution ρ1 (I)(x) , x ≥ 0 from E (2) , which
satisfies all the clauses of Cnt in the validation phase. We(1)thus return ρ1 = ρnt as a solution of Cnt .

4.1

Predicate Abstraction of pCSP into bCSP

We now describe our predicate abstraction technique whichuses predicates for abstracting the example instances E (i)into a bCSP B. For linear CHCs, predicate abstraction has
been studied in (Srivastava and Gulwani 2009). We here
present predicate abstraction for pCSP E that satisfies thecondition ftv (E) = ∅ (recall ftv (E (i) ) = ∅ for any i ≥ 1),
which helps greatly reduce the computational cost.
We first prepare, for each P ∈ fpv (E), the following set
QP of predicates from the octahedron abstract domain:ar(P ){λx1 , . . . , xar(P ) . Σi=1 ci · xi ≥ c0 |(`_α(Pi (eni ))) ∨ (i=1

4Note that ftv (E (i+1) ) = ∅ holds since E (i+1) is obtained
from C by substituting all the term variables with concrete values. Thus, by regarding each P (en) ∈ atms(E (i+1) ) as a distinct(i+1)
boolean variable, E
can be considered as a bCSP.

m_¬α(Pi (eni )))

i=`+1

where
α(P (e
n)) ,

nd |Q
P|
_
^

ψj,k

j=1 k=1

ψj,k ,>¬bj,k(|= pk (en))(6|= pk (en)).

Here, pk represents the k-th predicate of QP , nd specifies
the maximum number of disjuncts allowed in disjunctive
normal form (DNF) solutions for P to be searched, and bj,kis a boolean variable indicating whether the predicate pk isused in the j-th disjunct of the DNF solutions for P . We thus
obtain the bCSP B as α(E) , { α(c) | c ∈ E }. We can show
the following correctness theorem of predicate abstraction.
Theorem 4.1. Let B , α(E) be the bCSP abstracted fromthe given pCSP E with ftv (E) = ∅. Let σ be a satisfying
boolean assignment for B (i.e., |= σ(B)) and γ(σ) be theconcretization of σ defined as the predicate assignment:γ(σ)(P ) , λx1 , . . . , xar(P ) .

nd |Q
P|
_
^

φj,k

j=1 k=1


φj,k ,

pk (x1 , . . . , xar(P ) ) (|= σ(bj,k ))>(6|= σ(bj,k )).

Then, γ(σ) is a solution for E.
Thus, predicate abstraction reduces the problem of finding
a solution for example instances E to that of finding a solution for the bCSP B , α(E). In our implementation reportedin § 5, we iteratively increment nd starting from 1 until we
obtain a solution for B. The convergence of the iterations
follows from the facts that E has a solution and for any satisfying boolean assignment for atms(E), there is a satisfying
predicate assignment for fpv (E) expressible as disjunctionsof conjunctions of QP (in other words, QP is adequate in
the sense defined in Section 4.1 of (Sharma et al. 2013b)).
Example 4.2. Recall the running example Cnt in § 1. In thesecond iteration of CEGIS, our implementation obtains thefollowing set QI of predicates for abstraction of I:{λx.>, λx.x ≥ 0, λx.x ≥ −1} .

ar(P )

c0 ∈ {0} ∪ {Σi=1 ci · ni | P (en) ∈ atms(E)} ∧c1 , . . . , car(P ) ∈ {−1, 0, 1}}.

¬Pi (e
ni ))

i=`+1

(i)

date E (i+1) = E (i) ∪ { σc (c) | c ∈ C ∧ ∃j. 6|= ρj (c) }and check whether E (i+1) has no solution by using a SAT
solver.4 If it is the case, we report that C has no solution.
Otherwise, we proceed to the next iteration with E (i+1) .

m_

into the following boolean clause α(c):(i)
Validation Phase: Check whether ρj is a genuine so-lution of C for some j by using an off-the-shelf SMT(i)solver. If so, we return ρj as a solution. Otherwise, for`_

Predicate abstraction of E (2) = {¬I(−1)} by QI yields thebCSP B = {b1,2 }, which has a satisfying boolean assignment σ , {b1,2 7→ >}, indicating that the second predicate λx.x ≥ 0 of QI must be used. We thus obtain the(1)candidate solution ρ1 = γ(σ) = {I 7→ λx.x ≥ 0}.
5

We here omit φ because it is equivalent to either > or ⊥.

4.2

Survey Inspired Decimation for bCSP

Our motivation to use SP is to enumerate simpler and essentially different solutions for E that accelerate and stabilize the convergence of CEGIS in our method. To this end,
we enumerate solutions of the bCSP α(E) that (1) belong
to different clusters in the space of boolean assignments and(2) assign as much variables as possible the boolean value ⊥(indicating that the corresponding predicate is not used).
We achieve the requirement (1) by survey inspired decimation (SID) (Braunstein, Mézard, and Zecchina 2005;
Kroc, Sabharwal, and Selman 2007; Maneva, Mossel, andWainwright 2007). SID iteratively assigns a boolean value
to a boolean variable with the highest bias towards the value,
which is computed from the result of SP as briefly reviewed
later in this section, in order not to kill too many clusters.
SID thus returns a partial assignment σ0 to some boolean
variables of α(E). We then use an ordinary SAT solver toenumerate solutions of α(E) belonging to different clusters by enumerating solutions of σ0 (α(E)). We try to satisfy
the requirement (2) by heuristically detecting and assigning
don’t-care variables ⊥.
Factor Graphs Any bCSP can be modeled as a factor
graph which is a bipartite graph representing the factorization of a probability distribution function. For example,
the following is the factor graph of the bCSP {b1 ∨ b2 ∨¬b3 , ¬b2 ∨ ¬b3 ∨ ¬b5 , b3 ∨ b4 ∨ b5 }:
b1

b3

f1

b4

f3
f2

b2

b5

Here, the square nodes labeled with f1 , f2 , and f3 represent
the clauses of the bCSP and the dashed (resp. solid) edges
connect each variable node bi to the square nodes that represent a clause containing ¬bi (resp. bi ). The graph represents
the following probability density distribution over boolean
random variables b1 , . . . , b5 .
1
f1 (b1 , b2 , b3 )f2 (b2 , b3 , b5 )f3 (b3 , b4 , b5 )Z
f1 (b1 , b2 , b3 ) = e−δ(b1 ∨b2 ∨¬b3 )µ(b1 , . . . , b5 ) =f2 (b2 , b3 , b5 ) = e−δ(¬b2 ∨¬b3 ∨¬b5 )
f3 (b3 , b4 , b5 ) = e−δ(b3 ∨b4 ∨b5 ) .
Here, Z is the normalization constant and the function δ isdefined by δ(⊥) = 1, δ(>) = 0. Note that µ(b1 , . . . , b5 ) has
the maximum value (i.e., 1/Z) if and only if the valuationof b1 , . . . , b5 is a satisfying assignment for the bCSP. We canthus solve the bCSP by performing probabilistic inference inthe factor graph to compute arg max µ(b1 , . . . , b5 ).
b1 ,...,b5

Survey Propagation (SP) SID relies on SP to find aboolean variable with the highest bias towards a boolean
value; The bias for each boolean variable bi is computed byusing
P SP to approximate the marginal probability µ(bi ) =b1 ,...,bi−1 ,bi+1 ,...,bm µ(b1 , . . . , bm ) after extending the domain of variables bi to the three values >, ⊥ and ∗ respectively meaning that the variable bi is forced to be > by aclause, forced to be ⊥ by a clause, and not forced at all (see(Braunstein, Mézard, and Zecchina 2005; Kroc, Sabharwal,
and Selman 2007; Maneva, Mossel, and Wainwright 2007)
for details of message passing algorithms for SP). If SP converges, we obtain Wi> , µ(bi = >), Wi⊥ , µ(bi = ⊥),and Wi∗ , µ(bi = ∗) for each variable bi . Then the variable bj with the highest bias |Wj> − Wj⊥ | is assigned to >if Wj> − Wj⊥ > 0 and ⊥ if Wj⊥ − Wj> > 0.

5

Implementation and Evaluation

We have implemented a constraint solver PCS AT for the fullclass of pCSP based on the presented method. We adopted
M INI S AT (Eén and Sörensson 2004) and Z3 (de Moura andBjørner 2008) as the backend SAT and SMT solvers, respectively. We conducted three sets of experiments. In thefirst experiment (§ 5.1), we used the benchmark set from
SyGuS-Comp 2018 (Invariant Synthesis Track) to evaluate the effectiveness of our SID-based technique to enumerate multiple candidate solutions for a faster convergenceof CEGIS. In the second experiment (§ 5.2), we used thebenchmark sets from SyGuS-Comp 2017 and 2018 (Invariant Synthesis Track)6 , and CHC-COMP 2019 (LIA-nonlin
Track)7 to compare PCS AT with existing SyGuS and CHC
solvers for solving linear CHCs and (non-linear) CHCs thatare proper subclasses of pCSP. Finally (§ 5.3), we tested
PCS AT on a new pCSP benchmark set consisting of nonHorn clauses that go beyond the scope of existing SyGuSand CHC solvers. All the experiments were conducted on
3.1GHz Intel Xeon Platinum 8000 CPU and 32 GiB RAM.

5.1

Evaluation of Multiple Solution Enumeration

We evaluated the impact of our SID-based multiple solution
enumeration technique on the convergence speed of CEGIS
using the benchmark set consisting of 127 linear CHCs
from the InvTrack category of SyGuS-Comp 2018 with 300s
timeout. Figure 1 summarizes the results of running PCS AT with different configurations obtained by varying thenumber “#cand” of candidate solutions generated in the synthesis phase, and enabling or disabling SID, which are respectively represented by “SAT(...)” and “SID(...)”. There,“#SAT” and “#UNSAT” respectively represent the numberof solved SAT and UNSAT instances (out of 127). Notethat PCS AT obtained the best result with SID(#cand=8). The
number of solved instances however slowly got worse withlarger #cand. This is because the overhead of synthesizing
and checking candidate solutions becomes non-negligible
for larger #cand. We believe the overhead can be further reduced by tweaking the implementation and expect that better
results can be obtained with larger #cand.
We also observed that: (1) the average number of iterations taken for the commonly solved instances by SID with
6
7

http://sygus.org/comp/https://chc-comp.github.io/

Time in seconds (logscale)

104
103

SID(#cand=1)
SID(#cand=2)
SID(#cand=4)
SID(#cand=8)
SID(#cand=16)
SID(#cand=32)
SID(#cand=64)
SAT(#cand=1)
SAT(#cand=2)
SAT(#cand=4)
SAT(#cand=8)

102
101
SAT(#cand=1)
SAT(#cand=8)
SID(#cand=1)
SID(#cand=8)

100
10-1
0

20

40

60

80

100

#SAT
91
92
96
100
96
95
94
94
92
91
89

#UNSAT
8
8
8
8
8
7
6
8
8
8
7

120

Benchmarks passed (of 127)

Figure 1: Comparisons of cumulative runtime (left) and number of solved instances (right) among different configurations#cand=1, 2, 4, 8 were 15.980, 12.684, 11.510, and 10.663,
respectively, and (2) the average elapsed time taken for thecommonly solved instances by SID with #cand=1, 2, 4,
8 were 6.246, 4.257, 5.558, and 6.201 (sec.), respectively.
These results show that SP accelerates and stabilizes theconvergence of CEGIS, though the improvement of averagetime reached the ceiling at #cand=2. The rest of the experiments was conducted using the configuration SID(#cand=8).

5.2Comparison with CHC and SyGuS Solvers

To compare with state-of-the-art SyGuS solvers for invariant synthesis, we tested PCS AT on the benchmark setsfrom the InvTrack category of SyGuS-Comp 2017 and 2018with 300s timeout. The benchmark sets consist of linear
CHCs. PCS AT solved 61 SAT and 7 UNSAT (out of 74),
and 100 SAT and 8 UNSAT (out of 127) instances respectively from the SyGuS-Comp 2017 and 2018 benchmark
sets. The champion solver L OOP I NV G EN (Padhi, Sharma,and Millstein 2016) of SyGuS-Comp 2017 was reported
to have solved 65 SAT instances within 3600s.8 The top
three solvers L OOP I NV G EN, CVC4, and D RYAD S YNTH of
SyGuS-Comp 2018 were reported to have solved 115, 109,
and 103 SAT instances respectively within 3600s.9 The results show that PCS AT is comparable to the state of theart invariant generation tools for the task of solving linear CHCs, despite the facts that PCS AT is designed for thestrictly larger class of constraints, not tuned for the class of
linear CHCs, and less mature than these tools.
We also tested PCS AT on the CHC benchmark set from
CHC-COMP 2019 (LIA-nonlin Track) with 300s timeout,
and compared with state-of-the-art CHC solvers. PCS AT
solved 58 SAT and 33 UNSAT instances out of 283 instancesfrom the CHC-COMP 2019 benchmark set. According to89https://sygus.org/comp/2017/report.pdf
https://sygus.org/comp/2018/report.pdf

the report of CHC-COMP 201910 , the state-of-the-art CHC
solver S PACER (Komuravelli, Gurfinkel, and Chaki 2014)
has solved 153 SAT and 117 UNSAT instances, and one of
the best CHC solvers H O I CE (Champion et al. 2018) has
solved 110 SAT and 66 UNSAT instances. The results showthat we need engineering efforts of tuning PCS AT for CHC
solving to compete with the mature and highly tuned CHC
solvers. In particular, the current version of PCS AT cannot
exploit the restricted (i.e. Horn) constraint form when applied to CHC solving. In other words, the generality of PCS AT resulted in a negative impact on the speed. In particular,
the current implementation is not well-tuned for proving theunsatisfiability of CHCs, though it is rather out of the scopeof this paper. We could exploit the Horn form of constraints
for finding a resolution derivation of the contradiction via
an efficient SLD-resolution. We could also implement constraint simplification and specialization for pre-processing,which are supported by the other solvers, to obtain better
results on SAT instances.

5.3

Evaluation on the New pCSP Benchmark Set

The new benchmark set consists of pCSP benchmarks that
encode branching-time safety verification problems, whichcannot be handled by existing SyGuS and CHC solvers. Table 1 summarizes the experiment results on the benchmark
set. The problems there are as follows:• “nt-intro” is the pCSP Cnt generated from the nontermination verification problem of cnt in § 1.
• “nt-rec” is the pCSP Cntrec generated from the nontermination verification problem of cntrec in § 3.2.
• “nt-sum” is the pCSP!
(x > 0 ∧ y = 0) ⇒ I(x, y),(I(x, y) ∧ x > 0) ⇒ (I(x, y) ∨ I(x − 1, y + x)),(I(x, y) ∧ x ≤ 0) ⇒ ⊥10

https://chc-comp.github.io/2019/chc-comp19.pdf

problems
nt-intro
nt-recnt-sumnt-sum-mod
nt-sum-rec

results
SAT
SAT
SAT
UNSAT
SAT

Table 1: Results on the new pCSP benchmark set
time (sec.) #iterations problems
results
0.425
1 eq
SAT
1.557
2 eq-mod
UNSAT
0.454
1 eq-recSAT
0.313
0 eq-mod-rec
UNSAT
0.686
2 nt-sum-mod-rec UNSAT

generated from the non-termination verification problem:
assume (x > 0 ∧ y = 0);(while(x > 0) do
if ∗∃ then y := y + x; x := x - 1)
assert ⊥• “nt-sum-mod” is the pCSP obtained from “nt-sum” bymodifying the precondition to x ≥ 0 ∧ y = 0, whichmakes the pCSP unsatisfiable.
• “nt-sum-rec” is the pCSP(x > 0 ∧ P (x − 1, y1 ) ∧ P (x, y2 )) ⇒(P (x, x + y1 ) ∨ P (x, y2 )), (x ≤ 0 ∧ y = 0) ⇒ P (x, y),(x > 0 ∧ P (x, y)) ⇒ ⊥generated from the recursive version of “nt-sum”:
let rec sum x =if x > 0 thenif *∃ then x + sum(x-1) else sum x
else 0let main x =assume (x > 0); sum x; assert ⊥• “nt-sum-mod-rec” is the pCSP generated from the recursive version of “nt-sum-mod”.
• “eq” is the pCSP
(x = x0 ∧ y = 0) ⇒ I(x0 , x, y), (I(x0 , x, y) ∧ x 6= 0) ⇒(I(x0 , x − 1, y + 1) ∨ I(x0 , x − 1, y)), (I(x0 , x, y) ∧ x = 0) ⇒ y = x0
from the branching-time safety verification problem:
assume (x = x0 ∧ y = 0);(while(x 6= 0) do
x := x - 1; if *∃ then y := y + 1);
assert (y = x0)• “eq-mod” is the pCSP obtained from “eq” by modifying
the conditional expression of the while loop to x > 0,
which makes the pCSP unsatisfiable.
• “eq-rec” is the pCSP
(x 6= 0 ∧ P (x − 1, y, z1 ) ∧ P (x − 1, y + 1, z2 )) ⇒(P (x, y, z1 ) ∨ P (x, y, z2 )), (x = 0 ∧ z = y) ⇒ P (x, y, z),P (x, 0, z) ⇒ z = x
generated from the recursive version of “eq”:

time (sec.)
1.332
1.261
0.932
1.142
0.284

#iterations
5
5
2
3
0

let rec loop x y =if x <> 0 thenif *∃ then loop (x - 1) yelse loop (x - 1) (y + 1)
else ylet main x =let z = loop x 0 in assert (z = x)
• “eq-mod-rec” is the pCSP generated from the recursive
version of “eq-mod”.
Note that PCS AT successfully solved these benchmarks,
which are impossible by existing SyGuS and CHC solvers,
in a reasonable amount of time.

6

Related WorkTo our knowledge, our method is the first to apply survey propagation in factor graphs to constraint solving forverification. Except the data-driven approaches for solving
subclasses of CHCs mentioned in § 1, various methods forsolving CHCs have been proposed. To name a few: methods based on counterexample guided abstraction refinement
and Craig interpolation (Unno and Kobayashi 2009; Hojjat
and Rümmer 2018), generalized property directed reachability (Hoder and Bjørner 2012; Komuravelli, Gurfinkel, andChaki 2014), constraint specialization (Angelis et al. 2014;
Kafle, Gallagher, and Morales 2016), and inductive theorem proving (Unno, Torii, and Sakamoto 2017). For linear
CHCs, a number of existing invariant synthesis techniques
can be applied straightforwardly. The most related to ours
among them is the method in (Gulwani and Jojic 2007),
which models constraints as factor graphs and performs a local search based on Gibbs sampling to find a peak of the joint
probability distribution represented by the factor graph. In
contrast to the above methods, our constraint solving method
supports the full class of pCSP.
An extension of CHCs called existentially quantified
CHCs has been proposed in (Beyene, Popeea, and Rybalchenko 2013). We observe that any pCSP can be reduced
to a problem of solving existentially quantified CHCs. Their
constraint solving method relies on a dedicated technique for
Skolemization of existential quantifiers, while our method
supports non-Horn clauses without any additional twist.

7

Conclusion

We have presented a novel constraint solving method for thefull class of pCSP based on CEGIS and probabilistic inference in graphical models, in particular, SP in factor graphs.
We have experimentally confirmed that our technique toenumerate multiple candidate solutions accelerates and stabilizes the convergence of CEGIS. We expect our predicate
abstraction technique from pCSP to bCSP paves the way
to applying other techniques from the constraint satisfaction literature. Another interesting research direction is to directly model pCSP as factor graphs representing joint probability distributions over random predicate variables and apply other probabilistic inference such as variational inference and approximate model counting.
Acknowledgments We would like to thank anonymousreferees for their useful comments. This work was partly
supported by JSPS KAKENHI Grant Numbers 15H05706,
16H05856, 17H01720, 17H01723, and 19H04084.

References
Angelis, E. D.; Fioravanti, F.; Pettorossi, A.; and Proietti,
M. 2014. VeriMAP: A tool for verifying programs throughtransformations. In TACAS ’14, 568–574. Springer.
Beyene, T. A.; Popeea, C.; and Rybalchenko, A. 2013. Solving existentially quantified Horn clauses. In CAV ’13, 869–
882.
Bjørner, N.; Gurfinkel, A.; McMillan, K. L.; and Rybalchenko, A. 2015. Horn clause solvers for program verification. In Fields of Logic and Computation II, 24–51.
Braunstein, A.; Mézard, M.; and Zecchina, R. 2005. Survey
propagation: An algorithm for satisfiability. Random Structures & Algorithms 27(2):201–226.
Champion, A.; Chiba, T.; Kobayashi, N.; and Sato, R. 2018.
ICE-based refinement type discovery for higher-order functional programs. In TACAS ’18, 365–384. Springer.
Chen, H. Y.; Cook, B.; Fuhs, C.; Nimkar, K.; and O’Hearn,
P. W. 2014. Proving nontermination via safety. In TACAS’14, volume 8413 of LNCS, 156–171. Springer.
de Moura, L., and Bjørner, N. 2008. Z3: An efficient SMT
solver. In TACAS ’08, 337–340. Springer.
Eén, N., and Sörensson, N. 2004. An extensible SAT-solver.
In SAT ’04, 502–518. Springer.
Garg, P.; Löding, C.; Madhusudan, P.; and Neider, D. 2014.
ICE: A robust framework for learning invariants. In CAV’14, 69–87. Springer.
Garg, P.; Neider, D.; Madhusudan, P.; and Roth, D. 2016.
Learning invariants using decision trees and implication
counterexamples. In POPL ’16, 499–512. ACM.
Grebenshchikov, S.; Lopes, N. P.; Popeea, C.; and Rybalchenko, A. 2012. Synthesizing software verifiers fromproof rules. In PLDI ’12, 405–416. ACM.
Gulwani, S., and Jojic, N. 2007. Program verification asprobabilistic inference. In POPL ’07, 277–289. ACM.
Gupta, A.; Henzinger, T. A.; Majumdar, R.; Rybalchenko,A.; and Xu, R.-G. 2008. Proving non-termination. In POPL
’08, 147–158. ACM.
Gurfinkel, A.; Kahsai, T.; Komuravelli, A.; and Navas, J. A.
2015. The SeaHorn verification framework. In CAV ’15,
343–361. Springer.

Hoder, K., and Bjørner, N. 2012. Generalized property directed reachability. In SAT ’12, 157–171. Springer.
Hojjat, H., and Rümmer, P. 2018. The Eldarica horn solver.
In FMCAD ’18. IEEE.
Kafle, B.; Gallagher, J. P.; and Morales, J. F. 2016. RAHFT:
A tool for verifying horn clauses using abstract interpretation and finite tree automata. In CAV ’16, 261–268. Springer.
Kahsai, T.; Rümmer, P.; Sanchez, H.; and Schäf, M. 2016.
JayHorn: A framework for verifying Java programs. In CAV’16, volume 9779, 352–358. Springer.
Komuravelli, A.; Gurfinkel, A.; and Chaki, S. 2014. SMTbased model checking for recursive programs. In CAV ’14,
volume 8559 of LNCS, 17–34. Springer.
Kroc, L.; Sabharwal, A.; and Selman, B. 2007. Survey propagation revisited. In UAI ’07, 217–226. AUAI Press.
Kschischang, F. R.; Frey, B. J.; and Loeliger, H. . 2001.
Factor graphs and the sum-product algorithm. IEEE Transactions on Information Theory 47(2):498–519.
Maneva, E.; Mossel, E.; and Wainwright, M. J. 2007. A newlook at survey propagation and its generalizations. Journalof the ACM 54(4).
Padhi, S.; Sharma, R.; and Millstein, T. D. 2016. Data-driven
precondition inference with learned features. In PLDI ’16,
42–56.
Popeea, C., and Rybalchenko, A. 2012. Compositional termination proofs for multi-threaded programs. In TACAS ’12,
volume 7214 of LNCS. Springer. 237–251.
Sharma, R., and Aiken, A. 2016. From invariant checking toinvariant inference using randomized search. Form. Methods
Syst. Des. 48(3):235–256.
Sharma, R.; Gupta, S.; Hariharan, B.; Aiken, A.; Liang, P.;
and Nori, A. V. 2013a. A data driven approach for algebraic
loop invariants. In ESOP ’13, 574–592. Springer.
Sharma, R.; Gupta, S.; Hariharan, B.; Aiken, A.; and Nori,
A. V. 2013b. Verification as learning geometric concepts. In
SAS ’13, 388–411. Springer.
Si, X.; Dai, H.; Raghothaman, M.; Naik, M.; and Song, L.
2018. Learning loop invariants for program verification. In
NeurIPS ’18, 7762–7773. Curran Associates, Inc.
Solar-Lezama, A.; Tancau, L.; Bodik, R.; Seshia, S.; andSaraswat, V. 2006. Combinatorial sketching for finite programs. In ASPLOS XII, 404–415. ACM.
Srivastava, S., and Gulwani, S. 2009. Program verification using templates over predicate abstraction. In PLDI ’09,
223–234. ACM.
Unno, H., and Kobayashi, N. 2009. Dependent type inference with interpolants. In PPDP ’09, 277–288. ACM.
Unno, H.; Torii, S.; and Sakamoto, H. 2017. Automating
induction for solving horn clauses. In CAV ’17, 571–591.
Springer.
Winskel, G. 1993. The Formal Semantics of Programming
Languages: An Introduction. MIT Press.