Author name cluster

Marko Samer

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

8 papers

2 author rows

SAT Conference 2009 Conference Paper

Encoding Treewidth into SAT

Marko Samer
Helmut Veith

Abstract One of the most important structural parameters of graphs is treewidth, a measure for the “tree-likeness” and thus in many cases an indicator for the hardness of problem instances. The smaller the treewidth, the closer the graph is to a tree and the more efficiently the underlying instance often can be solved. However, computing the treewidth of a graph is NP -hard in general. In this paper we propose an encoding of the decision problem whether the treewidth of a given graph is at most k into the propositional satisfiability problem. The resulting SAT instance can then be fed to a SAT solver. In this way we are able to improve the known bounds on the treewidth of several benchmark graphs from the literature.

Details

AAAI Conference 2008 Conference Paper

Backdoor Trees

Marko Samer

The surprisingly good performance of modern satisfiability (SAT) solvers is usually explained by the existence of a certain “hidden structure” in real-world instances. We introduce the notion of backdoor trees as an indicator for the presence of a hidden structure. Backdoor trees refine the notion of strong backdoor sets, taking into account the relationship between backdoor variables. We present theoretical and empirical results. Our theoretical results are concerned with the computational complexity of detecting small backdoor trees. With our empirical results we compare the size of backdoor trees against the size of backdoor sets for real-world SAT instances and random 3SAT instances of various density. The results indicate that backdoor trees amplify the properties that have been observed for backdoor sets.

PDF Details

LPAR Conference 2008 Conference Paper

Variable Dependencies of Quantified CSPs

Marko Samer

Abstract Quantified constraint satisfaction extends classical constraint satisfaction by a linear order of the variables and an associated existential or universal quantifier to each variable. In general, the semantics of the quantifiers does not allow to change the linear order of the variables arbitrarily without affecting the truth value of the instance. In this paper we investigate variable dependencies that are caused by the influence of the relative order between these variables on the truth value of the instance. Several approaches have been proposed in the literature for identifying such dependencies in the context of quantified Boolean formulas. We generalize these ideas to quantified constraint satisfaction and present new concepts that allow a refined analysis.

Details

LPAR Conference 2007 Conference Paper

Algorithms for Propositional Model Counting

Marko Samer
Stefan Szeider

Abstract We present algorithms for the propositional model counting problem #SAT. The algorithms are based on tree-decompositions of graphs associated with the given CNF formula, in particular primal, dual, and incidence graphs. We describe the algorithms in a coherent fashion that admits a direct comparison of their algorithmic advantages. We analyze and discuss several aspects of the algorithms including worst-case time and space requirements and simplicity of implementation. The algorithms are described in sufficient detail for making an implementation reasonably easy.

Details

SAT Conference 2007 Conference Paper

Backdoor Sets of Quantified Boolean Formulas

Marko Samer
Stefan Szeider

Abstract We generalize the notion of backdoor sets from propositional formulas to quantified Boolean formulas in conjunctive normal form (QCNF). We develop parameterized algorithms that admit uniform polynomial time QCNF evaluation parameterized by the size of smallest strong backdoor sets. For our algorithms we develop a theory of variable dependency which is of independent interest. As a result, we obtain hierarchies of classes of tractable QCNF formulas with the classes of quantified Horn and quantified 2CNF formulas, respectively, at their first level, thus gradually generalizing these two prominent tractable classes. In contrast to known tractable classes based on bounded treewidth, the number of quantifier alternations of our classes is unbounded.

Details

LPAR Conference 2007 Conference Paper

On the Notion of Vacuous Truth

Marko Samer
Helmut Veith

Abstract The model checking community has proposed numerous definitions of vacuous satisfaction, i. e. , formal criteria which tell whether a temporal logic specification holds true on a system model for the intended reason. In this paper we attempt to study the notion of vacuous satisfaction from first principles. We show that despite the apparently vague formulation of the vacuity problem, most proposed notions of vacuity for temporal logic can be cast into a uniform and simple framework, and compare previous approaches to vacuity detection from this unified point of view.

Details

TIME Conference 2005 Conference Paper

Deterministic CTL Query Solving

Marko Samer
Helmut Veith

Temporal logic queries provide a natural framework to extend the realm of model checking from mere verification of engineers' specifications to computing previously unknown temporal properties of a system. Formally, temporal logic queries are patterns of temporal logic specifications which contain placeholders for subformulas; a solution to a temporal logic query is an instantiation which renders the specification true. In this paper, we investigate temporal logic queries that can be solved deterministically, i. e. , solving such queries can be reduced in a deterministic manner to solving their subqueries at appropriate system states. We show that this kind of determinism is intimately related to the notion of intermediate collecting queries studied by the authors in previous work. We describe a large class of deterministically solvable CTL queries and devise a BDD-based symbolic algorithm for this class.

Details

CSL Conference 2003 Conference Paper

Validity of CTL Queries Revisited

Marko Samer
Helmut Veith

Abstract We systematically investigate temporal logic queries in model checking, adding to the seminal paper by William Chan at CAV 2000. Chan’s temporal logic queries are CTL specifications where one unspecified subformula is to be filled in by the model checker in such a way that the specification becomes true. Chan defined a fragment of CTL queries called \(\mbox{CTL}^{v}\) which guarantees the existence of a unique strongest solution. The starting point of our paper is a counterexample to this claim. We then show how the research agenda of Chan can be realized by modifying his fragment appropriately. To this aim, we investigate the criteria required by Chan, and define two new fragments \(\mbox{CTL}^{v}_{new}\) and \(\mbox{CTL}^{d}\) where the first is the one originally intended; the latter fragment also provides unique strongest solutions where possible but admits also cases where the set of solutions is empty.

Details