* Subramanian et al. (2011) Subramanian, G, Koch, Donald L & Fitzgibbon, Sean R 2011 The stability of a homogeneous suspension of chemotactic bacteria. Physics of Fluids 23 (4), 041901.
  * Swift & Hohenberg (1977) Swift, Ju & Hohenberg, Pierre C 1977 Hydrodynamic fluctuations at the convective instability. Physical Review A 15 (1), 319.
  * Swinney & Gollub (1981) Swinney, Harry L & Gollub, Jerry P 1981 Hydrodynamic instabilities and the transition to turbulence. Hydrodynamic instabilities and the transition to turbulence .
  * Thampi et al. (2014) Thampi, Sumesh P, Golestanian, Ramin & Yeomans, Julia M 2014 Vorticity, defects and correlations in active turbulence. Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences 372 (2029), 20130366.
  * Wan et al. (2021) Wan, Dongdong, Sun, Guangrui & Zhang, Mengqi 2021 Subcritical and supercritical bifurcations in axisymmetric viscoelastic pipe flows. arXiv preprint arXiv:2108.00220 .
  * Wioland et al. (2013) Wioland, Hugo, Woodhouse, Francis G, Dunkel, Jörn, Kessler, John O & Goldstein, Raymond E 2013 Confinement stabilizes a bacterial suspension into a spiral vortex. Physical review letters 110 (26), 268102.
  * Xiao-Gang et al. (2014) Xiao-Gang, Yang, Forest, M Gregory & Qi, Wang 2014 Near equilibrium dynamics and one-dimensional spatial—temporal structures of polar active liquid crystals. Chinese Physics B 23 (11), 118701.
  * Yang et al. (2014) Yang, X, Marenduzzo, D & Marchetti, MC 2014 Spiral and never-settling patterns in active systems. Physical Review E 89 (1), 012711.
  * Zhang et al. (2010) Zhang, He-Peng, Be’er, Avraham, Florin, E-L & Swinney, Harry L 2010 Collective motion and density fluctuations in bacterial colonies. Proceedings of the National Academy of Sciences 107 (31), 13626–13630.


# Topological Data Analysis of copy number alterations in cancer

Stefan Groha${}^{\text{1, 2, 3,}\dagger}$ Caroline
Weis${}^{\text{4,5,}\dagger}$ Alexander Gusev${}^{\text{1, 2, 3}}$ Bastian
Rieck${}^{\text{4,5}}$
${}^{\text{\sf 1}}$Dana Farber Cancer Institute; ${}^{\text{\sf 2}}$Harvard
Medical School; ${}^{\text{\sf 3}}$Broad Institute of MIT and Harvard
${}^{\text{\sf 4}}$Machine Learning and Computational Biology Lab, D-BSSE, ETH
Zurich, Switzerland
${}^{\text{\sf 5}}$SIB Swiss Institute of Bioinformatics, Switzerland
<EMAIL_ADDRESS><EMAIL_ADDRESS>
$\dagger$These authors contributed equally

(September 2020)

###### Abstract

Identifying subgroups and properties of cancer biopsy samples is a crucial
step towards obtaining precise diagnoses and being able to perform
personalized treatment of cancer patients. Recent data collections provide a
comprehensive characterization of cancer cell data, including genetic data on
copy number alterations (CNAs). We explore the potential to capture
information contained in cancer genomic information using a novel topology-
based approach that encodes each cancer sample as a persistence diagram of
topological features, i.e., high-dimensional voids represented in the data. We
find that this technique has the potential to extract meaningful low-
dimensional representations in cancer somatic genetic data and demonstrate the
viability of some applications on finding substructures in cancer data as well
as comparing similarity of cancer types.

##  1 Introduction

Copy number alterations (CNA) are structural somatic mutations where parts of
the genome gets repeated or lost. They are common in most cancers [2] and are
known to be involved in cancer development and progression [4, 22, 10].
Specific CNAs, as well as the total number of CNAs, were shown to be
prognostic for overall survival of cancer patients [20, 8, 16, 15],
underlining the importance of these somatic mutations. Furthermore, it has
been shown that cancer types can be inferred based on the CNA landscape with
simple classification algorithms [17, 21]. Differences in CNAs between lung
cancer subtypes, for instance, have also been observed [11], hinting at an
inherent structure of these tumor features based on _type_ and _subtype_ of
the underlying tumor. Being able to distinguish and correctly diagnose cancer
types and subtypes is of great clinical importance and finding latent
biological subgroups or characterizing unknown tumor samples is a question of
active research [3, 13, 17, 18].

Topological data analysis (TDA) is a tool to study the shape of point clouds,
characterizing the underlying physical structure in a representation that is
robust to noise, and flexible with respect to selecting a metric. It has
gained popularity in recent years due to the fact that it can facilitate the
analysis of high-dimensional data by generating meaningful low-dimensional
representations in terms of topological features [14, 9, 12].

We present a proof-of-concept study in which we apply TDA to cancer CNA data
to find representations of CNAs per cancer type and characterize similarity
between cancer types based on abstracted topological features of their CNA.
Furthermore, we examine if the pan-cancer CNA data set factorizes into
connected components and if cancer types have meaningful subgroups based on
their CNA profile. To the best of our knowledge, this is the first application
of the powerful framework of topological data analysis to this kind of data.

##  2 Methods

###  2.1 Topological data analysis

TDA is a recently-emerging field that aims to bring methods from algebraic and
differential topology to machine learning [7]. In contrast to more geometrical
techniques, TDA focuses on connectivity information, which is coarse but also
more impervious to noise in the data [6]. The flagship algorithm of TDA is
called _persistent homology_ , a technique for assigning point clouds a set of
topological descriptors. More precisely, with the underlying assumption being
that the data $\mathcal{X}:=\\{x_{1},x_{2},\dots,x_{n}\\}$ constitutes a
discrete sample from a high-dimensional manifold $\mathcal{M}$, persistent
homology analyses topological features of the point cloud $\mathcal{X}$ at all
possible scales. This results in a set of topological descriptors, the
_persistence diagrams_ , containing tuples from $\mathds{R}\times\mathds{R}$
that describe the “creation” and “destruction” of topological features.

The advantage of such a description is that the resulting features are
interpretable in low dimensions $d$, corresponding to _connected components_
($d=0$) and _cycles_ ($d=1$) in the data, respectively. Persistent homology
supports working with arbitrary similarity measures and metrics, making it a
highly flexible tool for our proposed analysis. We will subsequently calculate
the Vietoris–Rips complex $\operatorname{\mathfrak{V}}(\mathcal{X})$ of the
input data [19], subject to different similarity measures. Figure 1 depicts
the calculation; for illustrative purposes, we used the Euclidean distance
here.

(a) (b) (c) (d) (e)

Figure 1:  An illustration of the Vietoris–Rips complex construction process.
Starting from a set of points $\mathcal{X}$, we grow a set of solid spheres
(closed metric balls) of radius $\epsilon$ and start connecting points
whenever two of the solid spheres have a non-empty intersection (analogously,
for subsets satisfying pairwise intersections, we create $k$-cliques). While
we increase $\epsilon$, we keep track of topological features and mark their
creation and destruction in a _persistence diagrams_ (right-most plot). The
distance of any point to the diagonal in this diagram signifies its
_persistence_ , i.e., its prominence. In this example, we observe one high-
persistence point, namely the one corresponding to the large-scale cycle or
hole. Figure is modeled after Moor et al. [12].

###  2.2 Copy number alteration (CNA) dataset

We are basing the analysis on the AACR Project GENIE (Genomics, Evidence,
Neoplasia, Information, Exchange) [1] data collection. This database provides
a comprehensive resource for genetic cancer analysis by linking tumor genome
information with longitudinal clinical outcomes. In this work, we base our
analysis on copy number alteration (CNA) values, i.e., somatic changes
resulting in multiplication or loss of DNA sections, which are prevalent in
many types of cancer. The copy number alteration values are
$\in\\{-2,-1.5,-1,0,1,2\\}$, leading to a point cloud with discrete values; it
would be formally justified to treat it as a subset of some $\mathds{R}^{d}$,
but this structure is also a perfect use case for employing different
similarity measures. CNA values were determined for a number of genes known to
be related to cancer. As each hospital determined the CNA values for a
slightly different set of genes, and to avoid missing values, we focus on a
subset of patients with information present for the same genes, all sequenced
at Memorial Sloan Kettering Cancer Center. We furthermore restrict to the
largest cancer types with more than 500 samples each.

