SC Chapter 6 Bit Vectors
Questions about the lecture 'Satisfiability Checking' of the RWTH Aachen Chapter 6 Bit Vectors
Questions about the lecture 'Satisfiability Checking' of the RWTH Aachen Chapter 6 Bit Vectors
Kartei Details
| Karten | 24 |
|---|---|
| Sprache | English |
| Kategorie | Informatik |
| Stufe | Universität |
| Erstellt / Aktualisiert | 18.02.2017 / 27.02.2017 |
| Weblink |
https://card2brain.ch/box/20170218_sc_chapter_6_bit_vectors
|
| Einbinden |
<iframe src="https://card2brain.ch/box/20170218_sc_chapter_6_bit_vectors/embed" width="780" height="150" scrolling="no" frameborder="0"></iframe>
|
Lernkarteien erstellen oder kopieren
Mit einem Upgrade kannst du unlimitiert Lernkarteien erstellen oder kopieren und viele Zusatzfunktionen mehr nutzen.
Melde dich an, um alle Karten zu sehen.
Why is bit vector logic (BVL) needed?
Because of bit-wise operation and arithmetic overflow in system-level software
What can happen for large software?
Formulas will become large
What are current implementations using BVL? [5]
1. CBMC
2. SATABS
3. F-Soft (NEC)
4. SATURN (Stanford, Aiken)
5. EXE (Stanford, Engler and Dill)
What are the syntax components of BVL? [5]
1. Operators op are + - * / << >> & | xor °
2. Terms t are t op t, identifier, ~t, constant c, a?t:t, t[c:c], ext(t)
3. Relations rel are = <
4. Atoms a are t rel t, Boolean-Identifier, t[c]
5. Formulas f are f \lor f, \neg f, atom
What is a semantic problem of BVL compared to N and R?
(x-y)>0 ↔ x>y does not hold for BVL
What are the semantic components of BVL? [3]
1. Vector x
2. Width
3. Encoding E
What are the characteristics of the vector x of BVL? [3]
1. Every entry x(i) or x_i is mapped to 0 or 1
2. Most left is highest index l-1
3. Most right is lowest index 0
What are possible encodings E of BVL? [4]
1. Binary U 2. two’s complement S 3. fixed-point and 4. floating-point
What is the definition of the encoding binary U for BVL?
<x>U = Sumi=0l-1 ai*2i
What is the definition of the encoding two’s complement S for BVL?
<x>S = -2l-1*al-1 + Sumi=0l-2 ai*2i
What are the characteristics of lambda-notations for BVL? [1+3]
1. Functions without a name
Examples
2. Zero vector of length l
3. Inverting vector
4. Bit-wise OR
How are arithmetic expression interpreted in BVL? [3]
1. a[l]E +-E b[l]E = c[l]E ↔ <a>E +- <b>E = <c>E mod 2l
2. a[l]E < b[l]E ↔ <a>E < <b>E
3. E can vary among components // Not supported by most compilers
What holds for the complexity of BVL? [2]
1. Unsatisfiable for unbounded width
2. NP-complete otherwise
Name two possible decision procedures of BVL? [2]
1. Flattening BVL
2. Incremental flattening
What are the characteristics of flattening BVL? [4]
1. Called bit blasting
2. Transform BVL into PL
3. Add boolean variable for every bit i of each term t: mye(t)_i
4. Add constraint for each term
Which types of constraints do you know for flattening BVL? [4]
Constraints for 1. bit-wise operators 2. bit+bit 3. bits+bits and 4. bit */mod bit
What is the constraint for bit-wise operators in flattening BVL?
a op[l] b: \foralli=0l-1 (mye(t)i = ai op bi)
What are the (two) constraints for bit+bit in flattening BVL? [4]
1. Use a full adder
2. s = a+b+i mod 2 = a xor b xor i
3. o = a+b+i div 2 = (a \land b) \lor (a \land i) \lor (b \land i
4. Convert s and o into CNF with 14 clauses
What holds for the constraints for bits+bits in flattening BVL? [4]
1. Use length times many full adder with o as I
2. So-called carry chain adder
3. 2*l more variables
4. 14*l more clauses
What holds for the constraints for bit */mod bit in flattening BVL? [2]
1. Small example creates around 11000 variables
2. Unsolvable for current SAT solvers
What are the characteristics of the counterexample guided abstraction refinement (CEGAR) algorithm of incremental flattening? [3]
1. phi_sk is boolean part of phi_f
2. F is set of terms in the encoding
3. I is set of terms inconsistent with the current assignment
What are the four steps of the CEGAR algorithm of incremental flattening? [4]
1. If phif SAT then compute I with satisfying assignment alpha
2. Else return UNSAT
3. If I = empty set then return SAT
4. Else compute
4.1 F’ \subseteq (I\F)
4.2 F = F \cup F’
4.3 phi_f = phi_f \land constraint(F)
4.4 and 2.
What are hints concerning incremental flattening? [4]
1. Add easy parts of the formula first
2. Add hard parts only when needed
3. Use incremental SAT solver
4. Guess values of missing variables
What are possible guesses for missing variables in incremental flattening? [3]
1. Zeros
2. Sign extension
3. Propagate constants
-
- 1 / 24
-
