Determining the clique-width or the linear clique-width of an undirected graph reduces to a Boolean satisfiability problem (a SAT problem in short) that can be solved for graphs of moderate size, depending on the available solver. This method is due to Heule and Szeider. We extend it to directed graphs, to vertex-labelled graphs and to the computation of relative clique-width. We have checked that certain proved upper-bounds to clique-width are actually reachable. We also propose open questions about upper-bounds to clique-width that this approach may help to solve. Every existential second-order graph property P has an NP-algorithm and can be formulated as a SAT problem constructed from the graph G for which P has to be checked. However, the resulting instance may be much too large to be solved in practice. We consider particular existential second-order sentences from which SAT problems of polynomial size can be easily constructed and, furthermore, that define hereditary graph properties, i.e. preserved by induced graph inclusion. Motivated by the search of minimal excluded graphs for hereditary graph properties (induced subgraph inclusion is here the relevant partial order on graphs), we examine cases where a SAT problem for an induced subgraph of a graph G can be obtained easily from the corresponding SAT problem for G .

Bounded rewriting for linear term rewriting systems has been defined in (I. Durand, G. Sénizergues, M. Sylvestre. Termination of linear bounded term rewriting systems. Proceedings of the 21st International Conference on Rewriting Techniques and Applications) as a restriction of the usual notion of rewriting. We extend here this notion to the whole class of left-linear term rewriting systems, and we show that bounded rewriting is effectively inverse-recognizability preserving. The bounded class (BO) is, by definition, the set of left-linear systems for which every derivation can be replaced by a bottom-up derivation. The class BO contains (strictly) several classes of systems which were already known to be inverse-recognizability preserving: the left-linear growing systems, and the inverse right-linear finite-path overlapping systems.

For the whole class of linear term rewriting systems and for each integer k, we define k-bounded rewriting as a restriction of the usual notion of rewriting. We show that the k-bounded uniform termination, the k-bounded termination, the inverse k-bounded uniform, and the inverse k-bounded problems are decidable. The k-bounded class (BO(k)) is, by definition, the set of linear systems for which every derivation can be replaced by a k-bounded derivation. In general, for BO(k) systems, the uniform (respectively inverse uniform) k-bounded termination problem is not equivalent to the uniform (resp. inverse uniform) termination problem, and the k-bounded (respectively inverse k-bounded) termination problem is not equivalent to the termination (respectively inverse termination) problem. This leads us to define more restricted classes for which these problems are equivalent: the classes BOLP(k) of k-bounded systems that have the length preservation property. By definition, a system is BOLP(k) if every derivation of length n can be replaced by a k-bounded derivation of length n. We define the class BOLP of bounded systems that have the length preservation property as the union of all the BOLP(k) classes. The class BOLP contains (strictly) several already known classes of systems: the inverse left-basic semi-Thue systems, the linear growing term rewriting systems, the inverse Linear-Finite-Path-Ordering systems, the strongly bottom-up systems.

We describe an application of partial evaluation to the optimization of Equational Logic programs.Our method treats the right-hand sides of reduction rules as partial input to subsequent reduction steps, allowing us to produce specialized forms of the rewriting system require complicated interpreters or semantic analysis.