simpleCDCL

graded project for 'Logic and program verification'

This code is essentially a loyal implementation of GRASP(Joa˜o P. Marques-Silva et al) algorithm in python, without the unique implication points optimization.

Key points in implementation

• several dicts(inside var_info, var_value) are maintained for fast lookup for unit clauses
• use of python generator(source: step.inflate_clause()) when calculating causes_of (see the paper in page #5, formula (3))
• iterative(not recursive)(source: step() push() pop()) approach of main DFS procedure
  • note: instead of exact undoing the side-effects(removing the entire clause when satisfied or removing the literal when unsatisfied, before_unmount() after_mounted()) of assignments during pop() process, one must follow the reverse mapping rev from variables to clauses in order to cover the newly-learned clause. see 1f4aaf1
• the ever-true clause where a variable exists in both positive and negative form just hurts the program, and must be got rid of, see also #1

Benchmarks

open tests: python3.61/archlinux/HyperV/Core i7 [email protected] (time in seconds)

BMC	fl100	fl30	sw100	uf100
>30s	1.41	0.04	0.29	0.72
bf26	h6	h7	pret	uf100
1.47	0.72	8.73	3.77	1.75