Line | |
---|
1 | |
---|
2 | cnf_sat - Perform SAT solving with CNF input |
---|
3 | _________________________________________________________________ |
---|
4 | |
---|
5 | cnf_sat [-h] [-a <assgined_filename>] [-f <output_filename>] [-t |
---|
6 | <timeout>] [-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 |
---|
12 | is built from the CNF clauses. If the monolithic BDD is built then we |
---|
13 | can conclude SAT or UNSAT, otherwise the normal SAT algorithm is |
---|
14 | invoked. |
---|
15 | |
---|
16 | -t <timeOutPeriod> |
---|
17 | Specify the time out period (in seconds) after which the command |
---|
18 | aborts. By default this option is set to infinity. |
---|
19 | |
---|
20 | -f <output_filename> |
---|
21 | Specify the output filename to save the satisfying assignments and the |
---|
22 | statistics of SAT solving. |
---|
23 | _________________________________________________________________ |
---|
24 | |
---|
25 | Last updated on 20050519 10h16 |
---|
Note: See
TracBrowser
for help on using the repository browser.