alpha-asp / alpha

A lazy-grounding Answer-Set Programming system

Alpha

Alpha is an Answer Set Programming (ASP) system: It reads a logic program (a set of logical rules) and computes the corresponding answer sets. ASP falls into the category of declarative and logic programming. Its applications are solving combinatorial problems, but it also is a good tool for reasoning in the context of knowledge-representation and databases.

Alpha is the successor of OMiGA and currently in development. In contrast to many other ASP systems, Alpha implements a lazy-grounding approach in hopes of overcoming memory constraints when working with large input.

Alpha is not the fastest system available, since its goal is not to be the fastest system with current technology but to explore new technologies rapidly. Those technologies, like lazy-grounding, allow Alpha to succeed where other ASP systems fail completely. The project deliberately chooses to trade shorter execution times (which would be possible by using unmanaged runtimes, e.g. C/C++, and low-level optimization) for a more straight forward system design and possibilities to interface with the ecosystem built around the Java Virtual Machine.

Getting Started

Download a current version of the distribution jar (alpha-cli-app-${version}-bundled.jar) from Releases and save it as alpha.jar for convenience.

Running Alpha is as simple as running any other JAR:

$ java -jar alpha.jar

Example Usage

Solve 3-colorability for some benchmarking instance and filter for color predicates:

$ java -jar alpha.jar -i benchmarks/omiga/omiga-testcases/3col/3col-10-18.txt -fblue -fred -fgreen

Note that in this example the path to the input file is relative to the root of this repository. If you have not checked out the repository, you can just download the example file from GitHub.

A coder's guide to answer set programming provides a short and high-level tutorial on Answer Set Programming.

Building

Alpha uses the Gradle build automation system. Executing

$ ./gradlew build

will automatically fetch all dependencies (declared in build.gradle.kts) and compile the project.

Artifacts generated will be placed in the build/ subfolder of the respective module. Most notably you'll find files ready for distribution at alpha-cli-app/build/distributions/. They contain archives which in turn contain a bin/ directory with scripts to run Alpha on Linux and Windows.

If you want to generate a JAR file to be run standalone, execute

$ ./gradlew alpha-cli-app:bundledJar

and pick up alpha-cli-app/build/libs/alpha-cli-app-${version}-bundled.jar.

A Note on IDEs

We have contributors using IntelliJ IDEA as well as Eclipse IDE. However, we decided to not check in files related to project configuration. For both tools, standard features to "import" the project based on its Gradle build configuration are available, and they will infer sane defaults. If you run into trouble feel free to file an issue.

Suggested Reading

Beginners' Tutorials

• A coder's guide to answer set programming

Theoretical Background and Language Specification

• Answer Set Programming: A Primer
• ASP-Core-2 Input Language Format
• Conflict-Driven Answer Set Solving: From Theory to Practice
• Learning Non-Ground Rules for Answer-Set Solving

Research Papers on Alpha

Peer-reviewed publications part of journals, conferences and workshops:

2021

• Solving Configuration Problems with ASP and Declarative Domain-Specific Heuristics

2020

• Conflict Generalisation in ASP: Learning Correct and Effective Non-Ground Constraints
• Advancing Lazy-Grounding ASP Solving Techniques - Restarts, Phase Saving, Heuristics, and More

2019

• Exploiting Partial Knowledge in Declarative Domain-Specific Heuristics for ASP (supplementary material)
• Degrees of Laziness in Grounding: Effects of Lazy-Grounding Strategies on ASP Solving (preprint | supplementary material)

2018

• Exploiting Justifications for Lazy Grounding of Answer Set Programs
• Lazy Grounding for Dynamic Configuration: Efficient Large-Scale (Re)Configuration of Cyber-Physical Systems with ASP

2017

• Blending Lazy-Grounding and CDNL Search for Answer-Set Solving (preprint)
• Introducing Heuristics for Lazy-Grounding ASP Solving
• Lazy-Grounding for Answer Set Programs with External Source Access
• Techniques for Efficient Lazy-Grounding ASP Solving (technical report)

Others (e.g. non-peer-reviewed publications, less formal articles, newsletters):

• The Alpha Solver for Lazy-Grounding Answer-Set Programming

Similar Work

• Smodels, a solver usually used in conjunction with lparse.
• DLV
• ASPeRiX, a solver that implements grounding-on-the-fly.

alpha's Issues

Malformed input sometimes ignored.

For the following ASP program, Alpha continues solving despite the parsing error (notice the missing . after r(Y) signifying the end of the rule):
p(X,Y) :- q(X), r(Y) p(a). q(b).

Expected behaviour: malformed input causes Alpha to stop and report the error.

Number of conflicts reported does not include backtracks

DefaultSolver reports number of conflicts encountered during search in a message like "512 decisions done with 237 conflicts" (introduced in 7f217f8).
However, this number corresponds only to the number of back jumps, while DefaultSolver also does back tracks in certain cases.
DefaultSolver shall report the total number of conflicts as well as the number of backjumps and backtracks.

Represent builtin-atom with its own class.

Currently, the builtin atoms (according to the standard) are internally represented by an ExternalAtom. I think it would be better to represent them by their own atom class, e.g. BuiltinAtom or ComparisonAtom. There are two reasons: first, it feels more natural than representing them with ExternalAtom, and second, these builtin atoms can bind variables (according to the standard) but it depends on the actual instance of the atom. If the comparison operator is = and on one side there is a single variable, then this variable is binding. So, X = Y + 3 would have X binding and Y non-binding while for X +1 = Y it would be the other way round. I think this behaviour cannot be modelled with ExternalAtom in a nice way.

