vault backup: 2023-09-26 15:32:01
This commit is contained in:
parent
b4bbe1ae12
commit
66ce1bb648
10 changed files with 150 additions and 106 deletions
|
@ -123,4 +123,4 @@ A formula $F$ is:
|
|||
## 2.1 DPLL Framework
|
||||
The idea is to **incrementally construct an assignment compatible with a CNF**, propagating the implications of the decisions made that are easy to detect and simplifying the clauses.
|
||||
|
||||
A CNF is satisfied by an assignment if all its clauses are satisfied. And a clause is satisfied if at least one of its literals is satisfied.
|
||||
A CNF is satisfied by an assignment if all its clauses are satisfied. And a clause is satisfied if at least one of its literals is satisfied.
|
Loading…
Add table
Add a link
Reference in a new issue