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 SolversArtificial 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,

Experiments on ASSAT 2.0  

Hard jobs we found for SAT solvers 

A set of Randomly Generated Logic Programs


1. Several files are needed in your directory to execute ASSAT(X).

2. Syntax

$ lparse <input-file> | assat -lparse <options>


$ dlv -instantiate <input-file> | assat -dlv <options>


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

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 )

-w ( -wellfounded )
Compute well-founded model.

-sat < Chaff2 > | < walksat > | < sato > | < satz > | < grasp > | < satz-rand >
Sat solvers used in the system. Defaultly Chaff2.

ASSAT output data in digital format. Defaultly in text format.

< -lparse > | < -dlv >
Using lparse (dlv) as the grounding system. Defaultly lparse.

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
* Pre-processing:
* Clark's Completion: ratio: 0.000000
* SAT solver:
Chaff2: User CPU time: 0.04 (seconds) Check... No
Chaff2: User CPU time: 0.03 (seconds) Check... No
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

Related Publications

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.

Yuting Zhao
Last modified: Thursday Octobor 25 2004