Are there any arguments against introducing this new atom class?

Move Alpha to a new non-personal namespace

As we now have approx. four contributors, I think that Alpha has grown beyond the scope of @AntoniusW. I suggest creating a new organization and moving Alpha over. All contributors to the project should be members of that organization and given push access to the repository.

Native lists via external atoms.

Lists are very convenient constructs in logic programming and some ASP solvers support them natively. Since our constants can be actual Java objects, it might be easy to allow list construction, membership testing, appending elements, etc. via external atoms that directly work on Java lists.

In a later iteration, the usual list constructs may be directly supported and internally rewritten into the respective external atoms.

Implement toString() in Program

Program shall provide a toString() implementation which produces a string containing first all the program's facts and then its other rules, separated by System.lineSeparator().

Too many backtracks counted in solver statistics

We report numbers of backtracks and backjumps in solver statistics (cf. #100). The problem is that the number of backtracks also increases when a backjump is made, because DefaultSolver#backjump(int) calls backtrackFast() internally. In my opinion, backtracks should not be counted during a backjump. @AntoniusW @lorenzleutgeb do you agree, or am I overlooking something? Should there be any counting-related difference between fast and slow backtracks?

API and Modularization

I have been thinking about implementing an API for Alpha for some time. With the introduction of the Alpha class that acts as a facade for the whole system I made a first step. There's still a long way to go if the API should be taken seriously by application developers.

Prototyping Applications

I identified at least two applications that might use the API and act as guides in the API design:

1. Angry-Alpha (first I have to wrap my head around higher order predicates and eliminate them)
2. Wolpertinger (paper; the interesting part where it shells out to clingo is here; pointed out to me by @lukeswissman)

Modularization

In order to provide a smooth API, I think that we should modularize Alpha as follows:

• alpha-core: Contains grounder(s) and solver(s), but no main entry point. Depends on alpha-api.
• alpha-api: Contains glue code that allows instantiation of the Alpha system with given parameters, run it, and collect solutions. This includes a specification of all I/O, so we need Programs to go in and AnswerSets to go out, these would have to move to some package ac.at.kt.tuwien.alpha.api or similar that resides in this module. Depends on alpha-core.
• alpha-cli: Contains a main entry point that fiddles with arguments in order to run Alpha via alpha-api.

Further down the line we might want to extend this scheme, for example by writing a wrapper that integrates Alpha with Clojure. Such a wrapper would then depend on alpha-api as well.

While it might seem strange that these modules all depend on each other in a trivial fashion, we would have the following side-effects:

• Any option that should be exposed to the CLI must also be exposed through the API. No dirty hacks to circumvent it.
• In some bright future, one might generalize the alpha-api package in a way that it is suitable for a large range of ASP systems. Instead of alpha-core one could then depend on evenbettersolver which implements everything declared in alpha-api. It is conceivable to wrap clasp, so applications could switch out implementations.

Related Projects

• In Java:
  • asp4j uses Annotations
  • net.sf.tweety.lp.asp.solver.AspInterface declares an interface for solvers
  • lukeswissman/jclingo
• Jess which lead to JSR94
• DLV Java wrapper
• https://github.com/gaste/gringo-wrapper
• https://github.com/phohenecker/asp-wrapper
• https://github.com/egnwd/pingo
• https://github.com/Aluriak/clyngor
• http://cmt.math.unipr.it/jsetl.html
• JASP

Course of Action

• Evaluate whether asp4j can be re-used/forked/adopted.
• Modularize Alpha
• Consume the API from some applications, to see whether the API feels nice

Do nogoods really need IDs?

Follow up from #86

Integrate with JPA

The Java Persistence API aims "to provide an object/relational mapping facility for the Java application developer using a Java domain model to manage a relational database." It is the canonical API that ORMs in the Java world implement. Most prominently Hibernate.

I think it would be desirable to integrate with JPA, because it is already in place in many business applications. For business applications it is common to have a domain model that directly supports JPA, so the entities that are juggled in those applications could then be used very naturally with Alpha. Thus it would make the use of Alpha easier in a commercial setting.

In a minimal integration, Alpha should be able to read facts using JPA. A good entry point would be EntityManager. Building up on that, Alpha might also use more fine-grained queries instead of wading through all the entities itself.

Note that there is DLVDB and some hints in the DLV User Manual, Chapter 8. ODBC interface (#import/#export Built-ins). With JPA we would go for a more high-level interface.

Constants whose values can be assigned via the command line

It would be nice if Alpha supported constants whose values are assigned via the command line (as does clingo).
Then, we could write programs like the following:
time(0..maxtime).
The value of maxtime could be passed from the outside:
java -jar Alpha.jar -c maxtime=100

Currently, we have to use programs like the following:
time(0..T) :- maxtime(T).
Then the value for maxtime is included in the problem instance:
maxtime(100).
Technically, this even makes it necessary to forbid the existence of two different values:
:- maxtime(T1), maxtime(T2), T1<T2.

NullPointerException when trying to solve Hanoi Tower instance 1 with random Naive

In d1e9b64, test cases for four different instances of the Tower of Hanoi problem are added to the project.
By this, a bug can be discovered that causes a NullPointerException to be thrown by at.ac.tuwien.kr.alpha.solver.BasicNoGoodStore.ensureWatchInvariantAfterAssignAtLowerDL(int, ThriceTruth) when the random Naive heuristic is employed:

java.lang.NullPointerException
at at.ac.tuwien.kr.alpha.solver.BasicNoGoodStore.ensureWatchInvariantAfterAssignAtLowerDL(BasicNoGoodStore.java:453)
at at.ac.tuwien.kr.alpha.solver.BasicNoGoodStore.propagate(BasicNoGoodStore.java:635)
at at.ac.tuwien.kr.alpha.solver.DefaultSolver.tryAdvance(DefaultSolver.java:104)
at at.ac.tuwien.kr.alpha.solver.AbstractSolver$1.tryAdvance(AbstractSolver.java:31)

Enable Arithmetics

In order to realize arithmetics as per the standard, the following is required:

• The parser needs to take operator precedence into account (* and / before + and -).
• Evaluation of all ground arithmetic terms occurring anywhere as a subterm ( a fact p(f(g(3+4,a)). must yield p(f(g(7,a)) in all answer sets).
• Ignoring instances of undefined arithmetics ( p(3+a). and p(3/0). are simply ignored, likewise a constraint :- not p(3/0). is also ignored).

Simplify input in preprocessor

State-of-the-art ASP systems employ sophisticated preprocessing to simplify input programs, thereby improving solving performance. Probably Alpha could benefit from such techniques as well.

Example reference:
Gebser, M., Kaufmann, B., Neumann, A., & Schaub, T. (2008, June). Advanced Preprocessing for Answer Set Solving. In ECAI (Vol. 178, pp. 15-19).

RuntimeException when trying to solve Hanoi Tower instance 1 with deterministic BerkMin

In d1e9b64, test cases for four different instances of the Tower of Hanoi problem are added to the project.
By this, a bug can be discovered that causes a RuntimeException to be thrown by at.ac.tuwien.kr.alpha.solver.BasicNoGoodStore.propagate() when the deterministic BerkMin heuristic is employed:

java.lang.RuntimeException: Assignment entry is for current decision level but marked as reassign at lower one. Should not happen.
at at.ac.tuwien.kr.alpha.solver.BasicNoGoodStore.propagate(BasicNoGoodStore.java:632)
at at.ac.tuwien.kr.alpha.solver.DefaultSolver.tryAdvance(DefaultSolver.java:104)
at at.ac.tuwien.kr.alpha.solver.AbstractSolver$1.tryAdvance(AbstractSolver.java:31)

Lift restrictions on external atoms.

Currently, external atoms have the following limitations:

• 1. An external must have some input and an external like &getFromExtern[](X) is not possible.
• 2. An rule comprised of only an external whose input consists of constants only will yield wrong answer sets (it is never evaluated). A rule like p(X) :- &getFromExtern[0](X). will not be evaluated correctly.
• 3. An external cannot have non-variable output like in &getFromExtern[0](3).

The following code for testing may be easily adapted to showcase each of the restrictions.

public static Set<List<ConstantTerm<Integer>>> returnTestNodes(int drop) {
	Set<List<ConstantTerm<Integer>>> ret = new LinkedHashSet<>();
	for (int i = 0; i < 5; i++) {
		List<ConstantTerm<Integer>> termList = new LinkedList<>();
		termList.add(ConstantTerm.getInstance(i + 3));
		ret.add(termList);
	}
	return ret;
}

@Test
public void externalAtomOutput() throws Exception {
	Alpha system = new Alpha();
	system.registerBinding(this.getClass().getMethod("returnTestNodes", int.class));

	Set<AnswerSet> actual = system.solve("p(0). node(X) :- p(Y), &returnTestNodes[Y](X).").collect(Collectors.toSet());
	Set<AnswerSet> expected = AnswerSetsParser.parse("{ p(0), node(3), node(4), node(5), node(6), node(7) }");
	assertEquals(expected, actual);
}

Naming: "choice" vs. "guess"

I am not aware of any distinction between "choice" and "guess" in our code base and it seems to me that we are using these words interchangeably.

For example, we have methods that are called guess but a ChoiceManager, "choice points" and a "choice stack".

In order to increase readability/comprehensibility of our code base, I'd like to settle this by preferring one concept over the other.

My personal preference is "guess" ... I like it more because it expresses that we really don't know what the solution(s) will be. Heuristics are also "just" guessing strategies IMO.

NonGroundRule.toString() returns erroneous string

For example, a(X) :- b1(X), b2(X), not c1(X), not c2(X). becomes :- a(X) b1(X), b2(X), not c1(X), not c2(X).

Nogoods: Fix index of head

I recently realized that we (nearly?) always use NoGood.headFirst whenever we create nogoods with head. We could simplify our nogoods such that the head (if present) is always at a fixed index. This would make some things easier (for example there is a TODO in DependencyDrivenHeuristic asking for that).

But it might make other things harder...

Currently, nogoods are sorted, so it is not guaranteed that the head will remain at index 0.

👍 or 👎 ?

NoGood Forgetting

Alpha uses a CDNL-based solving component which learns new nogoods after running into conflicts. Over time, the number of nogoods becomes very large and many of the learned ones are not helpful to later search. The search almost grinds to a halt due to the massive number of superflous nogoods, which need to be treated during propagation. SAT solvers and other APS solvers therefore implement some form of nogood forgetting in order to speed-up the search and only keep those nogoods that are useful. There is a variety of literature on this topic and Alpha needs some form of nogood forgetting in order to solve the harder instances from the ASP competition.

False negatives by ChoiceManager#isAtomChoice

As demonstrated by at.ac.tuwien.kr.alpha.solver.ChoiceManagerTests.testIsAtomChoice() in 27bb785, ChoiceManager.isAtomChoice(int) returns false in cases where it should return true (at least to my understanding).

Command-line interface should be able to accept multiple input files

In ASP it is common to provide problem encoding and instance in two separate files. Therefore, Alpha should be able to accept several input files via the -i command-line argument.

Investigate whether we can make logging faster

I just read this article and ended up asking myself whether we are already using Log4j 2 or not. It's not as simple as checking our dependencies because we use SLF4J as a logging facade.

I'll find out whether we already have Log4j 2. If not, I'll add it (even if that means ripping out SLF4J). If yes, I'll make sure it does the async append magic for us.

Then compare running times with logging enabled.

NullPointerException when trying to solve Hanoi Tower with NaiveSolver

In d1e9b64, test cases for four different instances of the Tower of Hanoi problem are added to the project.
By this, a bug can be discovered that causes a NullPointerException to be thrown by at.ac.tuwien.kr.alpha.solver.NaiveSolver.choicesLeft() when NaiveSolver is employed:

java.lang.NullPointerException
at at.ac.tuwien.kr.alpha.solver.NaiveSolver.choicesLeft(NaiveSolver.java:227)
at at.ac.tuwien.kr.alpha.solver.NaiveSolver.tryAdvance(NaiveSolver.java:110)
at at.ac.tuwien.kr.alpha.solver.AbstractSolver$1.tryAdvance(AbstractSolver.java:31)

This behaviour can be observed with HanoiTowerTest.testInstance1() and HanoiTowerTest.testInstance2().

Resolve variable-binding dependencies in rules.

In order to allow that X = 1 + Y is binding for X and other issues with variable binding, the dependencies of variable bindings in rules must be resolved. These dependencies dictate possible evaluation orders of the lazy grounding (i.e., variables restrict the join order of atoms).

We also have a kind of rules that lack an ordinary positive atom with variables to start the usual grounding (e.g., fully ground rules, rules with only interval terms or externals with output variables). Those rules must be treated once, e.g., directly at the beginning, similar to facts.

Investigate Rule Decomposition

Basic idea, informally:

• The more non-ground rules in the non-ground program, the bigger the ground program.
• The "larger" a non-ground rule, the bigger it's impact on the size of the ground program.
• We want smaller ground programs.
• Therefore it makes sense to split large non-ground rules into fewer smaller ones.

There is lpopt which implements this kind of rewriting.

What can we learn from that to make Alpha better? Would it make sense to implement this rewriting into Alpha's lazy grounding?

Treatment of Optimize Statements

ASP-Core-2 talks about optimize statements.

At some point, Alpha should be able to support them. We're looking at a lot of work:

• Research how other (ASP) solvers implement optimization.
  • Multi-Criteria Optimization in Answer Set Programming (Potassco Team)
  • Multi-Criteria Optimization in ASP and its Application to Linux Package Configuration (slides) (Potassco Team)
  • The Disjunctive Datalog System DLV (talks about weak constraints)
  • Rewriting Optimization Statements in Answer-Set Programs
• Design an optimization algorithm that integrates well with Alpha.
  • For a start, we probably should do Branch-and-Bound.
  • We would probably get new heuristics for choices (based on optimize statements) that need to be weighted against the heuristics that are already in place.
• Design new types and data structures needed to implement optimization.
  • We need to carry around upper and lower bounds for BnB, and while solving keep the best solution(s) in memory so we can present it/them once we are sure that there is no better one.
• Add parser support.
  • Should we split optimize statements into weak constraints as suggested in ASP-Core-2, or should we keep them as a whole?
• Write tests that narrow down the behavior of optimization.
• Integrate optimization into solving.

RuntimeException "Watch invariant violated" produced by HeadBodyTransformationTests

The following unit tests in HeadBodyTransformationTests (available on the benchmarking-heads_bodies branch) produce RuntimeException with the message "Watch invariant violated! Should not happen":

• testProgramA_N2
• testProgramA_N4
• testProgramA_N8

Stack trace:

java.lang.RuntimeException: Watch invariant violated! Should not happen.
at at.ac.tuwien.kr.alpha.Util.oops(Util.java:84)
at at.ac.tuwien.kr.alpha.solver.NoGoodStoreAlphaRoaming$WatchedNoGoodsChecker.checkOrdinaryWatchesInvariant(NoGoodStoreAlphaRoaming.java:724)
at at.ac.tuwien.kr.alpha.solver.NoGoodStoreAlphaRoaming$WatchedNoGoodsChecker.doWatchesCheck(NoGoodStoreAlphaRoaming.java:655)
at at.ac.tuwien.kr.alpha.solver.NoGoodStoreAlphaRoaming.backtrack(NoGoodStoreAlphaRoaming.java:83)
at at.ac.tuwien.kr.alpha.solver.ChoiceManager.backtrack(ChoiceManager.java:266)
at at.ac.tuwien.kr.alpha.solver.ChoiceManager.backtrackFast(ChoiceManager.java:232)
at at.ac.tuwien.kr.alpha.solver.ChoiceManager.backjump(ChoiceManager.java:220)
at at.ac.tuwien.kr.alpha.solver.DefaultSolver.learnBackjumpAddFromConflict(DefaultSolver.java:203)
at at.ac.tuwien.kr.alpha.solver.DefaultSolver.tryAdvance(DefaultSolver.java:130)
at at.ac.tuwien.kr.alpha.solver.AbstractSolver$1.tryAdvance(AbstractSolver.java:31)
at java.util.stream.ReferencePipeline.forEachWithCancel(ReferencePipeline.java:126)
at java.util.stream.AbstractPipeline.copyIntoWithCancel(AbstractPipeline.java:498)
at java.util.stream.AbstractPipeline.copyInto(AbstractPipeline.java:485)
at java.util.stream.AbstractPipeline.wrapAndCopyInto(AbstractPipeline.java:471)
at java.util.stream.FindOps$FindOp.evaluateSequential(FindOps.java:152)
at java.util.stream.AbstractPipeline.evaluate(AbstractPipeline.java:234)
at java.util.stream.ReferencePipeline.findFirst(ReferencePipeline.java:464)
at at.ac.tuwien.kr.alpha.solver.HeadBodyTransformationTests.test(HeadBodyTransformationTests.java:165)
at at.ac.tuwien.kr.alpha.solver.HeadBodyTransformationTests.testProgramA_N8(HeadBodyTransformationTests.java:131)
at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
at java.lang.reflect.Method.invoke(Method.java:498)
at org.junit.runners.model.FrameworkMethod$1.runReflectiveCall(FrameworkMethod.java:50)
at org.junit.internal.runners.model.ReflectiveCallable.run(ReflectiveCallable.java:12)
at org.junit.runners.model.FrameworkMethod.invokeExplosively(FrameworkMethod.java:47)
at org.junit.internal.runners.statements.InvokeMethod.evaluate(InvokeMethod.java:17)
at org.junit.internal.runners.statements.FailOnTimeout$CallableStatement.call(FailOnTimeout.java:298)
at org.junit.internal.runners.statements.FailOnTimeout$CallableStatement.call(FailOnTimeout.java:292)
at java.util.concurrent.FutureTask.run(FutureTask.java:266)
at java.lang.Thread.run(Thread.java:745)

Wrong answer sets for to example programs

Alpha returns wrong answer sets for the following two programs.

node(a).
node(b).

in(X) :- not out(X), node(X).
out(X) :- not in(X), node(X).

pair(X,Y) :- in(X), in(Y).

The answer sets returned for the program are:

{ node(a), node(b), in(b), in(a), pair(b, b), pair(a, a), pair(b, a) }
{ out(a), node(a), node(b), in(b), pair(b, b) }
{ out(b), node(a), node(b), in(a), pair(a, a) }
{ out(b), out(a), node(a), node(b) }

The atom pair(a,b)is not derived by the last rule, only the inverse atom pair(b,a) is contained in the first answer set. The correct answer sets would be:

{ node(a), node(b), in(b), in(a), pair(b, b), pair(a, a), pair(b, a), pair(a, b) }
{ out(a), node(a), node(b), in(b), pair(b, b) }
{ out(b), node(a), node(b), in(a), pair(a, a) }
{ out(b), out(a), node(a), node(b) }

A variant of the first program where the error occurs due to a missing constraint is the following:

node(a).
node(b).

edge(b,a).

in(X) :- not out(X), node(X).
out(X) :- not in(X), node(X).

:- in(X), in(Y), edge(X,Y).

The answer sets returned for the program are:

{ edge(b, a), node(a), node(b), in(b), in(a) }
{ out(a), edge(b, a), node(a), node(b), in(b) }
{ out(b), edge(b, a), node(a), node(b), in(a) }
{ out(b), out(a), edge(b, a), node(a), node(b) }

The first answer set should be removed by the constraint. The correct answer sets would be:

{ out(a), edge(b, a), node(a), node(b), in(b) }
{ out(b), edge(b, a), node(a), node(b), in(a) }
{ out(b), out(a), edge(b, a), node(a), node(b) }

Unit test configuration in CI

Since f9df0aa, unit tests are being executed in a different configuration on CI than on a local machine.

Alpha/src/test/java/at/ac/tuwien/kr/alpha/solver/AbstractSolverTests.java

Lines 79 to 82 in ecd354a

	String[] solvers = getProperty("solvers", ci ? "default" : "default,naive");
	String[] grounders = getProperty("grounders", "naive");
	String[] stores = getProperty("stores", ci ? "alpharoaming" : "alpharoaming,naive");
	String[] heuristics = getProperty("heuristics", ci ? "ALL" : "NAIVE");

What I find odd is that fewer configurations (e.g. heuristics) are tested in CI mode. Shouldn´t it be the other way round, i.e. faster tests on local machine and extensive tests in CI?

problem with constraints

For the following program the answer set {a(b,b)} is returned, but should not have an answer set:

a(b,b).
:- a(X,X).

Run (some) tests with internal checks enabled.

In the past we discovered several bugs only by running with the time-consuming internal checks enabled and we have several example programs that triggered those issues (e.g. in #101). In order to avoid regressions, I think it would make sense to have those programs running with internal checks enabled in our CI test suite.

Note that it is not so much important that Alpha computes the correct answer sets for those programs, but that it runs without violating any of the checks. These kind of tests do not fit well into our current test layout, but I think it would make a valuable contribution and hence I would like to have a place to put them.

Command-line interface should provide option to choose branching heuristic

At the moment, DefaultSolver supports two branching heuristics (see 5a50aba), a number which might even increase in the future. Therefore, the command-line interface should provide an option to choose the heuristic(s).

Fix external atom variable bindings.

External atoms have two open issues.

1. The binding of variables they report seems to contain a bug. External atoms have their input always non-binding, since they cannot be queried without some concrete input. I think for external atoms it should be as follows:

• If the external atom is negative, then all variables of input and output are non-binding and there are no binding variables (like for ordinary atoms).
• If the external atom is positive, then variables of input are non-binding and variables of output are binding.

2. In the NaiveGrounder line 585 there is a check
   if (substitutions.isEmpty() && rule.isBodyAtomPositive(atomPos))
   where it probably should just check for isEmpty(). The current check seems to solve an underlying bug where ExternalAtom.getSubstitutions should, in case of no bound variables, still return a singleton list containing only the partialSubstitution it received as input. It currently does not, because probably some subclass of FixedInterpretationPredicate.evaluate returns an empty set (of lists of constants) for when it finds no bindings, when instead it should return a singleton set containing an empty list of constants.
   So an external that is true but has no output should yield a singleton set containing an empty list (of constants) while an external that is false (and hence has not output) should yield an empty set (of lists of constants).

Empty set wrongly computed as answer set (for rules with more than one default negation in the body)

Hi,
For

a:-not b,not c.
b:-not a,not c.

Alpha currently returns the expected answer sets {{a} {b}}.

For

a:-not b,not c.
b:-not a,not c.
c:-not a,not b.

the result also contains the empty answer set, which is not an valid answer set:

{ ChoiceOn(1), ChoiceOn(0), ChoiceOn(2), ChoiceOff(2), ChoiceOff(1), _R_(0, ), a() }
{ ChoiceOn(1), ChoiceOn(0), ChoiceOn(2), ChoiceOff(2), ChoiceOff(0), _R_(1, ), b() }
{ ChoiceOn(1), ChoiceOn(0), ChoiceOn(2), ChoiceOff(1), ChoiceOff(0), _R_(2, ), c() }
% wrong
{ ChoiceOn(1), ChoiceOn(0), ChoiceOn(2) }

KR Gottfried

ArrayIndexOutOfBoundsException when trying to solve Hanoi Tower

In d1e9b64, test cases for four different instances of the Tower of Hanoi problem are added to the project.
By this, a bug can be discovered that causes an ArrayIndexOutOfBoundsException to be thrown by at.ac.tuwien.kr.alpha.common.NoGood.getLiteral(int):

java.lang.ArrayIndexOutOfBoundsException: -1
at at.ac.tuwien.kr.alpha.common.NoGood.getLiteral(NoGood.java:100)
at at.ac.tuwien.kr.alpha.solver.WatchedNoGood.getLiteralAtAlpha(WatchedNoGood.java:68)
at at.ac.tuwien.kr.alpha.solver.BasicNoGoodStore.addAlphaWatch(BasicNoGoodStore.java:102)
at at.ac.tuwien.kr.alpha.solver.BasicNoGoodStore.ensureWatchInvariantAfterAssignAtLowerDL(BasicNoGoodStore.java:575)
at at.ac.tuwien.kr.alpha.solver.BasicNoGoodStore.propagate(BasicNoGoodStore.java:635)
at at.ac.tuwien.kr.alpha.solver.DefaultSolver.tryAdvance(DefaultSolver.java:104)
at at.ac.tuwien.kr.alpha.solver.AbstractSolver$1.tryAdvance(AbstractSolver.java:31)

This was observed in the following constellations:

• HanoiTowerTest.testInstance2() with random BerkMinLiteral
• HanoiTowerTest.testInstance1() with random Naive

DefaultSolver / NaiveHeuristic: nondeterministic behaviour and wrong solution

When calling at.ac.tuwien.kr.alpha.solver.HanoiTowerTest.testSimple() (on testing-hanoi branch) with DefaultSolver and deterministic NaiveHeuristic, the following can be experienced:

1. Nondeterministic behaviour: Sometimes the solver finds an answer set quickly and returns it (after 87 decisions), sometimes it takes long time and finds no answer set (after 34228 decisions).
2. In the latter case, the result is actually wrong, because there is a solution to the problem.

Number of answer set depends on order of literals in constraint

Hi,
In the following program the number of answer sets produced by the solver depend on the order of the literals in the constraint. Without a constraint the correct answer sets are found i.e. 27 - 3 variables that can have 3 different values. With the constraint all the values of the variables should be different and therefore 6 answer set should remain. The correct result is neither found by the naive nor by the default solver. If the order of literals in the constraint is changed, the number of resulting answer sets change.

eq(1,1).
eq(2,2).
eq(3,3).
var(1).
var(2).
var(3).
val(VAR,1):-var(VAR),not val(VAR,2),not val(VAR,3).
val(VAR,2):-var(VAR),not val(VAR,1),not val(VAR,3).
val(VAR,3):-var(VAR),not val(VAR,1),not val(VAR,2).

% 0 answer sets
%:- val(VAR1,VAL1), val(VAR2,VAL2), eq(VAL1,VAL2), not eq(VAR1,VAR2).
% different literal order: 27 answer sets
%:- eq(VAL1,VAL2), not eq(VAR1,VAR2), val(VAR1,VAL1), val(VAR2,VAL2).

KR Gottfried

missing answer set

For the following program, Alpha outputs three answer sets:

assign(L, R) :- not nassign(L, R), possible(L, R).
nassign(L, R) :- not assign(L, R), possible(L, R).

assigned(L) :- assign(L, R).
:- possible(L,_), not assigned(L).
:- assign(L, R1), assign(L, R2), R1 != R2.

possible(l1, r1). possible(l3, r3). possible(l4, r1). possible(l4, r3). possible(l5, r4). possible(l6, r2). possible(l7, r3). possible(l8, r2). possible(l9, r1). possible(l9, r4).

The answer sets with --filter assign are:

{assign(l9,r4),assign(l8,r2),assign(l7,r3),assign(l6,r2),assign(l5,r4),assign(l4,r3),assign(l3,r3),assign(l2,r2),assign(l1,r1)}
{assign(l9,r1),assign(l8,r2),assign(l7,r3),assign(l6,r2),assign(l5,r4),assign(l4,r3),assign(l3,r3),assign(l2,r2),assign(l1,r1)}
{assign(l9,r1),assign(l8,r2),assign(l7,r3),assign(l6,r2),assign(l5,r4),assign(l4,r1),assign(l3,r3),assign(l2,r2),assign(l1,r1)}

None of the three answer sets contains assign(l9,r4) and assign(l4,r1) simultaneously. However, when I add the following two constraints

:- not assign(l9,r4).
:- not assign(l4,r1).

the following answer set is output:

{assign(l9,r4),assign(l4,r1),assign(l8,r2),assign(l7,r3),assign(l6,r2),assign(l5,r4),assign(l3,r3),assign(l2,r2),assign(l1,r1)}

The latter answer set contains assign(l9,r4) and assign(l4,r1), even though constraints should only delete answer sets.

Optimization: Evaluate input program partially.

It is often the case that rules could fire by facts of the input program alone. For example, the following ASP program contains facts for the edges of a graph and a rule that makes all edges bi-directional, e.g., to consider edges to be undirected.

edge(1,2).
edge(2,4).
edge(5,4).
...
edge(X,Y) :- edge(Y,X).
...

Here, the rule could be fully evaluated by the grounder such that the solver has less work to do and several rounds of back-and-forth between grounder and solver can be skipped.

This kind of optimization allows dramatic speed-ups for many programs and is implemented by all state-of-the-art ASP solvers. This evaluation can be done using stratified negation or well-founded semantics, where the latter is more general but also more involved.

Sort option not working

The sort option is not working. Answer sets are always sorted.
This seems to have 2 causes:

There is a bug in Line 205 of at/ac/tuwien/kr/alpha/Main.java.
if (options.hasOption(OPT_SORT)) {
should be:
if (commandLine.hasOption(OPT_SORT)) {

And both the solver and the sort option use -s, therefore if the solver option is present the sort option is also set.

Option to print statistics

Currently, DefaultSolver logs brief statistics containing numbers of choices, backtracks etc. in logStats() by writing to a Logger on the Debug level. This has the disadvantage that the log level has to be changed in order to see the statistics. It would be better to have a command-line option called "stats" that activates printing the statistics, as in other ASP systems (e.g. clingo).

Exception when using '!='-operator

When I call Alpha with the following program, an exception is returned:

location(a1).
region(r1).
region(r2).

assign(L,R) :- location(L), region(R), not nassign(L,R).
nassign(L,R) :- location(L), region(R), not assign(L,R).

:- assign(L,R1), assign(L,R2), R1 != R2.

aux_ext_assign(a1,r1).
aux_ext_assign(a1,r2).

aux_not_assign(L,R) :- aux_ext_assign(L,R), not assign(L,R).
:- aux_not_assign(L,R), assign(L,R).

The output is the following:

  209 I tuwien.kr.alpha.Main Seed for pseudorandomization is 6083566175591. 
Exception in thread "main" java.lang.IllegalArgumentException: Zero is not a literal (because it cannot be negated).
	at at.ac.tuwien.kr.alpha.common.Literals.atomOf(Literals.java:13)
	at at.ac.tuwien.kr.alpha.solver.GroundConflictNoGoodLearner.computeBackjumpingDecisionLevel(GroundConflictNoGoodLearner.java:250)
	at at.ac.tuwien.kr.alpha.solver.GroundConflictNoGoodLearner.analyzeConflictingNoGoodRepetition(GroundConflictNoGoodLearner.java:129)
	at at.ac.tuwien.kr.alpha.solver.GroundConflictNoGoodLearner.repeatAnalysisIfNotAssigning(GroundConflictNoGoodLearner.java:178)
	at at.ac.tuwien.kr.alpha.solver.GroundConflictNoGoodLearner.analyzeConflictingNoGoodRepetition(GroundConflictNoGoodLearner.java:134)
	at at.ac.tuwien.kr.alpha.solver.GroundConflictNoGoodLearner.analyzeConflictingNoGood(GroundConflictNoGoodLearner.java:76)
	at at.ac.tuwien.kr.alpha.solver.DefaultSolver.addAllNoGoodsAndTreatContradictions(DefaultSolver.java:388)
	at at.ac.tuwien.kr.alpha.solver.DefaultSolver.obtainNoGoodsFromGrounder(DefaultSolver.java:348)
	at at.ac.tuwien.kr.alpha.solver.DefaultSolver.tryAdvance(DefaultSolver.java:151)
	at at.ac.tuwien.kr.alpha.solver.AbstractSolver$1.tryAdvance(AbstractSolver.java:31)
	at java.util.Spliterator.forEachRemaining(Spliterator.java:326)
	at java.util.stream.ReferencePipeline$Head.forEach(ReferencePipeline.java:580)
	at at.ac.tuwien.kr.alpha.Main.main(Main.java:224)

However, if I replace the operator '!=' by using 'unequal'-facts, the exception does not occur. Thus, the problem might be connected to #45. The translation, which does not yield the exception, is the following:

location(a1).
region(r1).
region(r2).

assign(L,R) :- location(L), region(R), not nassign(L,R).
nassign(L,R) :- location(L), region(R), not assign(L,R).

:- assign(L,R1), assign(L,R2), unequal(R1,R2).

aux_ext_assign(a1,r1).
aux_ext_assign(a1,r2).

aux_not_assign(L,R) :- aux_ext_assign(L,R), not assign(L,R).
:- aux_not_assign(L,R), assign(L,R).

unequal(r1,r2).
unequal(r2,r1).

Alpha uses "\n" instead of System.lineSeparator() at some places

For platform independence, we should always use System.lineSeparator() instead of "\n" or "\r\n".

Calling arbitrary methods on constants

With the perspective of constants as objects, we might speculate about allowing rules of the form:

head(X,Y)     :- X.get[0](Y), isList(X).      % ex1
contains(X,Y) :- X.contains[0](Y), isList(Y). % ex2
colored(N,C)  :- N.getColor(C), node(N).      % ex3

The idea is that for some ConstantTerm<T> we could actually call any method from T on it as some sort of external atom and use the result to bind a new variable.

This would allow for very cool interoperability with the Java world. We would just need to make our users aware that calling methods with side-effects this way is probably blow up everything ...

Wrong answer-set with double occurrence of a variable in one atom.

The atom q(a) is missing from the answer-set of the following program:

p(a, a).

q(X) :- p(X, X).

s(X) :- p(X, X1), X = X1.
r(X) :- p(X, X1).
t(X) :- p(X, X1), p(X1, X).

Adding the constraint :- p(X,X). does not change its answer-sets (it should have no answer-sets then). This hints at the grounder erroneously not generating instances for atoms where the same variable occurs twice.

Rename NaiveGrounder to DefaultGrounder

The NaiveGrounder is now quite far away from implementing just a naive grounding procedure and it is used by default (with no real alternative at the moment). Therefore it is adequate to rename it to DefaultGrounder.

implied atom not in answer set

Hi,
Something i stumbled across, when i was porting a GGP tic tac toe program to ASP. The following program should have one answer set containing tictactoe(b,...). Alpha returns one answer set but without the atom tictactoe(b,...).

next(1,2).
size(1).
size(2).
size(3).
cell(R,C,b,1) :- size(R), size(C).

cell(M,N,b,TNEXT):-
    next(T,TNEXT),
    cell(M,N,b,T),
    not isMarked(M,N,T).

tictactoe(M11,M12,M13,M21,M22,M23,M31,M32,M33):-
    cell(1,1,M11,2),
    cell(1,2,M12,2),
    cell(1,3,M13,2),
    cell(2,1,M21,2),
    cell(2,2,M22,2),
    cell(2,3,M23,2),
    cell(3,1,M31,2),
    cell(3,2,M32,2),
    cell(3,3,M33,2).

% answer set should contain tictactoe(b,b,b,b,b,b,b,b,b)

KR Gottfried

Extended statistics

Currently, Alpha is able to log a small number of statistical values on the solving process (cf. #51, #99, #102).
To gather more data, it could be beneficial to log other values as well. Which ones should that be?

For example, clasp outputs something like the following:

Models : 1+
Calls : 1
Time : 28.071s (Solving: 27.05s 1st Model: 27.04s Unsat: 0.00s)
CPU Time : 27.191s

Choices : 133724
Conflicts : 103856 (Analyzed: 103856)
Restarts : 331 (Average: 313.76 Last: 167)
Model-Level : 26.0
Problems : 1 (Average Length: 0.00 Splits: 0)

Lemmas : 103856 (Deleted: 77119)

Binary : 1655 (Ratio: 1.59%)
Ternary : 2541 (Ratio: 2.45%)
Conflict : 103856 (Average Length: 33.4 Ratio: 100.00%)
Loop : 0 (Average Length: 0.0 Ratio: 0.00%)
Other : 0 (Average Length: 0.0 Ratio: 0.00%)

Backjumps : 103856 (Average: 1.26 Max: 48 Sum: 130701)

Executed : 103856 (Average: 1.26 Max: 48 Sum: 130701 Ratio: 100.00%)
Bounded : 0 (Average: 0.00 Max: 0 Sum: 0 Ratio: 0.00%)

Rules : 105814
Atoms : 36917
Bodies : 67239
Equivalences : 37788 (Atom=Atom: 303 Body=Body: 1758 Other: 35727)
Tight : Yes
Variables : 22212 (Eliminated: 0 Frozen: 0)
Constraints : 85168 (Binary: 77.7% Ternary: 22.2% Other: 0.1%)

Conflict-driven non-ground rule learning

Alpha'a predecessor OMiGA employs unfolding and shifting techniques to learn new non-ground rules during the solving process, thereby improving search performance [1]. Alpha would probably also benefit from such techniques (at least from unfolding). Rules learnt that way can also be added to the input program to improve future solver runs.

[1]: Weinzierl, Antonius (2013): Learning Non-Ground Rules for Answer-Set Solving. In David Pearce, Shahab Tasharrofi, Evgenia Ternovska, Concepción Vidal (Eds.): 2nd Workshop on Grounding and Transformations for Theories With Variables. Workshop on Grounding and Transformations for Theories With Variables. Corunna, Spain, September 15, pp. 25–37.