SAT-checker determines satisfiability for a set of propositional clauses. In the absence of an alternative approach that you prefer, use the DPLL algorithm described below.

We will prefer correct execution over performance, but performance should not be totally ignored.

The program should have one command-line argument which is the name of a file of clauses to read. That file will be in the format described by the DIMACS standard for CNF clauses.