chapter9 Flashcards
What is a non-deterministic way of computing stable models.
def stable_models ( program ) :
guess Y
i f Y = Cn (P^Y) :
return Y
else :
return fail
guess a Y check the consequences.
What is satifiability testing
It is the area of computer science that studies the problem of determining
whether a propositional formula is satisfiable or not.
What does it mean to be 3-Sat
A propositional formula is 3-SAT if it is a conjunction of clauses, where each clause is a disjunction
of at most three literals.
What is DPLL
DPLL (Davis-Putnam-Logemann-Loveland).is a backtracking algorithm, that uses pure literal elimination and unit propagation.
What is a backtracking algorithm?
A backtracking algorithmenumerates a set of partial candidates that, in principle, could be completed in various ways to give all the possible solutions to the given problem. The completion is done incrementally, by a sequence of candidate extension steps.
What is pure literal elimination?
A Pure literal is a literal that appears only in positive or only in negative form in the formula. Thus, when it is assigned such way, these clauses do not constrain the search anymore, and can be deleted.
What is unit propogation?
Unit propagation consists in removing every clause containing a unit clause’s literal and discarding the complement of a unit clause’s literal from every clause containing the complement. In practice, this often leads to deterministic cascades of units, thus avoiding a large part of the naive search space
What are partial assignments?
The pseudocode DPLL function only returns whether the final assignment satisfies the formula or not. In a real implementation, the partial satisfying assignment typically is also returned on success; this can be derived by keeping track of branching literals and of the literal assignments made during unit propagation and pure literal elimination
What is a unit clause?
A unit clause is one that is not satisfied by the current assiment and contains only a single
unassigned literal.
