Skip to content

[DPLL] Initialize Watch length with # of literals#1

Open
hyunsooda wants to merge 2 commits intoqwaz:mainfrom
hyunsooda:fix-watch-init
Open

[DPLL] Initialize Watch length with # of literals#1
hyunsooda wants to merge 2 commits intoqwaz:mainfrom
hyunsooda:fix-watch-init

Conversation

@hyunsooda
Copy link

The DPLL solver crashes due to out-of-bounds access when initialized with the clause length. This occurs when working with a CNF of four variables and three clauses.

c ( ¬A ∨ B ) ∧ ( ¬B ∨ ¬C ) ∧ ( C ∨ ¬D )
p cnf 4 3
-1 2 0
-2 -3 0
3 -4 0
thread 'main' panicked at 'index out of bounds: the len is 3 but the index is 3', src/solver/dpll.rs:30:21
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

This PR resolves the issue and includes a related test case. Thanks for the good resource. Learned a lot.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant