search

gaoyuanning / aic-expresso

Automatically exported from code.google.com/p/aic-expresso
0 stars 0 forks source link

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

Open GoogleCodeExporter opened 8 years ago

GoogleCodeExporter commented 8 years ago 
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 commented 8 years ago

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

GoogleCodeExporter commented 8 years ago

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