Rev | Line | |
---|
[14] | 1 | |
---|
| 2 | cnf_sat - Perform SAT solving with CNF input |
---|
| 3 | _________________________________________________________________ |
---|
| 4 | |
---|
| 5 | cnf_sat [-h] [-a <assgined_filename>] [-f <output_filename>] [-t <timeout>] |
---|
| 6 | [-v <verbose>] [-b] <cnf_filename> |
---|
| 7 | |
---|
| 8 | Perform SAT solving with CirCUs after reading CNF file |
---|
| 9 | |
---|
| 10 | -b |
---|
| 11 | If the given CNF has small number of variables and clause then the BDD is |
---|
| 12 | built from the CNF clauses. If the monolithic BDD is built then we can |
---|
| 13 | conclude SAT or UNSAT, otherwise the normal SAT algorithm is invoked. |
---|
| 14 | |
---|
| 15 | -t <timeOutPeriod> |
---|
| 16 | Specify the time out period (in seconds) after which the command aborts. By |
---|
| 17 | default this option is set to infinity. |
---|
| 18 | |
---|
| 19 | -f <output_filename> |
---|
| 20 | Specify the output filename to save the satisfying assignments and the |
---|
| 21 | statistics of SAT solving. |
---|
| 22 | _________________________________________________________________ |
---|
| 23 | |
---|
| 24 | Last updated on 20100410 00h02 |
---|
Note: See
TracBrowser
for help on using the repository browser.