OptSAT

optsat: A Tool for Solving SAT Related Optimization Problems. Propositional satisfiability (SAT) is one of the most important and central problems in Artificial Intelligence and Computer Science. Basically, most SAT solvers are based on the well-known Davis-Logemann-Loveland (DLL) procedure. DLL is a decision procedure: given a SAT formula φ, it can decide if φ is satisfiable (and it can return a satisfying assignment μ), or not. Often, this is not suffi- cient, in that we would like μ to be also “optimal”, i.e., that has also to minimize/ maximize a given objective function. max-sat, min-one, distance-sat and their weighted versions are popular optimization problems. (In the following, φ is the input formula expressed as a set of clauses). Almost all the systems that can deal with these problems follow a classical branch&bound schema: whenever a satisfying assignment μ for φ with a cost c μ is found, the search goes on looking for another satisfying assignment with a lower (or higher, depending on the problem) cos