Decide satisfiability of a CNF formula by DPLL

Unit propagation, pure literal elimination, then a split on the lowest-indexed unassigned variable trying TRUE first. The index rule is deterministic, so decision and propagation counts are reproducible and match the Python arm exactly.

Usage

Dpll(cnf)

Arguments

cnf

Iterated over elementwise, with lapply.

Value

A list with satisfiable, assignment, model, n_vars, n_clauses, decisions, propagations, pure_literals, method.

Examples

V <- c(1, 2, 3, 4, 5, 6, 7, 8)
Dpll(V)
#> $satisfiable
#> [1] TRUE
#> 
#> $assignment
#> $assignment$`1`
#> [1] TRUE
#> 
#> $assignment$`2`
#> [1] TRUE
#> 
#> $assignment$`3`
#> [1] TRUE
#> 
#> $assignment$`4`
#> [1] TRUE
#> 
#> $assignment$`5`
#> [1] TRUE
#> 
#> $assignment$`6`
#> [1] TRUE
#> 
#> $assignment$`7`
#> [1] TRUE
#> 
#> $assignment$`8`
#> [1] TRUE
#> 
#> 
#> $model
#> $model$`1`
#> [1] TRUE
#> 
#> $model$`2`
#> [1] TRUE
#> 
#> $model$`3`
#> [1] TRUE
#> 
#> $model$`4`
#> [1] TRUE
#> 
#> $model$`5`
#> [1] TRUE
#> 
#> $model$`6`
#> [1] TRUE
#> 
#> $model$`7`
#> [1] TRUE
#> 
#> $model$`8`
#> [1] TRUE
#> 
#> 
#> $n_vars
#> [1] 8
#> 
#> $n_clauses
#> [1] 8
#> 
#> $decisions
#> [1] 0
#> 
#> $propagations
#> [1] 8
#> 
#> $pure_literals
#> [1] 0
#> 
#> $method
#> [1] "DPLL: unit propagation, pure literal, split on the lowest-indexed variable, True first"
#>