source: vis_dev/vis-2.3/share/help/cnf_satCmd.txt @ 43

Last change on this file since 43 was 14, checked in by cecile, 13 years ago

vis2.3
File size: 907 bytes
Line 
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.