Saturday, February 12, 2011

Idea 50: On Demand Boolean Satisfiability Cloud Solver

The Boolean satisfiability problem, though barely encountered in every lives, has wide applications in software engineering and mathematical optimizations, in particular the problem of formally verifying the correctness of software and hardware. See the wikipedia page for an introduction, and paper written by Joao Marques-Silva on "Practical applications of boolean satisfiability".

The idea is to provide a web service, such that anyone can input a Boolean expression in terms of conjunctive normal form (CNF), and instantaneousness obtain the result of whether the expression is satisfiable. For example, input the following expression:
(x1 + x5 + ~x3) (~x6 + ~x2) (x2 + x3 + x4) 
where '+' represents Boolean OR, and '~' represents Boolean complement; the result will be a satisfying assignment (one of many) to the 6 variables involved.

In addition to HTML web interface with manual input, a developer's API service will be provided, where software programs can make remote requests to the server and supply an encrypted string of Boolean expressions, while the server respond by solving the problem instance, a satisfying assignment in the satisfiable case and a simple "no" in the unsatisfiable case. In some cases, delay may be encountered if the problem instance is large and requires large computation time.

The business model is to charge based on the bandwidth of API usage, or the amount of CPU cycles involved.

Update: the SAT solver itself could be implemented using current programming language Erlang and deployed on a large set of computer nodes.