cnf_sat

cnf_sat - Perform SAT solving with CNF input

cnf_sat [-h] [-a <assgined_filename>] [-f <output_filename>] [-t <timeout>] [-v <verbose>] [-b] <cnf_filename>

Perform SAT solving with CirCUs after reading CNF file

-b

If the given CNF has small number of variables and clause then the BDD is built from the CNF clauses. If the monolithic BDD is built then we can conclude SAT or UNSAT, otherwise the normal SAT algorithm is invoked.

-t <timeOutPeriod>

Specify the time out period (in seconds) after which the command aborts. By default this option is set to infinity.

-f <output_filename>

Specify the output filename to save the satisfying assignments and the statistics of SAT solving.

Last updated on 20050519 00h50