A study of approximation techniques for incremental SAT and MAX-SAT

Given a propositional formula F, the Propositional Satisfiability Problem (SAT) is to decide whether or not F is satisfiable. A literal is a propositional variable or its negation. If a propositional formula F is a conjunction over disjunctions of literals, it is in conjunctive normal form (CNF). The disjunctions of literals are called clauses. MAX-SAT is the optimization variant of SAT. For a given propositional formula in CNF, its objective is to find a truth assignment which satisfies the maximal number of clauses in a given formula.; We define an incremental SAT problem as a sequence of static SAT problems SAT0,···, SATi, SATi+1,···, SAT n each resulting from a change in the preceding one imposed by the "outside world". This change corresponds to the addition of new clauses. SATi+1 is obtained by performing an addition of clauses to SATi. Solving the incremental SAT problem consists of maintaining the satisfiability of the SAT formula anytime new clauses are added. We can define the incremental MAX-SAT problem similarly. Solving the incremental MAX-SAT problem is to find the truth assignment which satisfies the maximal number of clauses anytime new clauses are added.; An efficient GSAT implementation for incremental SAT and an improved GA implementation for incremental SAT are proposed in this thesis. An efficient GSAT implementation for MAX-SAT and incremental MAX-SAT is also proposed.; The experiments conducted on randomly generated instances as well as instances from the well known SAT library shows the efficiency of our algorithms.; A multi-agent system is a computational system where agents cooperate or compete with others to achieve some individual or collective task. Multi-agent systems are widely used to solve different problems in computer science. In this thesis, I propose new distributed algorithms for SAT and incremental SAT.