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.