CSE308 - Tutorial 7 - Decision procedures for SAT and Bounded Model Checking

Setup

For Exercise 2, you will need to download and extract the files of the tutorial CSE308-TD7-1-handin.zip. You’ll have a folder called CSE308-TD7-1-handin.

You should also have installed pysmt and a SMT solver (in case you did not, you can look at the instructions in the past tutorials).

Evaluation

You will receive a maximum 20 points, subdivided as follows:

• Decision procedures (DPLL and CDCL): 10 points.
• BMC Encodings: 10 points.

Exercise 1. Decision procedures (DPLL and CDCL)

You will first work pen and paper trying to understand better how the DPLL and CDCL algorithm works, and submit your answer in a file named dpll.pdf.

Exercise 1.1

Consider the following set of clauses:

\[ a \lor b \lor \neg c\] \[ c \lor \neg d \] \[ \neg a \lor d \]

Provide all the steps DPLL would do, assuming the algorithm decide the variable to assign in alphabetical order. So, as initially there are no unit clauses, DPLL would first pick the variable \(a\). Also, assume the algorithm first assign the variable to true.

Exercise 1.2

Consider the following set of clauses:

\[ \begin{align} c_1:& A_1 \lor \neg A_4 \lor \neg A_6 \\ c_2:& \neg A_1 \lor A_4 \\ c_3:& A_3 \lor \neg A_7 \\ c_4:& A_4 \lor \neg A_6 \\ c_5:& A_6 \end{align} \]

Write all the sequence of literals that are assigned by Boolean propagation with the corresponding reason clauses. That’s it, use the same notation we used in class where for each literal assigned by unit propagation in the trail you have both the literal and the unit clause (e.g., using the notation on the slides, you may have something like \(A_1\) (\(c_1\)), \(\neg A_7\) (\(c_3\)), … In the example above, the first unit propagation is \(A_6\) (\(c_5\))).

Exercise 1.3

Consider the following set of clauses (is the same from the previous exercise, adding the clause \(c6\)):

\[ \begin{align} c_1:& A_1 \lor \neg A_4 \lor \neg A_6 \\ c_2:& \neg A_1 \lor A_4 \\ c_3:& A_3 \lor \neg A_7 \\ c_4:& A_4 \lor \neg A_6 \\ c_5:& A_6 \\ c_6: & \neg A_1 \lor \neg A_4 \end{align} \]

1. Write the conflict clause you can find applying boolean propagation (here it does not matter if you’re considering all the decisions, 1-st UIP, …).

2. What can you infer about the satisfiability of the set of clause from the conflict clause you derive?

Exercise 1.3

Consider the following set of clauses:

\[ \begin{align} c_1:& A_1 \lor A_8 \\ c_2:& \neg A_1 \lor A_2 \\ c_3:& A_3 \lor A_9 \lor A_{10} \\ c_4:& \neg A_1 \lor \neg A_3 \lor A_4 \\ c_5:& \neg A_1 \lor A_5 \lor A_6 \\ c_6: & \neg A_5 \lor A_6 \\ c_7:& \neg A_5 \lor A_7 \\ c_8:& \neg A_1 \lor \neg A_2 \lor \neg A_6 \lor \neg A_7 \\ \end{align} \]

And the following trail obtained by CDCL: \[ \begin{align} A_1 & \quad \text{decision} \\ A_2 & \quad c_2 \\ A_3 & \quad \text{decision} \\ A_4 & \quad c_4 \\ A_5 & \quad \text{decision} \\ A_6 & \quad c_6 \\ A_7 & \quad c_7 \end{align} \]

Answer the following questions:

1. Compute the conflict clause using the “decision” strategy

2. At what decision level would CDCL backtrack to after this conflict?

3. What sequence Boolean Constraint Propagation steps does CDCL performs just after backtracking? What intepretations (models) will not be explored by CDCL after this Boolean Propagation step?

Bounded Model Checking

Implement the BMC encoding for G p properties

You will work in the file mc308/td7.py. In the first exercise you will implement the Bounded Model Checking algorithm for checking properties of the form G p, where p is a propositional logic formula.

Your task is to implement the function bmc_Gp:

def bmc_Gp(ts : SymbolicTS, p : BoolFormula, k : int) -> Tuple[bool, Optional[KL_lasso]]

The function takes as input a symbolic transition system (ts), the property p to check (i.e., the p from G p), and the length k of the path to check. The function returns a tuple: the first element is False if the function finds a counterexample, and in that case returns a lasso-shaped path as second argument (for now, ignore the second argument and always return None). If bmc cannot determine if there is a violation, the function returns (True,None).

Your task is to construct the bounded model checking encoding for finding a counterexample to the formula G p.

Some hints:

We already provided you with a function in the symbolic transition system class called retime. retime(f, i, j) takes as input a formula that only contains variables from the set V and V' (V_next in the code), an integer i, and an optional integer j, and produces a formula where all the variables V are replaced with variables with index i, and all the variables V_next are replaced with variables with index i+1, if j is not provided, and with index j otherwise. For example:

  ts.retime(And(va, va_next), 2)

where va is the Symbol variable with name a (so, the formula is really a & a_next) will return the formula a_at_2 & a_at_3. Similarly:

ts.retime(And(a, a_next), 2,1)

would return the formula a_at_2 & a_at_1.

Use this function to create the formulas of your BMC encoding.

To check if a formula is satisfiable, you can use different APIs from PySMT.

The easiest one is is_sat(formula) that returns true if the formula is satisfiable. You can call get_model(formula) to get a satisfying assignment in case.

You can directly use the Solver class as follows:

solver = Solver(logic=QF_BOOL)
solver.add_assertion(encoding)
res = solver.solve()
model = solver.get_model()

An important consideration is that calling get_model on a solver object will not try to find again a satisfying assignment (i.e., calling the CDCL algorithm) but will reuse the previous result (solver carries a state while just calling the function is_sat does not).

You can test your implementation in the function test_gp in the td7_script.py file. However, the function does not check that your implementation returns the expected result (i.e., it misses the assert statement), so you have to add these assertion and submit your modified version of the td7_script.py file. Be aware that you would need more calls to the bmc_Gp function to check multiple k-s.

Construct a lasso-shaped counter-example

Extend bmc_Gp to construct a lasso-shaped counter-example from the satisfying assignment found by the SAT solver.

We represent a (k-l)-lasso with the following type:

KL_lasso : TypeAlias = Tuple[List[Mapping[BoolFormula, bool]], int]

where:

• The first element of the tuple List[Mapping[BoolFormula, bool]] represent a path of length k: each element of the list is a state in the path, and each state is just a mapping from variables to truth assignments. So, the list [{a : True, b: False}, {a : True, b: True}] represents a path with 2 states, the first state where a is True and b is False and the second state where both a and b are True.

• The second element of the tuple is an integer representing l, the index where the loop of the lasso start.

You may find the function get_py_value of the Model object returned from get_model useful. The function returns the value (e.g., true or false) assigned to a variable in the encoding. Model is defined in pysmt.solvers.solver and useful, or not:

There are no explicit test cases for this function, but you can print the paths you find when testing your code.

BMC for FG p properties

Implement the function bmc_FGp defined in the file bmc.py to find violations to LTL properties of the form FG p:

def bmc_FGp(ts : SymbolicTS, p : BoolFormula, k : int) -> Tuple[bool, Optional[KL_lasso]]

Also here, look for the function `test_fgp in td7_script.py.

Submit your work

You’ll have to upload the following files