Non Increasing Variable Elimination Resolution
Resolution based formula simplifier
The Linux executable for NiVER SAT Preprocessor
NiVER takes an argument, the filename of a DIMACS-format CNF.
For example, "niver hanoi5.cnf ".
The simplified theory is written into a file named "outfile.cnf"
References
Sathiamoorthy Subbarayan and Dhiraj K Pradhan, NiVER: Non Increasing Variable Elimination Resolution for preprocessing SAT instances, Proceedings of The Seventh International Conference on Theory and Applications of Satisfiability Testing (SAT '04), May 2004 (PDF) (Slides)
Limited Increasing Variable Elimination Resolution
Resolution based formula simplifier
The Linux executable for LiVER SAT Preprocessor
LiVER takes two argument. The first one is the filename of a DIMACS-format CNF. The second one 'k' is the allowable increase in the total literal count when a variable is removed by VER.
For example, "liver hanoi5.cnf 10".
LiVER with k=0 is NiVER
The simplified theory is written into a file named "outfile.cnf"
Finds Average Number of implications by non-failed literals in a formula
The Linux executable for GetAveImps
GetAveImps takes an argument, the filename of a DIMACS-format CNF.
For example, "getaveimps hanoi5.cnf ".
The average number of implications by non-failed literals in the input formula is displayed in stdout
GetAveImps x86-linux executable
For comments and queries contact : Sathiamoorthy Subbarayan (sathi AT itu DOT dk)