A stand-alone application for converting

SAT DIMACS formulas to CNF

I have developed a SAT-based approach for the synthesis of fault-tolerant distributed programs. In particular, there exist many cases in the synthesis of fault-tolerant programs where we verify some properties of the program being synthesized. In our original approach, we perform such verifications exhaustively, whereas in the SAT-based approach we use state-of-the-art SAT solvers to achieve this goal.

Towards implementing our SAT-based method, we encode the verification problems in terms of DIMACS sat format. Before verifying the satisfiability of an encoded sat formula (i.e., verifying a property during the synthesis), we have to convert the sat formula to CNF format. To achieve this goal, I have studied the approach taken in Alloy for converting SAT to CNF format. 

The part of the Alloy code that converts SAT format to CNF has been developed on the CygWin platform where a .dll library provides a Linux-like environment for Windows. Since the efficiency of conversion is very important in the synthesis, I have been motivated with the idea of porting the code of the SAT2CNF layer in Alloy to Windows environment WITHOUT using CygWin. What you find here in the page is a stand-alone .EXE application for WIN32 platform that does not use CygWin.dll

Drop me a line (aebnenas at mtu dot edu) and I will send you the sat2cnf.exe file