##  3 Experiments

###  3.1 Extraction of topological features per cancer type

We calculated persistence diagrams on CNA data subsets for each cancer type
separately. We applied two metrics to determine the distance between samples,
_Euclidean_ and _Cosine_ distance. Formally, the _Cosine_ distance just
constitutes a similarity measure, lacking some properties required for it to
be a metric, but the persistent homology calculations are still well-defined.
For three cancer types, the resulting persistence diagrams are depicted in
Figure 2. We observe that a higher number of topological features is detected
when using _Cosine_ than by using the _Euclidean_ distance. Their distance to
the diagonal indicates that the discovered features are also more persistent
than those defined through the _Euclidean_ distance. This reflects the
necessity of choosing a domain-specific similarity measure for such an
analysis.

We observe gaps between points of dimension $0$, indicating that well-
separated connected components are detected through TDA. We hypothesize that
these connected components stem from cancer subtypes, separated using a
topological lens for the feature space; a more in-depth investigation of this
will require topology-driven clustering algorithms [5].

Figure 2:  Persistence diagrams of cancer types non-small cell lung cancer,
breast cancer and cancer of unknown primary. Points indicating connected
components are depicted in red, point indicating cycles in blue. For each
type, the diagram calculated with euclidean distance is depicted in the first
row, and cosine distance in the second row.

A full overview of all persistence diagrams, illustrating the differences over
different cancer types, can be found in Appendix Figure 5.

We furthermore study the independence of all cancer types by combining the
persistence diagrams of all cancer types analyzed separately, and comparing
this union to the persistence diagram obtained from the full pan-cancer data
point-cloud. This is shown in Figure 3. We observe more structure when
overlaying the separate cancer types, which points to the fact that the cancer
types are somewhat overlapping in the high-dimensional CNA space; data points
in overlapping, denser regions are assigned to less persistent features and
are therefore not available for larger structures.

Figure 3:  Comparison of persistence diagrams obtained through extraction of
topological features using _Cosine_ distance; from the whole dataset,
combining all cancer types (left), and overlay of all persistence diagrams
calculated on seperate cancer type datasets (right).

###  3.2 Comparison of different cancer types

In addition, we compare the persistence diagrams to analyze whether the
topological representations are capable of uncovering similarities between
different cancer types. A suitable choice of distance metric between sub-
diagrams of persistence diagrams, with the same homological dimension, has to
be independent from the different number of detected features. Different
metrics are used to compare pairs of persistence diagrams, based on _heat
diffusion_ [14], _Wasserstein_ distance, or the commonly-used _bottleneck_
distance; both the Wasserstein distance and the bottleneck distance are
instances of metrics based on optimal transport, with the latter one being
more robust towards noise. Since we observed a clear dependency on the sample
size for the _heat diffusion_ kernel and the _Wasserstein_ distance, we chose
to apply the _bottleneck_ distance for the analysis. The resulting distance
matrix is depicted in Figure 4.

Renal cell carcinoma clearly stands out over other cancer types. The
persistence diagram calculated on the whole dataset, _pan-cancer_ ,
differentiates itself from all single cancer types.

Figure 4:  Heatmap depicting the _bottleneck_ distance between persistence
diagrams of different cancer types. The persistence diagram calculated from
the complete dataset, including all cancer types, is seen in _pan-cancer_.

##  4 Conclusion

We have shown that topological data analysis is a feasible tool to find
structure and meaningful representations in tumor copy number alteration data.
We have demonstrated that it is possible to detect subgroups of cancer types
based on the connected components of the CNA point cloud, which we hypothesize
to be subtypes. Furthermore, we have examined the similarity of cancer types
based on topological features extracted from the CNA profile and observe some
cancer types to be highly different. This study is a proof-of-concept of the
viability of topological data analysis on cancer data and further in-depth
analyses are required. Moreover, while only CNA values are used for this
study, there are many other somatic mutations (e.g., SNVs, fusions) providing
further information on the underlying representation of cancer, possibly
better characterizing cancer types and giving the prospect of extending the
current analysis to more modalities in future work.

## References

  * gen [2017] AACR project GENIE: Powering precision medicine through an international consortium.  _Cancer Discovery_ , 7(8):818–831, June 2017\.  doi: 10.1158/2159-8290.cd-17-0151.  URL https://doi.org/10.1158/2159-8290.cd-17-0151.
  * Beroukhim et al. [2010] R. Beroukhim, C. H. Mermel, D. Porter, G. Wei, S. Raychaudhuri, J. Donovan, J. Barretina, J. S. Boehm, J. Dobson, M. Urashima, et al.  The landscape of somatic copy-number alteration across human cancers.  _Nature_ , 463(7283):899–905, 2010.
  * Bindea et al. [2013] G. Bindea, B. Mlecnik, M. Tosolini, A. Kirilovsky, M. Waldner, A. C. Obenauf, H. Angell, T. Fredriksen, L. Lafontaine, A. Berger, et al.  Spatiotemporal dynamics of intratumoral immune cells reveal the immune landscape in human cancer.  _Immunity_ , 39(4):782–795, 2013.
  * Budczies et al. [2016] J. Budczies, M. Bockmayr, C. Denkert, F. Klauschen, S. Gröschel, S. Darb-Esfahani, N. Pfarr, J. Leichsenring, M. L. Onozato, J. K. Lennerz, et al.  Pan-cancer analysis of copy number changes in programmed death-ligand 1 (pd-l1, cd274)–associations with gene expression, mutational load, and survival.  _Genes, Chromosomes and Cancer_ , 55(8):626–639, 2016.
  * Chazal et al. [2013] F. Chazal, L. J. Guibas, S. Y. Oudot, and P. Skraba.  Persistence-based clustering in Riemannian manifolds.  _Journal of the ACM_ , 60(6), 2013.  doi: 10.1145/2535927.
  * Cohen-Steiner et al. [2007] D. Cohen-Steiner, H. Edelsbrunner, and J. Harer.  Stability of persistence diagrams.  _Discrete & Computational Geometry_, 37(1):103–120, 2007.
  * Edelsbrunner et al. [2002] H. Edelsbrunner, D. Letscher, and A. J. Zomorodian.  Topological persistence and simplification.  _Discrete & Computational Geometry_, 28(4):511–533, 2002.
  * Hieronymus et al. [2018] H. Hieronymus, R. Murali, A. Tin, K. Yadav, W. Abida, H. Moller, D. Berney, H. Scher, B. Carver, P. Scardino, et al.  Tumor copy number alteration burden is a pan-cancer prognostic factor associated with recurrence and death.  _Elife_ , 7:e37294, 2018.
  * Hofer et al. [2017] C. Hofer, R. Kwitt, M. Niethammer, and A. Uhl.  Deep learning with topological signatures.  In I. Guyon, U. V. Luxburg, S. Bengio, H. Wallach, R. Fergus, S. Vishwanathan, and R. Garnett, editors, _Advances in Neural Information Processing Systems 30_ , pages 1633–1643. Curran Associates, Inc., 2017.
  * Huang et al. [2017] Y.-S. Huang, W.-B. Liu, F. Han, J.-T. Yang, X.-L. Hao, H.-Q. Chen, X. Jiang, L. Yin, L. Ao, Z.-H. Cui, et al.  Copy number variations and expression of mpdz are prognostic biomarkers for clear cell renal cell carcinoma.  _Oncotarget_ , 8(45):78713, 2017.
  * Li et al. [2014] B.-Q. Li, J. You, T. Huang, and Y.-D. Cai.  Classification of non-small cell lung cancer based on copy number alterations.  _PLoS One_ , 9(2):e88300, 2014.
  * Moor et al. [2020] M. Moor, M. Horn, B. Rieck, and K. Borgwardt.  Topological autoencoders.  In _Proceedings of the 37th International Conference on Machine Learning (ICML)_ , Proceedings of Machine Learning Research. PMLR, 2020.
  * Penson et al. [2020] A. Penson, N. Camacho, Y. Zheng, A. M. Varghese, H. Al-Ahmadie, P. Razavi, S. Chandarlapaty, C. E. Vallejo, E. Vakiani, T. Gilewski, J. E. Rosenberg, M. Shady, D. W. Y. Tsui, D. N. Reales, A. Abeshouse, A. Syed, A. Zehir, N. Schultz, M. Ladanyi, D. B. Solit, D. S. Klimstra, D. M. Hyman, B. S. Taylor, and M. F. Berger.  Development of Genome-Derived Tumor Type Prediction to Inform Clinical Cancer Care.  _JAMA Oncology_ , 6(1):84–91, 01 2020.  ISSN 2374-2437.  doi: 10.1001/jamaoncol.2019.3985.  URL https://doi.org/10.1001/jamaoncol.2019.3985.
  * Reininghaus et al. [2015] J. Reininghaus, S. Huber, U. Bauer, and R. Kwitt.  A stable multi-scale kernel for topological machine learning.  In _Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition_ , pages 4741–4748, 2015.
  * Ried et al. [2019] T. Ried, G. A. Meijer, D. J. Harrison, G. Grech, S. Franch-Expósito, R. Briffa, B. Carvalho, and J. Camps.  The landscape of genomic copy number alterations in colorectal cancer and their consequences on gene expression levels and disease outcome.  _Molecular aspects of medicine_ , 69:48–61, 2019.
  * Shao et al. [2019] X. Shao, N. Lv, J. Liao, J. Long, R. Xue, N. Ai, D. Xu, and X. Fan.  Copy number variation is highly correlated with differential gene expression: a pan-cancer study.  _BMC medical genetics_ , 20(1):175, 2019.
  * Soh et al. [2017] K. P. Soh, E. Szczurek, T. Sakoparnig, and N. Beerenwinkel.  Predicting cancer type from tumour dna signatures.  _Genome medicine_ , 9(1):1–11, 2017.
  * Søndergaard et al. [2017] D. Søndergaard, S. Nielsen, C. N. Pedersen, and S. Besenbacher.  Prediction of primary tumors in cancers of unknown primary.  _Journal of integrative bioinformatics_ , 14(2), 2017.
  * Vietoris [1927] L. Vietoris.  Über den höheren Zusammenhang kompakter Räume und eine Klasse von zusammenhangstreuen Abbildungen.  _Mathematische Annalen_ , 97(1):454–472, 1927\.
  * Zhang et al. [2018] L. Zhang, N. Feizi, C. Chi, and P. Hu.  Association analysis of somatic copy number alteration burden with breast cancer survival.  _Frontiers in genetics_ , 9:421, 2018.
  * Zhang et al. [2016] N. Zhang, M. Wang, P. Zhang, and T. Huang.  Classification of cancers based on copy number variation landscapes.  _Biochimica et Biophysica Acta (BBA)-General Subjects_ , 1860(11):2750–2755, 2016.
  * Zhou et al. [2017] C. Zhou, W. Zhang, W. Chen, Y. Yin, M. Atyah, S. Liu, L. Guo, Y. Shi, Q. Ye, Q. Dong, et al.  Integrated analysis of copy number variations and gene expression profiling in hepatocellular carcinoma.  _Scientific reports_ , 7(1):1–11, 2017.

