ryanbhayward/algs

python algorithms for CMPUT 204 and 304

algs's Issues

fix_literal() skips over some clauses

When stepping through the program for the sake of my own understanding, I came across a nasty bug in the fix_literal() method in backsat.py.

The problem is on these lines:

algs/hard/sat/backsat.py

Lines 44 to 51 in 38b5341

	for c in f:
	if t in c:
	f.remove(c)
	elif -t in c:
	c.remove(-t)
	if len(c)==0: # empty clause so f unsatisfiable
	print(' *- empty clause -*')
	return ''

Essentially, there is a for loop iterating on a list whose order is modified during the for loop. In some cases this doesn't cause any problems but is generally considered bad practice. Python's for x in y loop syntax uses indexing in the background, so removing an element might shift a further unseen element to an index for which Python has explored already.

Specifically, when there are two elements side by side in the list, that both match the removal condition, the first one will be removed and the second one will be skipped. Running the following input to the function:

f = [[1, 4, -5], [1, 3, -4], [2, -3, -4], [3, 4, 5]]
fix_literal(1, f, '?????')

produces the following result:

[[1, 3, -4], [2, -3, -4], [3, 4, 5]]

instead of the expected result:

[[2, -3, -4], [3, 4, 5]]

I'm not exactly sure what issues this might cause when the broader program is considered, as I have not analyzed it to that extent at the moment. I would imagine some valid satisfying assignments are thrown out because of this bug, though I haven't confirmed this.