LASCO is a tool that allows to compute inductive solutions of Learning from Answer Sets (LAS) tasks by genereating an ASP encoding that can be processed by state-of-the-art ASP solvers such as Clingo or DLV.
Full details are provided in my Master's Thesis.
Precompiled binaries are available in the GitHub Releases:
The LASCO binary depends on external ASP grounders and solvers for full functionality:
- gringo is required to solve tasks involving variables (i.e., non-ground programs).
- clingo or dlv must be installed if you want to solve the compiled encoding directly using the
--solveoption.
Note: Recommended versions of these tools are as follows. gringo 5.7.1; clingo 5.7.1; dlv 2.1.2
Note: If no solver is specified, LASCO will only produce the ASP encoding without solving it.
To build LASCO from source, you need:
- Clone the repository:
git clone https://github.com/robyBorelli/lasco.git
cd lasco- Build using Cabal:
cd code
cabal build-
The binary will be located inside
dist-newstyle/build/.../lasco. -
Test the compiled binary:
cabal run lasco -- --helpUsage: lasco [options]
Available options:
-i,--input IFILE Specifies the input file containing the learning task
to solve.
-o,--output OFILE Specifies the output file which will contain the
output encoding.
-e,--encoder ENCODER Specifies the encoding type:
- 'exponential'
- 'disjunctive' (default)
--solve SOLVER Solves the encoding using:
- 'clingo'
- 'dlv'
--solve-mode MODE Solving mode:
- 'first', 'all', or 'optimum'
- an integer (e.g. 3) for number of solutions
-t, --parallel-mode THREADS Specifies the number of threads to use with the SOLVER.
Works only with 'clingo' SOLVER. (default: 1)
-v,--verbose Prints intermediate steps and debug information.
--enable-comments Enables comments in the generated encoding.
--show-hypos [i1,i2,...] Prints hypotheses of specified indexes and exits.
--version Prints program version.
-h,--help Show this help text.
# Basic usage
lasco --input examples/ex1_normal_rules.las
# Solves at optimum using clingo
lasco --input examples/ex1_normal_rules.las --solve clingo --solve-mode optimum
# Shows the first two rules in the hypothesis space
lasco --input examples/ex1_normal_rules.las --show-hypos [1,2]
# Basic usage with exponential encoder
lasco --input examples/ex1_normal_rules.las --encoder exponentialInput files must use Answer Set Programming (ASP) syntax with some extensions to define the hypothesis and examples.
The background is a set of standard ASP rules, including:
- Facts (e.g.,
edge(a,b).) - Normal rules (e.g.,
reachable(X,Y) :- edge(X,Y).) - Constraints (e.g.,
:- not reachable(a,c).) - Arithmetic (e.g.,
X = Y + 1.) - Comparison predicates (e.g.,
X < Y.)
Syntax rules:
- Variables start with an uppercase letter:
X,Node,Time. - Constants start with a lowercase letter:
a,node1,zero. - Every word containing
LASCOorlascoas a substring, is a reserved word.
A rule in the hypothesis space is defined as:
weight ~ rule.where:
weightis a positive integer.ruleis an ASP rule.
A standard example is defined as:
#type(inclusion_set, exclusion_set).where:
typeis eitherpos(positive example) orneg(negative example).inclusion_setis a set of ground atoms. (e.g.,{p, q, reachable(a), edge(a,b)})exclusion_setis a set of ground atoms.
A context example is defined as:
#type(inclusion_set, exclusion_set, {context}).where:
contextis an ASP program.
p :- not q.
1 ~ q.
2 ~ q :- not p.
#pos({p},{q}).
#neg({q},{p}).