## Appendix

Figure 5:  Persistence diagrams of different cancer types using _Cosine_
distance. Points indicating connected components are depicted in red, point
indicating cycles in blue.


basicstyle = , breaklines = true, breakatwhitespace=true, upquote = true,
literate = │$\mid$1 |$\mid$1
{{1
}}1 .=.#=3 .<.#<3 .>.#>3 .=<.#=<4 .>=.#>=4 <<2 >>2 =<=<3 >=>=3
= \= 2
=\=2 ?-?- 3 :-:- 3
$1 keywords = , upquote = true, basicstyle = , basewidth = 0.48em,
numbers=none, xleftmargin=0cm, moredelim = *[s][]#pred., moredelim =
*[s][]#show., moredelim = *[s][]#hide., moredelim = *[s][](), moredelim =
*[s][]’’, commentstyle = , morecomment=[l]%, literate = |$\mid$1
$1 │$\mid$1, keywords = , upquote = true, basicstyle = , basewidth = 0.48em,
moredelim = **[is][]‘‘, moredelim = *[s][]#pred., moredelim = *[s][]#show.,
moredelim = *[s][]#hide., moredelim = *[s][](), moredelim = *[s][]’’,
moredelim = *[s][]:-., moredelim = *[s][]/**/, commentstyle = ,
morecomment=[l]%, morecomment=[s]/**/, literate = |$\mid$1 │$\mid$1 [[1 ]]1
$1 &((1 &))1 &..0
=\=2
$1,

11institutetext: CETINIA, Universidad Rey Juan Carlos, Madrid, Spain
22institutetext: Universidad Politécnica de Madrid, Spain 33institutetext:
IMDEA Software Institute, Madrid, Spain 44institutetext: University of Texas
at Dallas, Richardson, USA
44email<EMAIL_ADDRESS>44email: manuel.carro@{upm.es,imdea.org},
44email<EMAIL_ADDRESS>
# Towards Dynamic Consistency Checking in Goal-directed Predicate Answer Set
Programming

Joaquín Arias  11 0000-0003-4148-311X Manuel Carro 2233 0000-0001-5199-3135
Gopal Gupta 44 0000-0001-9727-0362

###### Abstract

Goal-directed evaluation of Answer Set Programs is gaining traction thanks to
its amenability to create AI systems that can, due to the evaluation mechanism
used, generate explanations and justifications. s(CASP) is one of these
systems and has been already used to write reasoning systems in several
fields. It provides enhanced expressiveness w.r.t. other ASP systems due to
its ability to use constraints, data structures, and unbound variables
natively. However, the performance of existing s(CASP) implementations is not
on par with other ASP systems: model consistency is checked once models have
been generated, in keeping with the generate-and-test paradigm. In this work,
we present a variation of the top-down evaluation strategy, termed _Dynamic
Consistency Checking_ , which interleaves model generation and consistency
checking. This makes it possible to determine when a literal is not compatible
with the _denials_ associated to the global constraints in the program, prune
the current execution branch, and choose a different alternative. This
strategy is specially (but not exclusively) relevant in problems with a high
combinatorial component. We have experimentally observed speedups of up to
90$\times$ w.r.t. the standard versions of s(CASP).

###### Keywords:

Dynamic Consistency Checking Goal-Directed Evaluation Constraints Answer Set
Programming

##  1 Introduction

s(CASP) [4] is a novel non-monotonic reasoner that evaluates Constraint Answer
Set Programs without a grounding phase, either before or during execution.
s(CASP) supports predicates and thus retains logical variables (and
constraints) both during the execution and in the answer sets. The operational
semantics of s(CASP) relies on backward chaining, which is intuitive to follow
and lends itself to generating explanations that can be translated into
natural language [2]. The execution of an s(CASP) program returns partial
stable models: the subsets of the stable models [10] which include only the
(negated) literals necessary to support the initial query. To the best of our
knowledge, s(CASP) is the only system that exhibits the property of relevance
[19]. s(CASP) has been already applied in relevant fields related to the
representation of commonsense reasoning:

  * •

