Recent research has shown that it is often preferable to encode real-world problems as propositional satisfiability (SAT) problems and then solve using a general purpose SAT solver. However, much of the valuable information and structure of these realistic problems is flattened out and hidden inside the corresponding Conjunctive Normal Form (CNF) encodings of the SAT domain. Recently, systematic SAT solvers have been progressively improved and are now able to solve many highly structured practical problems containing millions of clauses. In contrast, state-of-the-art Stochastic Local Search (SLS) solvers still have difficulty in solving structured problems, apparently because they are unable to exploit hidden structure as well as the systematic solvers. In this thesis, we study and evaluate different ways to effectively recognise, model and efficiently exploit useful structures hidden in realistic problems. A summary of the main contributions is as follows: 1. We first investigate an off-line processing phase that applies resolution-based pre-processors to input formulas before running SLS solvers on these problems. We report an extensive empirical examination of the impact of SAT pre-processing on the performance of contemporary SLS techniques. It emerges that while all the solvers examined do indeed benefit from pre-processing, the effects of different pre-processors are far from uniform across solvers and across problems. Our results suggest that SLS solvers need to be equipped with multiple pre-processors if they are ever to match the performance of systematic solvers on highly structured problems. [Part of this study was published at the AAAI-05 conference]. 2. We then look at potential approaches to bridging the gap between SAT and constraint satisfaction problem (CSP) formalisms. One approach has been to develop a many-valued SAT formalism (MV-SAT) as an intermediate paradigm between SAT and CSP, and then to translate existing highly efficient SAT solvers to the MV-SAT domain. In this study, we follow a different route, developing SAT solvers that can automatically recognise CSP structure hidden in SAT encodings. This allows us to look more closely at how constraint weighting can be implemented in the SAT and CSP domains. Our experimental results show that a SAT-based mechanism to handle weights, together with a CSP-based method to instantiate variables, is superior to other combinations of SAT and CSP-based approaches. In addition, SLS solvers based on this many-valued weighting approach outperform other existing approaches to handle many-valued CSP structures. [Part of this study was published at the AAAI-05 conference]. 3. Finally, we propose and evaluate six different schemes to encode temporal reasoning problems, in particular the Interval Algebra (IA) networks, into SAT CNF formulas. We then empirically examine the performance of local search as well as systematic solvers on the new temporal SAT representations, in comparison with solvers that operate on native IA representations. Our empirical results show that zChaff (a state-of-the-art complete SAT solver) together with the best IA-to-SAT encoding scheme, can solve temporal problems significantly faster than existing IA solvers working on the equivalent native IA networks. [Part of this study was published at the CP-05 workshop].

An NNF circuit is a directed acyclic graph (DAG), where each leaf is labelled with either true/false or a literal, and each inner node represents either a conjunction (∧) or a disjunction (∨). A decomposable NNF (DNNF) is an NNF satisfying the decomposabi- lity property for each conjunction node. The C-BDMC language generalizes the DNNF language. In a C-BDMC, the leaves can contain CNF formulae from a given base class C. In this paper, we focus only on renamable Horn formulae. We experimentally compare the sizes of d-BDMC and d-DNNF representations. We describe a new compilation langu- age, called cara DNNF (c-DNNF), that generalizes the DNNF language. A c-DNNF circuit can be considered as a compressed representation of a DNNF circuit. We present a new experimental knowledge compiler, called CaraCompiler, for converting a CNF formula into a d-BDMC or a (c)d-DNNF circuit. CaraCompiler is based on the state-of-the-art compiler D4. Also, we mention some extensions for the compiler D4, such as caching hypergraph cuts that can reduce the compilation times. 1

This work focuses on proposition of transfer of the expressions entered in the C pro­gramming language into DIMACS format and creation of program in programming language C++ making this transfer. This work contains a description of the C pro­gramming language and its operators. It also con­tains a description of the conjunctive normal form and a descri­ption of the DIMACS format. Following is a proposal for a program for the transfer of expression in the C programming language to the DIMACS format and description of reali­zation of program performing this transfer.