|
|
ASSAT
ASSAT (Answer Sets by SAT solvers) is a system for computing answer sets of a logic program by
using SAT solvers. Briefly speaking, given a ground logic program P, ASSAT(X),
depending on the SAT solver X used, works as follows:
-
Computes the completion of P and converts it into a set C
of clauses.
- Repeats
-
Calls X on C to get a model M
(terminates with failure if no such M exists).
-
If M is an answer set of P, then returns with it.
-
Otherwise, finds some loops in P whose loop formulas are not satisfied by
M and adds their corresponding clauses to C.
As shown in the paper "
ASSAT: Computing Answer Sets of A Logic Program By SAT Solvers"
Artificial Intelligence 157(1-2): 115-137 (2004) by Fangzhen Lin
and Yuting Zhao (This is actually
a revised version of the paper that corrects
an error in the definition of loops in the AIJ paper), this procedure is sound and complete, assuming
that X is a sound and complete SAT solver.
The current version of ASSAT; ASSAT 2.0,
has been implemented in C++ by Yuting Zhao, and works under Unix Solaris system.
We have successfully made it work with
zchaff (Dec 4, 2003 version),
mchaff (Chaff2) (Mar 23, 2001 version),
Satz 215.2,
Sato 4.1.
satz-rand,
and
Grasp
, which are SAT solvers based on systematic search algorithms, and
Walksat 41,
a SAT solver based on stochastic local search algorithms. One should also be able to make it work with other SAT solvers.
We have experimented with ASSAT on a variety of benchmark domains and compared its performance with several state-of-art ASP systems, such as smodels and dlv.
For ASSAT, we tried the following SAT solvers:
zchaff (Dec 4, 2003 version),
mchaff (Chaff2) (Mar 23, 2001 version),
Satz 215.2,
Sato 4.1.
satz-rand,
Grasp, and
Walksat 41,
1. Several files are needed in your directory to execute ASSAT(X).
-
A grounding system used to instantiate a given program. It could be
Lparse,
the grounding system of Smodels, or
DLV ( with the paramenter -instantiate ).
- assat, an executable file of ASSAT.
- SAT solver X and its associated files. By default ASSAT uses
Chaff2.
Users can specify other SAT solvers.
2. Syntax
$ lparse <input-file> | assat -lparse <options>
or
$ dlv -instantiate <input-file> | assat -dlv <options>
or
$ assat <input-file> <options>
Without any <option>, ASSAT believes lparse is the grounding system, and use Chaff2 to
compute its answet set. ASSAT will write the answet set, if found, to the standard output, along with some
statistics such as run time and number of loop formulas added.
ASSAT accepts the following options:
-c ( -completion )
This will cause ASSAT to compute the completion of the input program, and write the results to the
standard output. When this option is used, ASSAT will not attempt to call up a SAT solver.
-debug n
Set debug mode n. ASSAT will output some internal data.
-f
Recorde the details of the computation into the file: assat.log (Not available currently)
-l n ( -loop n )
Set the max number of iterations of adding loop formulas and calling sat solvers. Default value: 500
-r n ( -ratio n )
Set threshold of introducing new veriables.
-s n ( -simplify n )
simplify.
-w ( -wellfounded )
Compute well-founded model.
-sat < Chaff2 > | < walksat > | < sato > | < satz > | < grasp > | < satz-rand >
Sat solvers used in the system. Defaultly Chaff2.
-d
ASSAT output data in digital format. Defaultly in text format.
< -lparse > | < -dlv >
Using lparse (dlv) as the grounding system. Defaultly lparse.
-help
Display the ASSAT options.
3. Execution
The answer sets of a logic program np10c can be computed by the followings:
$ lparse np10c hc.lp | assat
ASSAT 1.34
Reading...Done
* Pre-processing:
* Clark's Completion: ratio: 0.000000
* SAT solver:
SAT>>1
Chaff2: User CPU time: 0.04 (seconds) Check... No
SAT>>2
Chaff2: User CPU time: 0.03 (seconds) Check... No
SAT>>3
Chaff2: User CPU time: 0.04 (seconds) Check...
Stable model:
reached(8) reached(9) reached(7) reached(6) reached(5) hc(9,5) reached(4) reached(3) reached(2) reached(1) reached(0)
hc(8,6) hc(7,3) hc(6,7) hc(5,1) hc(4,9) hc(3,0) hc(2,4) hc(1,8) hc(0,2) vertex(9) vertex(8) vertex(7) vertex(6)
vertex(5) vertex(4) vertex(3) vertex(2) vertex(1) vertex(0) initialnode(0) otherroute(9,8) otherroute(9,7)
otherroute(9,6) otherroute(9,4) otherroute(9,3) otherroute(9,2) otherroute(9,1) otherroute(9,0) otherroute(8,9)
otherroute(8,7) otherroute(8,5) otherroute(8,4) otherroute(8,3) otherroute(8,2) otherroute(8,1) otherroute(8,0)
otherroute(7,9) otherroute(7,8) otherroute(7,6) otherroute(7,5) otherroute(7,4) otherroute(7,2) otherroute(7,1)
otherroute(7,0) otherroute(6,9) otherroute(6,8) otherroute(6,5) otherroute(6,4) otherroute(6,3) otherroute(6,2)
otherroute(6,1) otherroute(6,0) otherroute(5,9) otherroute(5,8) otherroute(5,7) otherroute(5,6) otherroute(5,4)
otherroute(5,3) otherroute(5,2) otherroute(5,0) otherroute(4,8) otherroute(4,7) otherroute(4,6) otherroute(4,5)
otherroute(4,3) otherroute(4,2) otherroute(4,1) otherroute(4,0) otherroute(3,9) otherroute(3,8) otherroute(3,7)
otherroute(3,6) otherroute(3,5) otherroute(3,4) otherroute(3,2) otherroute(3,1) otherroute(2,9) otherroute(2,8)
otherroute(2,7) otherroute(2,6) otherroute(2,5) otherroute(2,3) otherroute(2,1) otherroute(2,0) otherroute(1,9)
otherroute(1,7) otherroute(1,6) otherroute(1,5) otherroute(1,4) otherroute(1,3) otherroute(1,2) otherroute(1,0)
otherroute(0,9) otherroute(0,8) otherroute(0,7) otherroute(0,6) otherroute(0,5) otherroute(0,4) otherroute(0,3)
otherroute(0,1) arc(9,8) arc(9,7) arc(9,6) arc(9,5) arc(9,4) arc(9,3) arc(9,2) arc(9,1) arc(9,0) arc(8,9) arc(8,7)
arc(8,6) arc(8,5) arc(8,4) arc(8,3) arc(8,2) arc(8,1) arc(8,0) arc(7,9) arc(7,8) arc(7,6) arc(7,5) arc(7,4) arc(7,3)
arc(7,2) arc(7,1) arc(7,0) arc(6,9) arc(6,8) arc(6,7) arc(6,5) arc(6,4) arc(6,3) arc(6,2) arc(6,1) arc(6,0) arc(5,9)
arc(5,8) arc(5,7) arc(5,6) arc(5,4) arc(5,3) arc(5,2) arc(5,1) arc(5,0) arc(4,9) arc(4,8) arc(4,7) arc(4,6) arc(4,5)
arc(4,3) arc(4,2) arc(4,1) arc(4,0) arc(3,9) arc(3,8) arc(3,7) arc(3,6) arc(3,5) arc(3,4) arc(3,2) arc(3,1) arc(3,0)
arc(2,9) arc(2,8) arc(2,7) arc(2,6) arc(2,5) arc(2,4) arc(2,3) arc(2,1) arc(2,0) arc(1,9) arc(1,8) arc(1,7) arc(1,6)
arc(1,5) arc(1,4) arc(1,3) arc(1,2) arc(1,0) arc(0,9) arc(0,8) arc(0,7) arc(0,6) arc(0,5) arc(0,4) arc(0,3) arc(0,2)
arc(0,1)
Find 1 Stable Model.
Rules: 1731 Atoms: 292 TemporaryVariable: 115 clause: 2278 LoopFormulas: 2
Total time cost of SAT: 0.110000
Execute SAT solver: 3
Check models from SAT: 3
The average time cost of SAT: 0.036667
Pre-processing: 0.02 seconds
Completion: 0.01 seconds
--------Totally: 0.42 seconds
ASSAT reports the total time cost of SAT solvers, the number of loop formulas added and the execution numbers of
SAT solvers. Users could use Unix " time " command to calculate the whole time cost of computing
answer set(s) by ASSAT.
ASSAT 2.0 Standard Dislaimer:
This system is
copyright by HKUST and is distributed freely for academic use without any warranty.
Usage of ASSAT
Fangzhen Lin and Yuting Zhao.
ASSAT: Computing answer sets of a logic program by SAT solvers
This is a revised version of the paper that appeared in
Artificial Intelligence 157(1-2): 115-137 (2004). Essentially,
the revised version includes the
erratum that corrects an error in the definition of loops in the AIJ paper.
|