Implemented interface to MiniSAT to refute/find models for quantifier-free formulas and sets of clauses.
Added sequence of quantifer-free test formulas: The pigeon hole principle.

Interface in CLI
================
miniSATsolve: HOLFormula => Option[Interpretation] - obtain a model for a quantifier-free formula using MiniSAT
miniSATprove: HOLFormula => Boolean - check if a quantifier-free formula is valid using MiniSAT
PigeonHolePrinciple: Int, Int => FOLFormula - construct a quantifier-free formula representing the pigeon hole principle

The programmatic MiniSAT interface also allows sets of clauses as input.

Sample CLI session
==================

// Put 3 pigeons in 2 holes.
val valid = PigeonHolePrinciple(3, 2)
miniSATprove(valid)

// Put 3 pigeons in 3 holes
val notvalid = PigeonHolePrinciple(3, 3)
miniSATprove(notvalid)

// Get a model for the negated formula, i.e. a model
// where no hole contains two pigeons.
val m = miniSATsolve(Neg(notvalid)).get

// Query the model to see which pigeon sits in hole 1
val p1 = at.logic.testing.PigeonHolePrinciple.atom(1, 1)
val p2 = at.logic.testing.PigeonHolePrinciple.atom(2, 1)
val p3 = at.logic.testing.PigeonHolePrinciple.atom(3, 1)

m.interpret(p1) // Is pigeon 1 in hole 1?
m.interpret(p2) // Is pigeon 2 in hole 1?
m.interpret(p3) // Is pigeon 3 in hole 1?

// We can also interpret quantifier-free formulas.
m.interpret( And(p1, p2) )
m.interpret( Neg(notvalid) )



git-svn-id: http://gapt.googlecode.com/svn/trunk/source@1559 85d21ef8-add0-11de-ae77-5bfb9c5a3f34