AI代写|Lab 2 – Artificial Intelligence



Write a program with 3 modes:

A generic DPLL solver

A BNF to CNF converter

Takes BNF and solves it by running the above two steps


out of 100:

35 points for correct DPLL solver behavior
55 points for correct BNF to CNF converter behavior
10 points for well written code: clear data structures, methods, control flow, etc.
10 points of extra-credit if your converter correctly handles parenthesis ‘(‘ ‘)’

Running your program

A program run should look like: (may be slightly different depending on language, note this in your README)

solver [-v] -mode $mode $input-file

-v is an optional flag for verbose mode (more later)
-mode is followed by one of: cnf, dpll, solver
a mode-dependent input file (see next section)


In mode “cnf” you should expect a BNF input file, convert to CNF and print to console

In mode “dpll” you should expect a CNF input file, which you solve using the DPLL algorithm printing the
solution to console

In mode “solver” you should expect a BNF input file, run cnf mode, but instead of printing, send the input
to dpll mode

Your program should exit gracefully and indicate as best as possible the problem in case of bad arguments or file.

DPLL solver

It should handle arbitrary CNF input and run DPLL as described in class, RN chapter 7.6, and also here. When
guessing, use the smallest lexicographic atom and guess True first. The output should be either: an assignment of
all atoms that satisfies the clauses, or ‘NO VALID ASSIGNMENT’.

Each line of the input file (when running in dpll mode) represents a sentence, with space separated atoms

Atoms are only alphanumeric [so no parenthesis or brackets as used in class

No punctuation is needed as in CNF every sentence is a disjunction

Except ! the negation operator which may be directly in front of an atom (no spaces)

So, the CNF sentences:

P v Q v ! W
! P v Q
W !
P v ! W

Would be written in input as simply:

P Q !W
!P Q
W !
P !W

And output:


In verbose node you should indicate each step taken, e.g.

easy case: unit literal W
easy case: pure literal Q=true
hard case: …