|
|
( April 11 2002)
ASSAT 1.0
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"
(to
appear in AAAI-02) by Fangzhen
Lin
and
Yuting Zhao,
this procedure
is sound and complete, assuming that X is a sound and complete SAT solver.
The current version of ASSAT; ASSAT
1.0,
has been implemented in C++ by Yuting
Zhao, and works under Unix Solaris system.
We have successfully made it work with
Chaff2,
sato,
satz,
satz-rand,
and
Grasp
,
which are SAT solvers based on systematic search algorithms, and
walksat,
a SAT solver based on stochastic local search algorithms. One should also
be able to make it work
with other SAT solvers.
Experiments
We have experimented with ASSAT on a variety of benchmark domains and compared
its performance with smodels and dlv.
The systems tested are as follows: For specialized answer set generators:
Smodels
version 2.25
and dlv
(Jun 11, 2001 version);
for ASSAT, we tried the following SAT solvers:
Chaff2
(Mar 23, 2001 version),
walksat
3.7,
satz
2.13,
satz-rand
4.7,
and sato.
The following are some pointers to our experimental data on the blocks
world planning domain,
the graph coloring domain, and the Hamiltonian Circuit
domain, all using the logic program encodings by
Niemela
for these problems.
All experiments were done on Sun Ultra 5 machines with
256M memory running Solaris. The reported
times are in CPU seconds as reported
by Unix ''time'' command, and include, for smodels the time
for grounding,
and for ASSAT the time for grounding, computing program completions,
and
checking that the returned assignment is indeed an answer set. We use 2
hours as the cut off
limit. So if an entry is marked by ''---'', it means
that the system in question did not return
after it had used up 2 hours
of the CPU time.
1. Several files are needed in your directory to execute ASSAT(X).
-
lparse,
the grounding system of Smodels, is used
to instantiate a given program.
- assat, an executable file of ASSAT that reads output from lparse.
- A config file that contains information about some parameters used by ASSAT. The
default one is assat-config.
Users could also specify another config file by using option - g <file>
in the command line of assat.
- SAT solver X and its associated files. By default ASSAT uses
Chaff2.
Users can specify other SAT solvers in their ASSAT config file.
2. Syntax
$ assat <option> <input-file1> [<input-file2>]
Without any <option>, ASSAT will call lparse to ground <input-file1>;
( or <input-file1> + <input-file2>), 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
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.
-f <file>
This option will cause ASSAT to write some detailed information into the following 5 files with <file> as the base:
-
<file>.cn0 : the clausal set of the program completion
-
<file>.md0 : the model of <file>.cn0 found by the SAT solver
-
<file>.lpi : the loops found in each iteration
-
<file>.cni : the loop formulas of the loops found in each iteration.
-
<file>.mdi : the model of <file>.cn0 + <file>.cn(i) found by the SAT solver in each
iteration
-t
ASSAT output data in text format.
-g <file>
This option will specify a config file for ASSAT. (The default one is assat-config . )
In addition to specifying the SAT solver, the configuration file can also include options like whether
to do any simplification before computing the completion, and under what conditions the program should
introduce temporary variables in converting the completion and loop formulas to clauses.
The command assat will display the available ASSAT options.
3. Execution
The answer sets of a logic program np10c can be computed by the followings:
$ assat -t np10c
ASSAT 1.0
* Grounding: Lparse ...
* Pre-processing: rules: 1731 atoms: 292
* Clark's Completion:
* SAT solver:
satz-rand: User CPU time: 0.150000 (seconds) Check... Model: 0 NO
satz-rand: User CPU time: 0.170000 (seconds) Check... Model: 1 OK!
reached(8) hc(9,8) reached(9) reached(7) reached(6) reached(5) reached(4) reached(3) reached(2)
reached(1) reached(0) hc(8,1) hc(7,6) hc(6,3) hc(5,4) hc(4,9) hc(3,0) hc(2,5) hc(1,7) 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,7) otherroute(9,6) otherroute(9,5) otherroute(9,4) otherroute(9,3)
otherroute(9,2) otherroute(9,1) otherroute(9,0) otherroute(8,9) otherroute(8,7) otherroute(8,6)
otherroute(8,5) otherroute(8,4) otherroute(8,3) otherroute(8,2) otherroute(8,0) otherroute(7,9)
otherroute(7,8) otherroute(7,5) otherroute(7,4) otherroute(7,3) otherroute(7,2) otherroute(7,1)
otherroute(7,0) otherroute(6,9) otherroute(6,8) otherroute(6,7) otherroute(6,5) otherroute(6,4)
otherroute(6,2) otherroute(6,1) otherroute(6,0) otherroute(5,9) otherroute(5,8) otherroute(5,7)
otherroute(5,6) otherroute(5,3) otherroute(5,2) otherroute(5,1) 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,4) otherroute(2,3) otherroute(2,1) otherroute(2,0) otherroute(1,9)
otherroute(1,8) 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: 0 clause: 1837 LoopFormulas: 1
Total time cost of SAT: 0.310000
Execute SAT solver: 2
Check models from SAT: 2
The average time cost of SAT: 0.155000
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.
4. Config file.
An example config file is given blow:
-Reduce 1
-ConstraintFactReduction 1
-DebugMode 0
-Station 1
-CompletionMode 1
-Order 0
-LoopToSearch 3000
-CheckConclusion 0
-RateOfSubstitute 10000
-ExecuteGrounding 1
-ExecuteSAT 1
-MakeCompletion 1
-OutputModel 1
-grounding:
NONE
-SAT:
satz-rand
walksat
grasp +s1 +O
sato -m2
Chaff2
- The first part are parameters which control the behavior of ASSAT.
LoopToSearch gives the number of total iterations of ASSAT.
In order to avoid a combination explosion when converting clauses to CNFs,
new variables (atom) may be introduced. ASSAT introducea a new variable
only if it can reduce the number of CNFs by RateOfSubstitute times.
So the larger the value of the RateOfSubstitute , the smaller the number of
temporary variables.
- The second part is about the commands of grounding. If you want to use execute
lparse with some parameters, you could write the whole sentence on the line
next. Otherwise, ASSAT reads "NONE" and do the grounding in a simple way.
- The third part is about the commands of SAT. ASSAT will read the next line to get the name of
the SAT specified. If the SAT solver is not specified, then ASSAT will default to Chaff2.
Downloads
ASSAT 1.0 Standard Dislaimer: This system is
copyright by HKUST and is distributed freely for academic use without any warranty.
Usage of ASSAT 1.0
Related Publications
Fangzhen Lin and Yuting Zhao,
ASSAT: Computing Answer Sets of A Logic Program By SAT Solvers, In Proc. of AAAI-02
|