C32SAT

C32SAT takes one boolean C expression as input. It can check whether it can be satisfied, is tautological, or can potentially be undefined according to the C99 standard.

News

Version 1.4.1 is available!

Version 1.4 is available!

Version 1.3 is the first public release.

Download

[ c32sat-1.4.1.tar.gz ]

These are the sources of our solver C32SAT. All C operators are supported, including multiplication and division, except pointer related operators. We are going to support them in future releases.

C32SAT uses a SAT solver as backend. At the moment the SAT solvers PicoSAT, NanoSAT, CompSAT and BoolForce are supported. Please note that the default SAT solver PicoSAT has not been published yet. Please configure C32SAT to work with one of the other solvers. Detailed installation instructions are contained in the README file. Note that C32SAT has been designed to run on UNIX-like systems.

License

C32SAT uses a BSD style license. In essence, you can use and modify the sources as you like provided that you acknowledge the origin of the software. More details can be found in the LICENSE file.

Background

C32SAT encodes one boolean C expression into propositional logic (SAT) in an eager way, sometimes referred to as bit blasting. The SAT encoding is functional, e.g. not relational, and thus in essence is performed by synthesizing the sub-expressions into circuits, similar to synthesis of VHDL or Verilog expressions. Internally the circuits are represented as an And-Inverter-Graph (AIG), before they are encoded into conjunctive normal form (CNF). Optionally the AIG and the CNF can be dumped instead of calling the backend SAT solver directly. C32SAT uses AIGER as dumping format for the internal AIG representation.

The tool is similar to Cogent, except that we support a different set of operators and use a functional SAT encoding. More details on C32SAT can be found in the Master Thesis of Robert Brummayer. Please note that the thesis describes C32SAT 1.0. Hence, the description is not up-to-date. The document update.pdf describes the most important changes of C32SAT. Finally, the document errata.pdf contains error corrections and additional notes to the thesis.

In July 2007 we presented C32SAT at CAV'07 in Berlin: [ Paper ] [ Talk ]