FASP

Fasp is an implementation for computing the answer sets of a logic program with functions that are generally defined symbolic functions as that of typed first-order logic. The current implementation is based upon the state-of-the-art CSP solvers that are available for the international competition of CSP solvers. For the sake of simplicity, the current implementation of fasp can only work with the logic programs that are free of functions in arguments, namely, none of predicates or functions has a proper functional term in their arguments.

Briefly, given a ground logic program (possibly) with functions P, Fasp(X), depending on the CSP solver X used, works as follows:

Computes the completion of P and convert it into a CSP instance Σ in the language CSP2.0 used at the 2006 CSP competition.
Repeats

Finds a solution S of Σ by X.
If no solution, returns with no answer set.
Maps S to an interpretation I of P.
If I is an answer set of P returns with it.
Otherwise, finds some loops in P that are not satisfied by I and adds their corresponding loop formulas as constraint into Σ.

The above method is similar to that of ASSAT. Comparing with ASSAT, Fasp makes use of CSP solvers instead of SAT solvers.

The current version of fasp, fasp-0.6, has been implemented using C++ with STL by Yisong Wang, and works under Linux Red Hat system. We had tested it with the CSP solovers: Abscon, sat4j and sugar 0.3 using minisat2.0. All the three CSP solvers are implemented in java, thus Java(TM) is also needed for our Fasp.

Download & install

This system is copyright by HKUST and is distributed freely for academic use at your own risk under the GNU Public Licence. You can download, unpack and compile it into binary file. The sample instructions for unpack and compile are as follows:

% tar xvf fasp0.6.tar

% cd fasp0.6

% make

Now there will be the executable file "fasp".

Usage

In this package, we also included the CSP solver abscon109 and a test logic program for Hamiltonian circuit whose graph is encoded as {arc(1,2), arc(2,1), arc(2,3), arc(3,4),arc(4,3), arc(4,1)}. You can test fasp by simply run:

% test/test.lp

The output looks like the follows:

version 0.6 build: May 7 2008, 17:14:36
Answer set:
vertex(1) vertex(2) vertex(3) vertex(4) arc(2,1) arc(1,2) arc(2,3) arc(3,4) arc(4,3) arc(4,1) initial(1) reached(2) reached(1) reached(4) reached(3) hc(1)=2 hc(4)=1 hc(3)=4 hc(2)=3
Duration: 1.4642
Number of atoms: 25
Number of functions: 4
Number of rules: 38
Number of loop formulas: 0
Number of calls to CSP solver: 1
CSP solver duration: 1.4482
Total Duration: 1.4642

In particular, if there is no function assignment is given in terms of the answer set returned by fasp, then the function can be assigned arbitrary value of its range. For instance,

% fasp test/test4.lp

The output is as following:

Answer set:
num(0) num(1) f(1)=0
Duration: 1.1921
Number of atoms: 2
Number of functions: 1
Number of rules: 3
Number of loop formulas: 0
Number of calls to CSP solver: 1
CSP solver duration: 1.1761
Total Duration: 1.1921

where the function f(0) can be arbitrary.

1. Several files are needed in your directory to execute fasp

fasp: the executable binary file.
fasp.ini: the confiuration file for CSP solvers. The current implementation require the fasp.ini contains the following contents:

It indicates fasp how to recognize the output of the CSP solvers.

The CSP solver and its environment. Please assure yourself that the CSP solver is executable by your own. For instance, you can test the CSP solver abscon as the following:

% fasp -x test.xml test

% java -jar abscon109.jar mac.xml 1 XSax test.xml

2. Syntax

% fasp [options] <a ground logic program> Without any option, fasp believes the default CSP solver, abscon109.jar, is the intended CSP solver that you want to call. fasp will write the answer set, if found, to the standard output, along with some statistics, including elapsed CPU time. Fasp accepts the following options: options: -v Print the version number of make and exit. -h, --help Print this message and exit. -lf <number> The restriction of number of loops. -s Do not simplify the input program. -c '<csp_solver>' Use <csp_solver>, default is abscon109.jar. -p <file> Print the program into the <file> only. -x <file> Print the completion into <file> in CSP2.0 only. -t <hours> Set time resource, default 0 means forever. -o <file> Print into given <file> instead of screen. Related Publications Fangzhen Lin and Yisong Wang. Answer Set Programming with Functions, (To appear in KR-08)

Yisong Wang

Last modified: Thursday June 15 2008