|
UCSB circuit SAT solver |
|
- A Circuit SAT Solver Based Upon Signal Correlation Guided Learning - |
| C-SAT source code is available Here.
You can also download the executable version for Linux
and Solaris.
When results are published using our tool, please refer to the two
papers below: The readme file is available Here. C-SAT is a circuit sat solver implemented in C++. This solver is maintained by Feng Lu. We call it "a CIRCUIT sat solver," instead of "a SAT solver" because our solver operates directly on circuits, rather than on those examples in CNF. Moreover, our solver performs the best if the input is given in multi-level circuit format. C-SAT implements a new type of learning approach called Signal Correlation Guided Learning. Please refer to the papers above for the detail. Two forms of the signal correlation guided learning is included in this version: implicit learning and explicit learning. The current solver default is using the implicit learning. Using the option "-e" will invoke the explicit learning. Using the option "-b" will turn off the default implicit learning and hence, the solver will behave similarly to zChaff. C-SAT with the explicit learning is particularly efficient with the multi-level circuit unsatisfiable examples. For example, in the case of c6288 example, only with the "-e" option will the solver complete the run. Without the "-e" option, it will not finish. Our solver takes the standard ".bench" format as inputs. If you want to use the CNF input examples, you need to convert them into the ".bench" format first. Sorry, we do not support the CNF format inputs.Moreover, if your circuit examples are obtained from CNF inputs, since they are not the original multi-level circuits, the explicit learning will not be efficient. In these cases, implicit learning is usually better. Thank you for your interest in this circuit SAT solver. Feng Lu, PhD student, ECE, UCSB |