SC Chapter 3 SAT Solving
Questions about the lecture 'Satisfiability Checking' of the RWTH Aachen Chapter 3 SAT Solving
Questions about the lecture 'Satisfiability Checking' of the RWTH Aachen Chapter 3 SAT Solving
Set of flashcards Details
| Flashcards | 25 |
|---|---|
| Language | English |
| Category | Computer Science |
| Level | University |
| Created / Updated | 18.02.2017 / 27.02.2017 |
| Weblink |
https://card2brain.ch/box/20170218_sc_chapter_3_sat_solving
|
| Embed |
<iframe src="https://card2brain.ch/box/20170218_sc_chapter_3_sat_solving/embed" width="780" height="150" scrolling="no" frameborder="0"></iframe>
|
What are the components of SAT-solving? [3]
1. Decision as enumeration
2. Boolean constraint propagation (BCP)
3. Conflict resolution and backtracking
What is the definition of the enumeration algorithm? [4]
1. Assign values to all variables as (var, v, false)
2. If all clauses satisfy return SAT // Order of variables and values influences runtime
3. Else change the latest false variable assignment to (var, \neg v, true)
4. If no variable assignment is left return UNSAT
What are characteristics of decision heuristics? [4]
1. Static variable order // x < y < z
2. Static value order // true < false
3. Influences runtime of SAT formulae
4. Does not influence runtime of UNSAT formulae
What are examples of decision heuristics? [3]
1. Dynamic largest individual sum (DLIS), 2. Jerosolow-Wang method and 3. Variable state independent decaying sum (VSIDS)
What are the characteristics of DLIS? [6]
1. Cx is number of unresolved clauses for positive x
2. C\negx is number of unresolved clauses for negative x
3. Choose x as max Cx and y as max C\negy
4. Choose x as true if Cx>C\negy otherwise y as false
5. Requires O(#literals) queries for each decision
6. O(2^n *n*m*k) with n #var, m #clauses and k #litPerClause
What are the characteristics of Jerosolow-Wang method? [3]
1. Compute J(l) = Sum_(l \in c, c \in phi) 2^(-|c|) for all literals l with clause c and |c| number of literals in c // Sum of all clauses where the literal l appears
2. Choose maximizing l
3. Literals in shorter clauses have higher weight
What are the characteristics of VSIDS? [8]
1. Watch variables used in recent clauses used for conflict resolution // Conflict driven decision strategy
2. Static because does not depend on current assignment
3. Dynamic because it gradually changes
4. Count for every variable by increasing increment value
5. Choose unassigned variable with the highest counter for decision // constant time
6. Periodically counters and increment value and counters are divided by constant
7. Chaff stores unassigned variables sorted by counter value
8. Update is only necessary when adding conflict clauses
What are the statues of clauses? [4]
1. satisfied if at least one literal is satisfied
2. unsatisfied if all literals are assigned but unsatisfied
3. unit if all but one literals are assigned but unsatisfied // imply consequences of decisions
4. unresolved if none of the other statuses
What is the definition of decision level (DL)?
A counter for decisions
What is the definition of the antecedent?
The unit clause implying the value of l // nil if decision
What are the characteristics of watching literals? [2]
1. Large effort to watch each literal in each clause of each propagation
2. Instead watch two literals for each clause such that one of them is true or both unassigned
What is the definition of the watching literals algorithm? [5]
1. If l gets assigned update clause(\neg l, k)
2. If k is true then clause is satisfied
3. Else if k is false then replace k by other literal k’
4. Else if k is unassigned then clause is unit
5. Else clause is unsatisfied
What is the definition of the implication graph? [4]
1. labeled directed acyclic with G=(V,E,L)
2. V is set of currently assigned variables and conflict node kappa
3. L is labeling function assigning to each node (var=v@DL) and kappa for node kappa
4. E is set of edges that unit clauses imply other assignments and to node kappa for conflicting clause
What is the definition of asserting clauses? [2]
1. Asserting clause has one literal from the current DL // considered by modern solvers
2. The clause obtained by applying resolution on the conflicting clauses of the decision level
What is the definition of unique implication points (UIP)?
A node reached by all paths from the decision node // first UIP is closest to the conflict
What is the definition of the backtracking algorithm? [2]
1. Add asserting clause to clause set // Not necessary for completeness
2. Backtrack to second highest DL (dl) in the asserting clause without erasing
What means a conflict at DL zero?
The formula is unsatisfiable
What is the definition of an unsatisfiable core? [3]
1. Original set of clauses is a core
2. Set of clauses used for resolution in CA // not minimal
3. Small set of clauses via resolution graph
What is the theorem of conflict resolution and backtracking?
“It is never the case that the solver enters decision level dl again with the same partial assignment.”
What is the definition of the basic SAT algorithm CDCL? [4]
1. If BCP not possible return UNSAT
2. Loop { If decision not possible return SAT // satisfiable assignment found
3. While BCP not possible // conflict found
4. If conflict not resolvable return UNSAT } <---
What is the definition of the basic SAT algorithm DPLL? [5]
1. Clear trail of all assignments
2. If BCP not possible return UNSAT
3. Loop { If decision not possible return SAT // satisfiable assignment found
4. While BCP not possible // conflict found
5. If backtrack not possible return UNSAT } <---
What is the definition of the basic SAT algorithm BCP? [3]
1. While unit clauses available push assignment to trail
2. If one clause is unsatisfiable return false
3. Else return true
What is the definition of the basic SAT algorithm Decision? [3]
1. If all variables are assigned return false
2. Choose unassigned variable and push assignment to trail
3. return true
What is the definition of the basic SAT algorithm Backtrack? [3]
1. Loop { If trail is empty return false
2. Pop assignment from trail
3. If assignment unmodified change value and return true }
What is an example for an basic SAT algorithm implementation? [4]
1. DPLL for search
2. CDCL for backtracking
3. Watching literals to enhance propagation
4. VSIDS as variable ordering heuristics with lexicographic order
