Heya, Raphael Hertzog <hertzog@debian.org> writes: >> * What do you think of the advantages and improvements that I point >> out? > To me it looks great but I have no experience with SAT solver and I > wonder whether the sheer amount of predicates that it will have to handle > will not result in something dog-slow. I am pretty sure that this is not the case. SAT solvers are extremely efficient and reduction to SAT has replaced many specialised search algorithms because of its efficiency. Apart from that, one can always feed complex instances back to the SAT Race, making hundreds of researchers fine-tune their tools on the specific problem structure... However, finding minimal unsatisfiable cores (which are basically needed to get output for the "A might not migrate because of ..." bits) is harder, especially if they have an even weaker definition as in the MAX-SAT setting. For that, i would recommend reviewing the current literature. Marc
Attachment:
pgp6hG6hJskKJ.pgp
Description: PGP signature