Please enable JavaScript.
Coggle requires JavaScript to display documents.
CS161 Homework 4 - Coggle Diagram
CS161
Homework 4
CNF Representatation
Examples
(1 ∨ ¬2 ∨ 3)
(1 -2 3)
(X ∨ ¬Y ∨ Z) ∧ ¬X ∧ (¬Y ∨ ¬Z)
\(\Delta\) = ((1 -2 3) (-1) (-2 -3))
Solution = (-1 -2 3) or any combination of this
Not
Negative numbers
-2 = ¬2
List of lists
Solution
(-1 -2 3) means X = False, Y = False, Z = True
Symbols
\(\lor\) = or
\(\land\) = and
sat-solver
is-clause-true
Variable ordering
Start with the simplest and fastest one
on path
Choosing which VARIABLE to start with
Choosing which VARIABLE ASSIGNMENT to start with
Questions
Iterative?
Do we Wait until we assign all variables?
Variable Ordering
(-1)
How do we assign?
How do we know whaat variables are inside
If we have (-2 -3) as a clause how do we try assignments
Recursively call try-move on (car expr) and (* -1 (car expr))
How to eliminate
Constraint Satisfaction Problem
Variable Domain
0 or 1
Constraint
Backtrack
Backtrack when no legal value to assign to variable
variable -> Possible solutions
1 -> (-1 1)
1 -> () backtrack
sat (n delta)
Returns
any solution
nil otherwise
Arguments
n = number of variables
delta = cnf
Test
cnfs folder
Useful for testing larger cnfs
DIMACS
Example
A file example with line numbers
(1 ∨ ¬2 ∨ 3) ∧ −1 ∧ (¬2 ∨ ¬3) ∧ 3
c this is a comment line
p cnf 3 4
1 -2 3 0
-1 0
-2 -3 0
3 0
Clauses
4 in the example implies 4 clauses
Each clause ends with a 0
Comments
Must be at start of file or between clauses
Comments are followed by the letter c
Problem line
Starts with p
3 = number of variables
4 = number of clauses
Naming
Expr
The question at hand