Integrate ability to run black box SAT solver's against propositionalized formulas in order to validate R_complete_simplify satisfiability logic

[GoogleCodeExporter]

Develop a set of utilities to allow the transformation of R_card formulas to a 
propositional representation that can be fed into a black box SAT solver to 
determine satisfiability. The target solver is to be SAT4J:

http://www.sat4j.org/ 

which also provides a basic mechanism for counting models:

http://www.sat4j.org/howto.php#models 

Additional utilities are to be developed for randomly generating formulas, 
passing them to the SAT solver and building up a known suite of 
satisfiable/unsatisfiable instances that can be used in a regression test suite 
for R_complete_simplify's satisfiability logic.

Original issue reported on code.google.com by ctjoreilly@gmail.com on 23 Apr 2013 at 5:40

[GoogleCodeExporter]

Original comment by ctjoreilly@gmail.com on 23 Apr 2013 at 5:48

• Changed state: Started

[GoogleCodeExporter]

Original comment by ctjoreilly@gmail.com on 16 May 2013 at 8:26

• Added labels: Milestone-Unscheduled