Implement a SAT solver from scratch.(See Russell and Norvig,

Implement a SAT solver from scratch.(See Russell and Norvig,Ch.7 for
details on the SAT problem.) Your solver should read a satis\x0cability problem
in conjunctive normal form,in DIMACS format (see below),from standard
input.The output should be A satis\x0cying 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 \x0cle starts with comments (each line starts with
c).The number of variables and the number of clauses is de\x0cned by the line p
cnf variables clauses Each of the next lines speci\x0ces 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
有人知道怎麼做吗?那个output是什麼回事

Implement a SAT solver from scratch.(See Russell and Norvig,Ch.7 for
details on the SAT problem.) Your solver should read a satis\x0cability problem
in conjunctive normal form,in DIMACS format (see below),from standard
input.The output should be A satis\x0cying 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 \x0cle starts with comments (each line starts with
c).The number of variables and the number of clauses is de\x0cned by the line p
cnf variables clauses Each of the next lines speci\x0ces 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