(b) If (X \ *Head*(Π))∩ At(Π) = /0, then X is an input answer set of Π if and only if X ∩*Head*(Π) is an answer set of Π.

We now introduce a propositional formalism that we call satisfiability modulo ASP and denote by SM(ASP). Later in the paper we show that SM(ASP) can be viewed as a common generalization of both ASP and PC(ID). Theories of SM(ASP) are pairs [F,Π], where F
is a set of clauses and Π is a program. In the definition below and in the remainder of the paper, for a set M of literals we write M+ to denote the set of atoms (non-negated literals)
in M. For instance, {a,¬b}
+ = {a}.

Definition 3 For an SM(ASP) theory [F,Π], a consistent and complete (over At(F∪Π)) set M of literals is a model of [F,Π] if M is a model of F and M+ is an input answer set of Π.

For instance, let F be a clause b∨¬c and Π be program (3). The SM(ASP) theory [F,Π]
has two models {b,¬c,a} and {b,c,¬a}.

The problem of finding models of pairs [F,Π] can be regarded as an SMT problem in which, given a formula F and a program Π, the goal is to find a model of F that is (its representation by the set of its true atoms, to be precise) an input answer set of Π. This observation motivated our choice of the name for the formalism.

As for PC(ID) theories, also for an SM(ASP) theory [F,Π] we write Πofor the program ΠAt(Π∪F). We have the following simple observation.

Proposition 4 A set M of literals is a model of an SM(ASP) theory [F,Π] if and only if M is a model of an SM(ASP) theory [F,Πo].

It is evident that a set M of literals is a model of F if and only if M is a model of [F, /0].

Thus, SM(ASP) allows us to express the propositional satisfiability problem. We now show that the SM(ASP) formalism captures ASP. Let Π be a program. We say that a set F of clauses is Π-safe if 1. F |= ¬a, for every a ∈ O
Π
At(Π)
, and 2. for every answer set X of Π there is a model M of F such that X = M+ ∩*Head*(Π).

Proposition 5 Let Π be a program. For every Π-safe set F of clauses, a set X of atoms is an answer set of Π if and only if X = M+ ∩At(Π), for some model M of [F,Π].

This result shows that for an appropriately chosen theory F, answer sets of a program Π
can be derived in a direct way from models of an SM(ASP) theory [F,Π]. There are several possible choices for F that satisfy the requirement of Π-safety. One of them is the Clark's completion of Π (Clark 1978). We recall that the completion of a program Π consists of clauses in Πcl and of the formulas that can be written as

¬a∨_
B∈Bodies(Π,a)
B (4)
for every atom a in Π that is not a fact (that is, the set *Bodies*(Π,a) contains no empty body). Formulas (4) can be clausified in a straightforward way by applying distributivity.