An automated reasoner that uses Event Calculus (EC) [1]
(http://bit.ly/EventCalculus). s(CASP) can make deductive reasoning tasks in
domains featuring constraints involving dense time and continuous properties.
It is being used to model real-world avionics systems, to verify (timed)
properties, and to identify gaps with respect to system requirements [11].

  * •

The s(CASP) justification framework has been used to bring Explainable
Artificial Intelligence (XAI) principles to rule-based systems capturing
expert knowledge [2, 8].

  * •

It is at the core of two natural language understanding systems [6]: SQuARE, a
Semantic-based Question Answering and Reasoning Engine, and StaCACK, Stateful
Conversational Agent using Commonsense Knowledge. They use the s(CASP) engine
to ‘‘truly understand’’ and perform reasoning while generating natural
language explanations for their responses. Building on these systems, s(CASP)
was used to develop one of the nine systems selected to participate in the
Amazon Alexa Socialbot Grand Challenge 4
[7],111https://cs.utdallas.edu/computer-scientists-enhance-alexas-small-talk-
skills/ and is being used to develop a conversational AI chatbot.

  * •

It has been used in ILP systems that generate ASP programs [20] and concurrent
imperative programs from behavioral, observable specifications [22].

  * •

A legal expert system [18], developed at the SMU Centre for Computational Law
at Singapore, coded rule 34 of Singapore’s Legal
Profession.222https://github.com/smucclaw/r34˙sCASP Its front-end is a web
interface that collects user information, runs queries on s(CASP), and
displays the results with explanations in natural language.

  * •

s(LAW), an administrative and judicial discretion reasoner [5], which allows
modeling legal rules involving ambiguity and infers conclusions, providing
(natural language) justifications based on them.

However, in the standard implementation of s(CASP), the global constraints in
a program are checked when a tentative but complete model is computed. This
strategy takes a large toll on the performance of programs that generate many
tentative models and use global constraints to discard those that do not
satisfy the specifications of the problem.

In this work, we propose a technique termed _Dynamic Consistency Checking_
(DCC) that anticipates the evaluation of global constraints to discard
inconsistent models as early as possible. Before adding a literal to the
tentative model, DCC checks if any global constraint is violated. If so, this
literal is discarded and the evaluation backtracks to look for other
alternatives. We show, through several examples, that using this preliminary
implementation, s(CASP) with DCC is up to 90$\times$ faster. Section 2
contains an overview of the syntax, operational semantics, and implementation
of s(CASP). Section 3 explains the motivation behind DCC with examples, and
describes its design and implementation Section 4 presents the evaluating
results of several benchmarks using s(CASP) with DCC enabled or not. Finally,
in Section 5 we draw conclusions and propose future work. All the program and
files used or mentioned in this paper are available at
http://platon.etsii.urjc.es/~jarias/papers/dcc-padl21/.

##  2 Background: s(CASP)

An s(CASP) program is a set of clauses of the following form:

a:-ca, b1, $\dots$, bm, not bm+1, $\dots$, not bn.

where a and b1, $\dots$, bn are atoms. An atom is either a propositional
variable or the expression p(t1, $\ldots$, tn) if p is an $n$-ary predicate
symbol and t1, $\ldots$, tn are terms. A term is either a variable xi or a
function symbol f of arity n, denoted as f/n, applied to $n$ terms, e.g.,
f(t1, t2, $\ldots$, tn), where each ti is in turn a term. A function symbol of
arity 0 is called a constant. Therefore, s(CASP) accepts terms with the same
conventions as Prolog: f(a, b) is a term, and so are f(g(X),Y) and [f(a)|Rest]
(to denote a list with head f(a) and tail Rest). Program variables are usually
written starting with an uppercase letter,333There are additional syntactical
conventions to distinguish variables and non-variables that are of no interest
here. while function and predicate symbols start with a lowercase letter.
Numerical constants are written solely with digits.

The term ca is a simple constraint or a conjunction of constraints: an
expression establishing relations among variables in some constraint system
[15]. Similar to CLP, s(CASP) is parametrized w.r.t. the constraint system,
from which it inherits its semantics. Since the execution of an s(CASP)
program needs negating constraints, soundness requires that this can be done
in the chosen constraint system by means of a finite disjunction of basic
constraints [9, 21].

At least one of a, bi, or not bi must be present. When the head a is not
present, it is supposed to be substituted by the head _false_. Headless rules
have then the form

:-ca, b1, $\dots$, bm, not bm+1, $\dots$, not bn.

and their interpretation is that the conjunction of the constraints and goals
has to be false, so at least one constraint or goal has to be false. For
example, the rule :-p, q, expresses that the conjunction of atoms p $\land$ q
cannot be true: either p, q, or both, have to be false in any stable model.
ASP literature often uses the term _constraint_ to denote these constructions.
To avoid the ambiguity that may arise from using the same name for constraints
appearing among (free) variables during program execution and in the final
models and for rules without heads, we will refer to headless rules as
_denials_ [16].

The execution of an s(CASP) program starts with a _query_ of the form

?- ca, b1, $\dots$, bm, not bm+1, $\dots$, not bn.

The s(CASP) answers to a query are _partial_ stable models where each one is a
subset of a stable model that satisfies the constraints, makes non-negated
atoms true, makes the negated atoms non-provable, and, in addition, includes
only atoms that are relevant to support the query. Additionally, for each
partial stable model s(CASP) returns on backtracking _partial answer sets_
with the justification tree and the bindings for the free variables of the
query that correspond to the most general unifier (_mgu_) of a successful top-
down derivation.

###  2.1 Execution Procedure of s(CASP)

Let us present an abridged description of the top-down strategy of s(CASP):

  1. 1.

Rules expressing the constructive negation of the predicates in the original
ASP program are synthesized. We call this the _dual program_. Its mission is
to provide a means to constructively determine the conditions and constraints
under which calls to non-propositional predicates featuring variables would
have failed: if we want to know when a rule such as p(X,Y):-q(X), not r(Y)
succeeds, the dual program computes the constraints on Y under which the call
r(Y) would fail. This is an extension of the usual ASP semantics that is
compatible with the case of programs that can be finitely grounded.444Note
that, in the presence of function symbols and constraints on dense domains,
this is in general not the case for s(CASP) programs. A description of the
construction of the dual program can be found in [3, 4, 14].

  2. 2.

The original program is checked for loops of the form r:-q, not r. and
introduces additional denials to ensure that the models satisfy $\lnot q\lor
r$, even if the atoms r or q are not needed to solve the query. This is done
by building a dependency graph of the program and detecting the paths where
this may happen, including call paths across calls. Therefore, for the
program:

⬇

1p :- not q.

2q :- not p.

3r :- not r.

s(CASP) will determine that there are no stable models, regardless of the
initial query. For the propositional case, such an analysis can be precise.
For the non-propositional case, an over-approximation is calculated. In both
cases, denials that are not used during program evaluation can be generated.
These may impose a penalty in execution time, but are safe.

  3. 3.

The denials generated in point 2, together with any denials present in the
original program, are collected in predicates synthesized by the compiler that
are evaluated by adding an auxiliary goal, nmr_check/0, at the end of the top-
level query.

  4. 4.

The union of the original program, the dual program, and the denials is
handled by a top-down algorithm that implements the stable model semantics.

Point number 4 is specially relevant. The dual program (point 1) is
synthesized by means of program transformations drawing from classical logic.
However, its intended meaning differs from that of first-order logic. That is
so because it is to be executed by a metainterpreter that does not implement
the inference mechanisms of first-order logic, as it is designed to ensure
that the semantics of answer set programs is respected (see Section 2.4). In
particular, it treats specifically cyclic dependencies involving negation.

###  2.2 Unsafe Variables and Uninterpreted Function Symbols

The following code, from [3, Pag. 9] has variables that would be termed as
_unsafe_ in regular ASP systems: variables that appear in negated atoms in the
body of a clause, but that do not appear in any positive literal in the same
body.

⬇

1p(X):- q(X, Z), not r(X).

2p(Z):- not q(X, Z), r(X).

3q(X, a):- X #> 5.

4r(X):- X #< 1.

Since s(CASP) synthesizes explicit constructive goals for these negated goals,
the aforementioned code can be run as-is in s(CASP). The query ?-p(A).
generates three different answer sets, one for each binding:

⬇

{ p(A| {A #> 5}), q(A| {A #> 5}, a), not r(A| {A #> 5}) }

A #> 5

{ p(A| {A \= a}), not q(B| {B #< 1}, A| {A \= a}), r(B| {B #< 1}) }

A \= a

{ p(a), not q(B| {B #< 1}, a), r(B| {B #< 1}) }

A = a

where the notation V|{C} for a variable V is intended to mean that V is
subject to the constraints in {C}. The constraints A = 5, A $\not=$ a, and A =
a correspond to the bindings of variable A that make the atom from the query
?-p(A) belong to the stable model.

Another very relevant point where s(CASP) differs from ASP is in the
possibility of using arbitrary uninterpreted function symbols to build, for
example, data structures. While in mainstream ASP implementations these could
give rise to an infinite grounded program (i.e., if the program does not have
the _bound-term-depth_ property), the s(CASP) execution model can deal with
them similarly to Prolog, with the added power of the use of constructive
negation in the execution and in the returned models.

###### Example 1

The predicate member/2 below, from [3, Pag. 11], models the membership to a
list as it is usual in (classical) logic programming. The query is intended to
derive the conditions for one argument not to belong to a given list.

⬇

1member(X, [X|Xs]).

2member(X, [_|Xs]):- member(X, Xs).

3list([1,2,3,4,5]).

4?- list(A), not member(B, A).

This program and query return in s(CASP) the following model and bindings:

⬇

{ list([1,2,3,4,5]),

not member(B| {B \= 1,B \= 2,B \= 3,B \= 4,B \= 5}, [1,2,3,4,5]),

not member(B| {B \= 1,B \= 2,B \= 3,B \= 4,B \= 5}, [2,3,4,5]),

not member(B| {B \= 1,B \= 2,B \= 3,B \= 4,B \= 5}, [3,4,5]),

not member(B| {B \= 1,B \= 2,B \= 3,B \= 4,B \= 5}, [4,5]),

not member(B| {B \= 1,B \= 2,B \= 3,B \= 4,B \= 5}, [5]),

not member(B| {B \= 1,B \= 2,B \= 3,B \= 4,B \= 5}, []) }

A = [1,2,3,4,5], B \= 1, B \= 2, B \= 3, B \= 4, B \= 5

I.e., for variable B not to be a member of the list [1,2,3,4,5] it has to be
different from each of its elements.

###  2.3 s(CASP) as a Conservative Extension of ASP

The behavior of s(CASP) and ASP is the same for propositional programs. They
differ in programs with unsafe variables (not legal in mainstream ASP
systems), programs that could create unbound data structures, or whose
variable ranges are defined in infinite domains (either unbound or bound but
dense). Such programs are outside the standard domain of ASP systems as they
cannot be finitely grounded, For them, s(CASP) extends ASP consistently.

In addition, the domain of the variables is implicitly expanded to include a
domain which can be potentially infinite. Let us use the following example,
from [3, Pag. 12], where we are interested in knowing whether p(X) (for some
X) is or not part of a stable model:

⬇

1d(1).

2p(X) :- not d(X).

The only constant in the program is 1, which is the only possible domain for X
in the second clause. That clause is not legal for ASP, as X is an unsafe
variable (Section 2.2). Adding a domain predicate call for it (i.e., adding
d(X) to the body of the second clause), makes its model be {d(1)} (not p(1) is
implicit).

That second clause is however legal in s(CASP). Making the query ?-p(X)
returns the _partial_ model {p(X| {X \= 1}), not d(X| {X \= 1})} stating that
p(X) and not d(X) are true when X \= 1, which is consistent with, but more
general than, the model given by ASP. As the model is partial, only the atoms
(perhaps negated) involved in the proof for ?-p(X) appear in that model.

###  2.4 The s(CASP) Interpreter

⬇

1scasp(Query) :-

2 solve(Query,[],Mid),

3 solve_goal(nmr_check,Mid,Model),

4 print_just_model(Model).

5

6solve([],In,[’\$success^{\prime}|In]).solve([Goal|Gs],In,Out):-solve_{g}oal(Goal,In,Mid),solve(Gs,Mid,Out).\par
solve_{g}oal(Goal,In,Out):-user_{d}efined(Goal),!,@@check_{l}oops(Goal,In,Out).solve_{g}oal(Goal,In,Out):-Goal=forall(Var,G),!,@@c_{f}orall(V,G,In,Out).@@solve_{g}oal(Goal,In,Out):-call(Goal),@@Out=[^{\prime}\
$success’,Goal|In].

7

8check_loops(Goal,In Out) :-

9 loop_type(Goal,In,Loop),

10 s_loop(Loop,Goal,In,Out).

11

12s_loop(odd,_,_,_) :- fail.

13s_loop(even,G,In,[chs(G)|In]).

14s_loop(no_loop,G,In,Out) :-

15 pr_rule(G, Body),

16 solve(Body,[G|In],Out).

17s_loop(proved,G,In,[proved(G)|In]).

18s_loop(positive,_,_,_) :- fail.

Figure 1: Outline of the s(CASP) interpreter’s code implemented in Ciao
Prolog.

Queries to the original program extended with the dual rules are evaluated by
a runtime environment. This is currently a metainterpreter (see Fig. 1) in
Prolog that executes an algorithm [12] that has similarities with SLD
resolution. But it takes into account specific characteristics of ASP and the
dual programs, such as the denials, the different kinds of loops, and the
introduction of universal quantifiers in the body of the clauses:

  1. 1.

The query Query is evaluated invoking solve/3 in line 2 starting with an empty
model represented as the empty list [].

  2. 2.

After the query evaluation, and to ensure that the returned model, Mid, is
consistent with the denials, nmr_check (item 3 in page 3) is evaluated in line
3.

  3. 3.

In line 4, the models that are consistent (and their justifications), Model,
are output by print_just_model/1.

  4. 4.

The predicate solve/3 receives a list with the literals in the query (or in
the body of some rule) and evaluates them, one by one, invoking solve_goal/3.

  5. 5.

When the literal is a user defined predicate (line 6), the interpreter checks
if there is a loop invoking check_loops/3. Three main cases are distinguished
by type_loop/3:

Odd loop

When a call eventually invokes itself and there is an odd number of
intervening negations (as in, e.g., p:- q. q:- not r. r:- p.), the evaluation
fails in line 12, to avoid contradictions of the form $p\land\lnot p$, and
backtracking takes place.

Even loop

When there is an even number of intervening negations (as in p:- not q. q:- r.
r:- not p.), the metainterpreter succeeds in line 13 to generate several
stable models, such as {p, not q, not r} and {q, r, not p}.

No loop

If no loops are detected, in line 14 the interpreter invokes pr_rule/2 to
retrieve the rule that unifies with the goal G and continues the evaluation by
invoking solve/3 with the literals of the rule.

  6. 6.

The construction forall(Var, G) in line 6 is the dual of the existential
quantifications in the body of the clauses. To evaluate them the runtime
environment invokes the predicate c_forall/4 in line 6, which determines if G
holds for all the values of Var \--- see [4] for implementation details.

  7. 7.

Finally, operations involving constraints and/or builtins are natively handled
by invoking call/1 in line 6.

##  3 Dynamic Consistency Checking in s(CASP)

The Dynamic Consistency Checking proposal of [13] is designed for
propositional programs, while our proposal can also take care of predicate ASP
programs. It is based on anticipating the evaluation of denials to fail as
early as possible

###  3.1 Motivation

As we mentioned before, a denial such as :-p, q, expresses that the
conjunction of atoms p $\land$ q cannot be true: either p, q, or both, have to
be false in any stable model. In predicate ASP the atoms have variables and a
denial such as :-p(X), q(X,Y) means that:

$false\ \ \leftarrow\ \exists x,y\ (\ p(x)\land q(x,y)\ )$

i.e., p(X) and q(X,Y) can not be simultaneously true for any possible values
of X and Y in any stable model. To ensure that the tentative partial model is
consistent with this denial, the compiler generates a rule of the form

$\forall x,y\ (chk_{i}\ \ \leftrightarrow\ \lnot(\ p(x)\land q(x,y)\ )\ )$

and to ensure that each sub-check ($chk_{i}$) is satisfied, they are included
in the rule $nmr\\_check\leftarrow chk_{1}\land\dots\land chk_{k}\land\ldots$,
which is transparently called after the program query by the s(CASP)
interpreter (see Fig. 1, line 3).

However, this generate-and-test strategy has a high impact on the performance
of programs that create many tentative models and use denials to discard those
that do not satisfy the constraints of the problem.

⬇

1reachable(V) :- chosen(a, V).

2reachable(V) :- chosen(U, V), reachable(U).

3chosen(U, V) :- edge(U, V), not other(U, V). % Choose or not an

4other(U, V) :- edge(U, V), not chosen(U, V). % edge of the graph.

5

6:- vertex(U), not reachable(U). % Every vertex must be reachable.

7:- chosen(U, W), U \= V, chosen(V, W). % Do not choose edges to or

8:- chosen(W, U), U \= V, chosen(W, V). % from the same vertex.

9#show chosen/2.

10

11?- reachable(a). % Is there a path from a to a?

Figure 2: Code of the Hamilonian problem à la ASP, available at
hamiltonian.pl.

⬇

1% Graph

2vertex(a).

3vertex(b).

4vertex(c).

5vertex(d).

6edge(b, a).

7edge(b, d).

8edge(a, c).

9edge(a, b).

10edge(b, c).

11edge(c, d).

12edge(d, a).

13edge(c, a).

14edge(a, d).

15edge(d, b).

Figure 3: Graph with 4 nodes available at graph_4.pl.

abdc

######  Example 2 (Hamiltonian path problem)

Consider the Hamiltonian path problem, in which for a given graph we search
for a cyclic path that visits each node of the graph only once. The standard
ASP code for this problem, available at hamiltonian.pl, is in Fig. 2. The
conditions of the problem are captured (i) in line 6 to discard tentative
paths that do not visit all the nodes, and (ii) in lines 7-8 to discard paths
that have edges violating the properties of the Hamiltonian path. For the
query in line 11, using the graph in Fig. 3 there are three stable models, one
for each Hamiltonian cycle:

⬇

1{ chosen(a,c), chosen(c,d), chosen(d,b), chosen(b,a),$\dots$ }

2{ chosen(a,b), chosen(b,c), chosen(c,d), chosen(d,a),$\dots$ }

3{ chosen(a,d), chosen(d,b), chosen(b,c), chosen(c,a),$\dots$ }

As mentioned before, the standard s(CASP) execution follows a generate-and-
test scheme, choosing a cycle that reaches node a from node a and then
discards any cycle in which:

  * •

Not all vertices are reached (line 6), e.g., \\{chosen(a,b),chosen(b,a)\

.

Two chosen edges reach / leave the same vertex (line 7), e.g., \\{chosen(a,b),
chosen(d,b), chosen(b,a)\

or \\{chosen(a,b), chosen(b,d), chosen(b,a)\. As a consequence, if the
evaluation chooses an edge that breaks any of these conditions, trying
combinations with the rest of the edges would be misused effort.

###  3.2 Outline of the DCC Approach

The main idea behind our proposal is to anticipate the evaluation of the
denials to fail and backtrack as early as possible. When an atom involved in a
denial is a candidate to be added to a tentative model, the denial is checked
to ensure that it is not already violated. By contrast, the classical
implementation of s(CASP) checked the tentative model as a whole once it had
been completely built. The latter is akin to the generate-and-test approach to
combinatorial problems, while the former tries to cut the search early. In the
most general case, DCC can take the form of a constraint-and-test instance.
While detecting some denial violations can be performed by just checking the
current state of the (partial) candidate model, better, more powerful
algorithms can impose additional constraints on the rest of the atoms
belonging to the partial model and also on the parts of the denials that
remain to be checked. These constraints can propagate additional conditions
through the candidate model to ensure that it is consistent with the denials.
These conditions will also remain active for the rest of the construction of
the model, so that they can be carried forward, further reducing the search
space. Note that since s(CASP) includes constraints _à la_ CLP, the effect is
very similar to the constraint propagation mechanisms that take place in
constraint satisfaction systems, therefore making a full s(CASP) + DCC system
an instance of a constraint-and-generate evaluation engine. The current
implementation, which we describe in this paper, is a _proof of concept_ that
only checks grounds literals and does not anticipate the consistency check of
constrained literals. As we will see later, this does not have a negative
impact on the soundness of the system.

###  3.3 Implementation of DCC in s(CASP)

The implementation of s(CASP) + DCC is available as part of the source code of
s(CASP) at https://gitlab.software.imdea.org/ciao-lang/scasp.

####  3.3.1 Compilation of the Denials

As we mentioned before, the denials are compiled in such a way that the
interpreter checks consistency by proving that forall possible values, the
negation of the denial is satisfied. For example, for the denial :-p(X),
q(X,Y), the compiler generates the rule:

⬇

chk1 :- forall(X, forall(Y, not chk_body(X,Y))).

not chk_body(X,Y) :- not p(X).

not chk_body(X,Y) :- p(X), not q(X,Y).

The last clause includes a call to p(X) to avoid duplicated solutions provided
by the two clauses. If the interpreter is able to prove that for all the
possible values of X and Y the tentative partial model is consistent with the
predicate not chk_body(X,Y), then it means that the tentative partial model is
a stable partial model. The approach followed by the DCC proposal is to detect
when a rule like the above determines that a model candidate is inconsistent.
If that is the case, s(CASP) fails and provokes backtracking to explore the
generation of a different model. In the example above, if a model being
generated is consistent with p(X) $\land$ q(X,Y), then it should be discarded.
Since it is only necessary to check for violation of denials when adding a
goal involved in one of the denials, the compiler creates a series of rules
that state what has to be checked for in case a goal involved in the denial is
generated. For the case above, if p(X) is added, then q(X,Y) has to be checked
to ensure it does not hold, and the other way around. This is represented as:

⬇

dcc(p(X), [q(X,Y)]).

dcc(q(X,Y), [p(X)]).

which can be understood as ‘‘if p(X) is present, check that q(X,Y) is not
present’’. In general, given a denial of the form :-c$_a$, b$_1$, $\dots$,
b$_n$ for each (negated) literal b$_k$, of a user defined predicate, the
compiler generates a DCC rule dcc(b$_k$, [c$_a$, $\dots$,
b$_{k-1$,b$_k+1,…$])$ for each $k,1\leq k\leq n$.

⬇

% The only clauses that changes

s_loop(even,G,In,[chs(G)|In]) :-

eval_dcc(G,In). % New call

s_loop(no_loop,G,In,Out) :-

pr_rule(G, Body),

solve(Body,[G|In],Out),

eval_dcc(G,In). % New call

eval_dcc(G,In):-

\\+ &( ground(G),

pr_dcc_rule(G,F_Atoms),

holds_dcc(F_Atoms,In) &).

holds_dcc([],_).

holds_dcc([F_A|F_As],In) :-

holds_dcc_(F_A,In),

holds_dcc(F_As,In).

holds_dcc_(F_A,In) :-

user_defined(F_A), !,

member(F_A,In).

holds_dcc_(F_A,In) :-

call(F_A).

Figure 4: Outline of the changes to the s(CASP) interpreter extended with DCC.

####  3.3.2 Extending the s(CASP) interpreter with DCC

Fig. 4 shows the relevant fragment of the s(CASP) interpreter extended with
Dynamic Consistency Checking. The basic intuition is that as soon as an atom
that is involved in a denial is a candidate to be added to a model, DCC checks
whether the candidate model is consistent with the rest of the atoms
(including builtins) in that denial. Depending on the result of this check,
the candidate atom is added or not. The modified interpreter performs the
following steps:

  1. 1.

The DCC check starts when the interpreter proves that a goal G holds, by
invoking the predicate eval_dcc/2. If it succeeds, G is added to the model and
the evaluation continues. Otherwise, an inconsistency has been detected and
backtracking takes place.

  2. 2.

The current implementation of eval_dcc/2 only evaluates fully instantiated
goals. Therefore, if the G is not ground (line 4), eval_dcc/2 succeeds and the
evaluation continues. This is not a source of unsoundness, as in any case the
whole set of denials are checked before finally returning a model.

  3. 3.

Otherwise, dcc_rule(G,F_Atoms) (line 4) retrieves the DCC rules that involve
goal G. If there are no DCC rules, eval_dcc/2 succeeds.

  4. 4.

Since one atom in the rule (G) is to be added to the model, we need to ensure
that not all the rest of the atoms in the rule (F_Atoms) appear in the
candidate model In. In order not to instantiate the model, this is done by
checking with holds_dcc(F_Atoms,In) whether _all_ the atoms appear in In555For
builtins: checking that they succeed if evaluated in the environment of the
model. and then negating (by failure) the calling predicate.

Let us consider a program including the denial :-p(X), q(X,Y). When the
evaluation of p(1) succeeds, and before it is added to the tentative model,
the interpreter calls eval_dcc(p(1),[$\dots$]), where [$\dots$] is the current
tentative model. Since p(1) is ground, pr_dcc_rule(p(1),F_Atoms) retrieves in
F_Atoms a list of the atoms that cannot be true in the model --- in this case,
[q(1,Y)]. Then, the interpreter checks if the literals in [q(1,Y)] are true in
the current (tentative) model In. If that is the case,
holds_dcc([q(1,Y)],[$\dots$]) succeeds, eval_dcc/2 fails, and the interpreter
backtracks because the denial has been violated. Otherwise, the evaluation
continues. It is easy to see that this implementation of dynamic consistency
checking is _complete_ , i.e., we do not lose answers: since only ground goals
are checked, there is no risk of instantiating free variables which could
restrict degrees of freedom of the tentative model and therefore potentially
removing solutions. Furthermore, to ensure _correctness_ , we keep the non-
monotonic rule checking that is performed once the tentative model is found.
Note that non-ground goals are at the moment not subject to DCC rules, but
they may be involved in denials, and denials of atoms not needed to support
the query must be checked. DCC is also used during the execution of the
nmr_check predicate. As we mentioned before (item 3 in page 3), denials are
compiled into a synthesized goal, nmr_check, that is executed after a model
has been generated. During its execution, DCC rules are actively used to look
for atoms that are introduced and when an inconsistency is flagged, execution
fails and backtracks.

######  Example 3 (Cont. Example 2)

Let us consider the Hamiltonian program in Fig. 2. As explained above, the
compiler generates the DCC rules below. For this example each denial is
translated into two specialized rules.

⬇

dcc(vertex(U), [not reachable(U)]).

dcc(not reachable(U), [vertex(U)]).

dcc(chosen(U,W), [U \= V, chosen(V,W)]).

dcc(chosen(V,W), [chosen(U,W), U \= V]).

dcc(chosen(W,U), [U \= V, chosen(W,V)]).

dcc(chosen(W,V), [chosen(W,U), U \= V]).

By invoking scasp –dcc hamiltonian.pl graph_4.pl, s(CASP) evaluates the query
?-reachable(a) following a goal-directed strategy. Let us refer to the code in
Fig. 2 and the graph in Fig. 3 to explain how the evaluation with DCC takes
place:

  1. 1.

The query unifies with the clause in line 1 but the goal chosen(a,a) fails
because edge(a,a) does not exist.

  2. 2.

From the clause in line 2, chosen(b,a) is added to the tentative model,
because no DCC rule succeeds. The goal reachable(b) is then called.

  3. 3.

The goal reachable(b) unifies with the clause in line 1 and chosen(a,b) is
added, because it is consistent with chosen(b,a).

  4. 4.

As the query succeeds for the model \\{chosen(b,a), chosen(a,b), reachable(a),
reachable(b), $\dots$\

, s(CASP) invokes nmr_check. nmr_check executes checks for all the denials.
The code corresponding to line 6 is:

⬇

chk1 :- forall(U, not chk1_1(U))).

not chk1_1(U) :- not vertex(U).

not chk1_1(U) :- vertex(U), reachable(U).

i.e., all vertices (vertex(U)) must be reachable (reachable(U)). For vertices
U = a and U = b, reachable(a) and reachable(b) are already in the model, so
there is nothing to check. But for vertex U = c, reachable(c) is not in the
model and therefore reachable(c) has to be invoked while checking the denials.
From the clause in line 1, chosen(a,c) is selected to be added to the model,
but it is discarded by DCC, because of the DCC rule dcc(chosen(V,W),
[chosen(U,W), U \= V]), corresponding to the denial in line 7. Note that this
DCC rule is instantiated to dcc(chosen(a,c), [c \= b, chosen(a,b)] and the
literal chosen(a,b) is already in the model. The evaluation backtracks and
continues the search using another edge.

The denial in line 6 makes the interpreter to select edges to reach all
vertices. The interleaving of the dynamic consistency checking prunes the
search, which, as shown in Section 4, improves performance.

##  4 Evaluation

In this section we compare the performance of s(CASP) with and without DCC
using a macOS 11.5.2 Intel Core i7 at 2.6GHz. We use s(CASP) version
0.21.10.09 available at https://gitlab.software.imdea.org/ciao-lang/scasp and,
as mentioned before, all the benchmarks used or mentioned in this paper are
available at http://platon.etsii.urjc.es/~jarias/papers/dcc-padl21.

Table 1: Performance comparison: s(CASP) and s(CASP)+DCC. | Speedup | s(CASP) | s(CASP)+DCC
---|---|---|---
Hamiltonian (4 vertices) | 10.0 | 11.985 | 1.196
Hamiltonian (7 vertices) | 41.1 | 134.460 | 3.191
n_queens (n=4) | 4.3 | 8.147 | 1.910
n_queens (n=5) | 4.9 | 92.756 | 18.786
n_queens (n=6) | 90.8 | 1362.840 | 15.001
n_queens_attack (n=6) | 1.0 | 77.039 | 76.827

Table 1 shows the results of the performance comparison (in seconds), and the
speedup of s(CASP) with DCC w.r.t. s(CASP). First, we evaluate the Hamiltonian
path problem (Example 2) using the encoding in Fig. 2 (available at
hamiltonian.pl) and the graph with 4 vertices in Fig. 3 (available at
graph_4.pl). We see that s(CASP) with DCC obtains a speedup of 10.0$\times$.
When the size of the graph is increased by adding three vertices666The graph
with seven vertices is available at graph_7.pl. we obtain a speedup of
41.1$\times$. We also evaluated the performance of s(CASP) with DCC with the
well-known $n$-queens problem, using two different versions. These examples
are especially interesting, as they have no finite grounding and thus cannot
be run by other implementations of the stable model semantics. In particular,
the size of the board is not fixed by the programs and therefore the same code
can be used to find solutions to several board sizes. The first version,
n_queens (available in Appendix 0.A and at n_queens.pl), uses denials to
discard solutions where two queens attack each other. The speedup obtained by
s(CASP) with DCC ranges from 4.3$\times$ (for $n=4$) to 90.8$\times$ (for
$n=6$). The second version is the one presented in [12, Pag. 37] (available in
Appendix 0.B and at n_queens_attack.pl). In this case, the predicate attack/3
is used to check whether a candidate queen attacks any previously selected
queen. This version does not have denials, as the check is done as part of the
computation, and therefore DCC checks are not useful. Two interesting
conclusions can be drawn from the numbers in the table:

  * •

The execution time of n_queens_attack does not significantly change using or
not DCC, which supports our assumption that the overhead of using DCC checks
when they are not needed is negligible.

  * •

On the other hand, the DCC-enabled execution for the version with denials
(n_queens, column ‘‘s(CASP)+DCC’’) is faster than the version without denials
(n_queens_attack, column ‘‘s(CASP)’’) for a factor of 4.1$\times$. This can be
attributed to the runtime being sophisticated enough to perform checks earlier
and more efficiently than the hand-crafted code, even with the current,
preliminary implementation.

Table 2: Models generated and/or discarded: s(CASP) vs. s(CASP)+DCC.

|  #models returned |  | #models discarded |  #DCC detected
---|---|---|---|---
|  | s(CASP) | s(CASP)+DCC
Hamiltonian (4 vertices) | 3 |  | 7 | 7 | 52
Hamiltonian (7 vertices) | 1 |  | 13 | 13 | 34
n_queens (n=4) | 2 |  | 253 | 0 | 44
n_queens (n=5) | 10 |  | 3116 | 0 | 167
n_queens (n=6) | 4 |  | 46652 | 0 | 742

Table 4 sheds some additional light on the effectiveness of DCC. It contains,
for the same benchmarks as Table 1, how many models were returned, how many
candidate models were discarded by nmr_check after they were generated (column
‘‘#models discarded -- s(CASP)’’), how many (partial) candidate models were
discarded using DCCs (column ‘‘#models discarded -- s(CASP) + DCC’’) and how
many times the dynamic consistency checking detects an inconsistency and
backtracks (column ‘‘#DCC detected’’). Let us first focus on the n_queens
benchmark.777n_queens_attack does not have denials, hence we do not include it
in this table. As the size of the board grows, the number of models that are
completely generated and discarded by s(CASP) without using DCCs grows
exponentially; this is of course the reason why its execution time also
increases very quickly. If we look at the column ‘‘#models discarded --
s(CASP) + DCC’’ we see that, when DCC is active, none of final models is
discarded by nmr_check. That means that all models not consistent with the
denials have been removed early, while they were being built. We also see that
the number of times that DCC rules were activated is much smaller than the
number of times that nmr_check was executed \--- early pruning made it
possible to avoid attempting to generate many other candidate models. On top
of that, executing DCC rules is done directly in Prolog, while nmr_check is
executed using the s(CASP) metainterpreter, and the former is considerably
faster than the latter. This adds to the advantage of early pruning. The
Hamiltonian path benchmark is different and very interesting. The number of
models discarded by nmr_check is the same regardless of whether DCC is
activated or not. That means that the DCC could not detect inconsistencies in
candidate models. In this case the advantage of using DCC comes from applying
it when nmr_check is invoked to ensure that the final model is consistent with
the denials. nmr_check is executed as a piece of (synthesized) code by the
metainterpreter. The denials in the Hamiltonian path not only check, but also
generate new atoms which are checked by the DCC. This accelerates the
execution of nmr_check, making it fail earlier, and it is the cause of the
speedup of the Hamiltonian path benchmark.

##  5 Conclusions

In this paper, we have reported on a preliminary design and implementation of
Dynamic Consistency Checking (DCC), a technique that anticipates the
consistency evaluation of tentative models in s(CASP), a goal-directed
(predicate) Constraint Answer Set Programming. This technique translates the
denials to check them as early as possible rather than when a full model is
found for a given query. Its ability to detect inconsistencies before a
literal is added to the tentative model greatly increases the performance.
with respect with executions without DCC. Early denial checking can also beat
programs that use auxiliary predicates explicitly called from the user code to
check for inconsistencies. The current DCC implementation can still be
improved, in particular to properly handle constraints by reducing the domain
of constrained variables: checking denials using literals with constrained
variables has to keep track of the domains of the variables, while avoiding
introducing non-determinism when conflicting values are removed from the
domain of the variables.

## References

  * [1] Arias, J., Chen, Z., Carro, M., Gupta, G.: Modeling and Reasoning in Event Calculus Using Goal-Directed Constraint Answer Set Programming. In: Pre-Proc. of the 29th Int’l. Symposium on Logic-based Program Synthesis and Transformation (September 2019)

* [2] Arias, J., Carro, M., Chen, Z., Gupta, G.: Justifications for goal-directed constraint answer set programming. In: Proceedings 36th International Conference on Logic Programming (Technical Communications). EPTCS, vol. 325, pp. 59--72. Open Publishing Association (2020). https://doi.org/10.4204/EPTCS.325.12
* [3] Arias, J., Carro, M., Chen, Z., Gupta, G.: Modeling and Reasoning in Event Calculus using Goal-Directed Constraint Answer Set Programming. CoRR abs/2106.14566 (2021), https://arxiv.org/abs/2106.14566
* [4] Arias, J., Carro, M., Salazar, E., Marple, K., Gupta, G.: Constraint Answer Set Programming without Grounding. Theory and Practice of Logic Programming 18(3-4), 337--354 (2018). https://doi.org/10.1017/S1471068418000285
* [5] Arias, J., Moreno-Rebato, M., Rodriguez-García, J.A., Ossowski, S.: Modeling Administrative Discretion Using Goal-Directed Answer Set Programming. In: Advances in Artificial Intelligence, CAEPIA 20/21. pp. 258--267. Springer International Publishing, Cham (2021). https://doi.org/10.1007/978-3-030-85713-4_25
* [6] Basu, K., Varanasi, S., Shakerin, F., Arias, J., Gupta, G.: Knowledge-driven Natural Language Understanding of English Text and its Applications. AAAI’21 (2021)
* [7] Basu, K., Wang, H., Dominguez, N., Li, X., Li, F., Varanasi, S.C., Gupta, G.: CASPR: A Commonsense Reasoning-based Conversational Socialbot. In: 4th Proceedings of Alexa Prize (Alexa Prize 2021). (2021)
* [8] Chen, Z., Marple, K., Salazar, E., Gupta, G., Tamil, L.: A Physician Advisory System for Chronic Heart Failure Management Based on Knowledge Patterns. Theory and Practice of Logic Programming 16(5-6), 604--618 (2016). https://doi.org/10.1017/S1471068416000429
* [9] Dovier, A., Pontelli, E., Rossi, G.: A Necessary Condition for Constructive Negation in Constraint Logic Programming. Information Processing Letters 74(3-4), 147--156 (2000)
* [10] Gelfond, M., Lifschitz, V.: The Stable Model Semantics for Logic Programming. In: 5th International Conference on Logic Programming. pp. 1070--1080 (1988), http://www.cse.unsw.edu.au/~cs4415/2010/resources/stable.pdf
* [11] Hall, B., Varanasi, S.C., Fiedor, J., Arias, J., Basu, K., Li, F., Bhatt, D., Driscoll, K., Salazar, E., Gupta, G.: Knowledge-Assisted Reasoning of Model-Augmented System Requirements with Event Calculus and Goal-Directed Answer Set Programming. In: Proc. 8th Workshop on Horn Clause Verification and Synthesis (2021)
* [12] Marple, K., Bansal, A., Min, R., Gupta, G.: Goal-Directed Execution of Answer Set Programs. In: Schreye, D.D., Janssens, G., King, A. (eds.) Principles and Practice of Declarative Programming, PPDP’12, Leuven, Belgium - September 19 - 21, 2012. pp. 35--44. ACM (2012). https://doi.org/10.1145/2370776.2370782
* [13] Marple, K., Gupta, G.: Dynamic Consistency Checking in Goal-Directed Answer Set Programming. Theory and Practice of Loging Programming 14(4-5), 415--427 (2014). https://doi.org/10.1017/S1471068414000118
* [14] Marple, K., Salazar, E., Gupta, G.: Computing Stable Models of Normal Logic Programs Without Grounding. arXiv 1709.00501 (2017), http://arxiv.org/abs/1709.00501
* [15] Marriott, K., Stuckey, P.J.: Programming with Constraints: an Introduction. MIT Press (1998)
* [16] Mellarkod, V.S., Gelfond, M., Zhang, Y.: Integrating Answer Set Programming and Constraint Logic Programming. Tech. rep., Texas Tech University (October 2008), this is a long version of [17], available at https://www.depts.ttu.edu/cs/research/documents/46.pdf
* [17] Mellarkod, V.S., Gelfond, M., Zhang, Y.: Integrating Answer Set Programming and Constraint Logic Programming. Annals of Mathematics and Artificial Intelligence 53(1-4), 251--287 (2008)
* [18] Morris, J.: Constraint answer set programming as a tool to improve legislative drafting: a rules as code experiment. In: ICAIL. pp. 262--263. ACM (2021)
* [19] Pereira, L.M., Aparício, J.N.: Relevant counterfactuals. In: EPIA 89, 4th Portuguese Conference on Artificial Intelligence, Lisbon, Portugal, September 26-29, 1989, Proceedings. pp. 107--118 (1989). https://doi.org/10.1007/3-540-51665-4_78
* [20] Shakerin, F., Gupta, G.: Induction of Non-Monotonic Logic Programs to Explain Boosted Tree Models Using LIME. In: AAAI 2019. pp. 3052--3059 (January - February 2019). https://doi.org/10.1609/aaai.v33i01.33013052
* [21] Stuckey, P.: Constructive negation for constraint logic programming. In: Proc. LICS’91. pp. 328--339 (1991)
* [22] Varanasi, S.C., Salazar, E., Mittal, N., Gupta, G.: Synthesizing Imperative Code from Answer Set Programming Specifications. In: LOPSTR. Lecture Notes in Computer Science, vol. 12042, pp. 75--89. Springer (2019). https://doi.org/10.1007/978-3-030-45260-5_5

##  Appendix 0.A Encoding of n_queens.pl

⬇

% N-queens program.

nqueens(N, Q) :-

nqueens_(N, N, [], Q).

% Pick queens one at a time.

nqueens_(X, N, Qi, Qo) :-

X > 0,

pickqueen(X, Y, N),

X1 is X - 1,

nqueens_(X1, N, [queen(X, Y) | Qi], Qo).

nqueens_(0, _, Q, Q).

% pick a queen for row X.

pickqueen(X, Y, Y) :-

Y > 0,

queen(X, Y).

pickqueen(X, Y, N) :-

N > 1,

N1 is N - 1,

pickqueen(X, Y, N1).

queen(X, Y) :- not neg_q(X, Y).

neg_q(X, Y) :- not queen(X, Y).

#show queen/2.

% Test

:- queen(I,J1), queen(I,J2), J1 \= J2.

:- queen(I1,J), queen(I2,J), I1 \= I2.

:- queen(I,J), queen(II,JJ), I\=II, J\=JJ, T1 is I+J, T2 is II+JJ, T1=T2.

:- queen(I,J), queen(II,JJ), I\=II, J\=JJ, T1 is I-J, T2 is II-JJ, T1=T2.

##  Appendix 0.B Encoding of n_queens_attack.pl

⬇

nqueens(N, Q) :-

nqueens_(N, N, [], Q).

% Pick queens one at a time and test against all previous queens.

nqueens_(X, N, Qi, Qo) :-

X > 0,

pickqueen(X, Y, N),

not attack(X, Y, Qi),

X1 is X - 1,

nqueens_(X1, N, [q(X, Y) | Qi], Qo).

nqueens_(0, _, Q, Q).

% pick a queen for row X.

pickqueen(X, Y, Y) :-

Y > 0,

q(X, Y).

pickqueen(X, Y, N) :-

N > 1,

N1 is N - 1,

pickqueen(X, Y, N1).

% check if a queen can attack any previously selected queen.

attack(X, _, [q(X, _) | _]). % same row

attack(_, Y, [q(_, Y) | _]). % same col

attack(X, Y, [q(X2, Y2) | _]) :- % same diagonal 1

T1 is X + Y, T2 is X2 + Y2, T1 = T2.

attack(X, Y, [q(X2, Y2) | _]) :- % same diagonal 2

T1 is X - Y, T2 is X2 - Y2, T1 = T2.

attack(X, Y, [_ | T]) :-

attack(X, Y, T).

q(X, Y) :- not neg_q(X, Y).

neg_q(X, Y) :- not q(X, Y).

#show q/2.