Implement a SAT solver from scratch.

Implement a SAT solver from scratch.

Implement a SAT solver from scratch. (See Russell and Norvig, Ch. 7 for
details on the SAT problem.) Your solver should read a satisability problem
in conjunctive normal form, in DIMACS format (see below), from standard
input. The output should be A satisying variable assignment, if one exists; or
UNSATISFIABLE, if there is no solution.
Your code does not need to be heavily optimized but should be able to solve
problems with hundreds of clauses and up 20 variables in at most a few seconds.
(State of the art solvers can handle problems with millions of clauses and tens
of thousands of variables.)
DIMACS CNF format is widely accepted as the standard format for boolean
formulas in CNF. Benchmarks listed on satlib.org, for instance, are in the DI-
MACS CNF format. An input le starts with comments (each line starts with
c). The number of variables and the number of clauses is dened by the line p
cnf variables clauses Each of the next lines species a clause: a positive literal
is denoted by the corresponding number, and a negative literal is denoted by
the corresponding negative number. The last number in a line should be zero.
Example 1: (x1 _ x2) ^ (:x1 _ :x2)
Input:
c example1.cnf
p cnf 2 2
1 2 0
-1 -2 0
Output:
1 -2
Example 2: (x1 _ x2) ^ :x1 ^ :x2
Input:
c example2.cnf
p cnf 2 3
1 2 0
-1 0
-2 0
Output:
UNSATISFIABLE

不知