( April 11 2002)


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. 


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.

The Block's World Planning Domain 

The Graph Coloring Domain 

The Hamiltonian Circuit Domain 

Hard jobs we found for SAT solvers 


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:

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

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


* 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


grasp +s1 +O
sato -m2

  • 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.


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

Yuting Zhao
Last modified: Thursday April 11 2002