Arrow Research search

Author name cluster

Carsten Sinz

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.

15 papers
2 author rows

Possible papers

15

AIJ Journal 2016 Journal Article

SAT Race 2015

  • Tomáš Balyo
  • Armin Biere
  • Ashlin Iser
  • Carsten Sinz

Boolean satisfiability (SAT) solving is one of the most competitive research areas of theoretical computer science. The performance of state-of-the-art SAT solvers has been continuously improving in the last decades and has reached a level where SAT solvers can be employed to solve real world problems in fields such as hardware and software verification, automated planning and many others. One of the important driving forces of this progress are the yearly organized (since 2002) SAT competitions. In this paper we describe the 2015 SAT Race that featured the traditional sequential and parallel tracks (with 64 core computers) and introduced the Incremental Library Track, which is particularly interesting for developers of SAT based applications. We describe the 2015 SAT Race and provide a detailed analysis of its results.

Details DOI

SAT Conference 2015 Conference Paper

HordeSat: A Massively Parallel Portfolio SAT Solver

  • Tomás Balyo
  • Peter Sanders 0001
  • Carsten Sinz

Abstract A simple yet successful approach to parallel satisfiability (SAT) solving is to run several different (a portfolio of) SAT solvers on the input problem at the same time until one solver finds a solution. The SAT solvers in the portfolio can be instances of a single solver with different configuration settings. Additionally the solvers can exchange information usually in the form of clauses. In this paper we investigate whether this approach is applicable in the case of massively parallel SAT solving. Our solver is intended to run on clusters with thousands of processors, hence the name HordeSat. HordeSat is a fully distributed portfolio-based SAT solver with a modular design that allows it to use any SAT solver that implements a given interface. HordeSat has a decentralized design and features hierarchical parallelism with interleaved communication and search. We experimentally evaluated it using all the benchmark problems from the application tracks of the 2011 and 2014 International SAT Competitions. The experiments demonstrate that HordeSat is scalable up to hundreds or even thousands of processors achieving significant speedups especially for hard instances.

Details

AIJ Journal 2015 Journal Article

Overview and analysis of the SAT Challenge 2012 solver competition

  • Adrian Balint
  • Anton Belov
  • Matti Järvisalo
  • Carsten Sinz

Programs for the Boolean satisfiability problem (SAT), i. e. , SAT solvers, are nowadays used as core decision procedures for a wide range of combinatorial problems. Advances in SAT solving during the last 10–15 years have been spurred by yearly solver competitions. In this article, we report on the main SAT solver competition held in 2012, SAT Challenge 2012. Besides providing an overview of how SAT Challenge 2012 was organized, we present an in-depth analysis of key aspects of the results obtained during the competition.

Details DOI

SAT Conference 2015 Conference Paper

Recognition of Nested Gates in CNF Formulas

  • Ashlin Iser
  • Norbert Manthey
  • Carsten Sinz

Abstract We present a new algorithm to efficiently extract information about nested functional dependencies between variables of a formula in CNF. Our algorithm uses the relation between gate encodings and blocked sets in CNF formulas. Our notion of “gate” emphasizes this relation. The presented algorithm is central to our new tool, cnf2aig, that produces equisatisfiable and-inverter-graphs (AIGs) from CNF formulas. We compare the novel algorithm to earlier approaches and show that the produced AIG are generally more succinct and use less input variables. As the gate-detection is related to the structure of input formulas, we furthermore analyze the gate-detection before and after applying preprocessing techniques.

Details

SAT Conference 2013 Conference Paper

Minimizing Models for Tseitin-Encoded SAT Instances

  • Ashlin Iser
  • Carsten Sinz
  • Mana Taghdiri

Abstract Many applications of SAT solving can profit from minimal models—a partial variable assignment that is still a witness for satisfiability. Examples include software verification, model checking, and counterexample-guided abstraction refinement. In this paper, we examine how a given model can be minimized for SAT instances that have been obtained by Tseitin encoding of a full propositional logic formula. Our approach uses a SAT solver to efficiently minimize a given model, focusing on only the input variables. Experiments show that some models can be reduced by over 50 percent.

Details

SAT Conference 2012 Conference Paper

Optimizing MiniSAT Variable Orderings for the Relational Model Finder Kodkod - (Poster Presentation)

  • Ashlin Iser
  • Mana Taghdiri
  • Carsten Sinz

Abstract It is well-known that the order in which variables are processed in a DPLL-style SAT algorithm can have a substantial effect on its run-time. Different heuristics, such as VSIDS [2], have been proposed in the past to obtain good variable orderings. However, most of these orderings are general-purpose and do not take into account the additional structural information that is available on a higher problem description level. Thus, structural, problem-dependent strategies have been proposed (see, e. g. , the work of Marques-Silva and Lynce on special strategies for cardinality constraints [1]).

Details

SAT Conference 2009 Conference Paper

Problem-Sensitive Restart Heuristics for the DPLL Procedure

  • Carsten Sinz
  • Ashlin Iser

Abstract Search restarts have shown great potential in speeding up SAT solvers based on the DPLL procedure. However, most restart policies presented so far do not take the problem structure into account. In this paper we present several new problem-sensitive restart heuristics. They all observe different search parameters like conflict level or backtrack level over time and, based on their development, decide whether to perform a restart or not. We also present a Java tool to visualize these search parameters on a given SAT instance over time in order to analyze existing heuristics and develop new one.

Details

SAT Conference 2008 Conference Paper

A New Bound for an NP-Hard Subclass of 3-SAT Using Backdoors

  • Stephan Kottler
  • Michael Kaufmann 0001
  • Carsten Sinz

Abstract Knowing a Backdoor Set B for a given Sat instance, satisfiability can be decided by only examining each of the 2 | B | truth assignments of the variables in B. However, one problem is to efficiently find a small backdoor up to a particular size and, furthermore, if no backdoor of the desired size could be found, there is in general no chance to conclude anything about satisfiability. In this paper we introduce a complete deterministic algorithm for an NP-hard subclass of 3- Sat, that is also a subclass of Mixed Horn Formulas (MHF). For an instance of the described class the absence of two particular kinds of backdoor sets can be used to prove unsatisfiability. The upper bound of this algorithm is O ( p ( n )*1. 427 n ) which is less than the currently best upper bound for deterministic algorithms for 3- Sat and MHF.

Details

SAT Conference 2008 Conference Paper

Computation of Renameable Horn Backdoors

  • Stephan Kottler
  • Michael Kaufmann 0001
  • Carsten Sinz

Abstract Satisfiability of real-world Sat instances can be often decided by focusing on a particular subset of variables - a so-called Backdoor Set. In this paper we suggest two algorithms to compute Renameable Horn deletion backdoors. Both methods are based on the idea to transform the computation into a graph problem. This approach could be used as a preprocessing to solve hard real-world Sat instances. We also give some experimental results of the computations of Renameable Horn backdoors for several real-world instances.

Details

SAT Conference 2007 Conference Paper

A First Step Towards a Unified Proof Checker for QBF

  • Toni Jussila
  • Armin Biere
  • Carsten Sinz
  • Daniel Kroening
  • Christoph M. Wintersteiger

Abstract Compared to SAT, there is no simple concept of what a solution to a QBF problem is. Furthermore, as the series of QBF evaluations shows, the QBF solvers that are available often disagree. Thus, proof generation for QBF seems to be even more important than for SAT. In this paper we propose a new uniform proof format, which captures refutations and witnesses for a variety of QBF solvers, and is based on a novel extended resolution rule for QBF. Our experiments show the flexibility of this new format. We also identify shortcomings of our format and conjecture that a purely resolution based proof calculus is not powerful enough to trace the most efficient solvers.

Details

IS Journal 2007 Journal Article

Configuration

  • Carsten Sinz
  • Albert Haag
  • Nina Narodytska
  • Toby Walsh
  • Esther Gelle
  • Mihaela Sabin
  • Ulrich Junker
  • Barry O'Sullivan

Over the years, a whole sector of AI dealing with configuration problems has emerged, and since 1996, an annual configuration workshop has been held in affiliation with a major AI conference. This installment of Trends & Controversies presents essays from the configuration workshop held in August 2006 as part of ECAI in Riva del Garda, Italy.

Details DOI

SAT Conference 2006 Conference Paper

Extended Resolution Proofs for Symbolic SAT Solving with Quantification

  • Toni Jussila
  • Carsten Sinz
  • Armin Biere

Abstract Symbolic SAT solving is an approach where the clauses of a CNF formula are represented using BDDs. These BDDs are then conjoined, and finally checking satisfiability is reduced to the question of whether the final BDD is identical to false. We present a method combining symbolic SAT solving with BDD quantification (variable elimination) and generation of extended resolution proofs. Proofs are fundamental to many applications, and our results allow the use of BDDs instead of—or in combination with—established proof generation techniques like clause learning. We have implemented a symbolic SAT solver with variable elimination that produces extended resolution proofs. We present details of our implementation, called EBDDRES, which is an extension of the system presented in [1], and also report on experimental results.

Details

SAT Conference 2005 Conference Paper

DPvis - A Tool to Visualize the Structure of SAT Instances

  • Carsten Sinz
  • Edda-Maria Dieringer

Abstract We present DPvis, a Java tool to visualize the structure of SAT instances and runs of the DPLL (Davis-Putnam-Logemann-Loveland) procedure. DPvis uses advanced graph layout algorithms to display the problem’s internal structure arising from its variable dependency (interaction) graph. DPvis is also able to generate animations showing the dynamic change of a problem’s structure during a typical DPLL run. Besides implementing a simple variant of the DPLL algorithm on its own, DPvis also features an interface to MiniSAT, a state-of-the-art DPLL implementation. Using this interface, runs of MiniSAT can be visualized—including the generated search tree and the effects of clause learning. DPvis is supposed to help in teaching the DPLL algorithm and in gaining new insights in the structure (and hardness) of SAT instances.

Details

SAT Conference 2004 Conference Paper

Verifying the On-Line Help System of SIEMENS Magnetic Resonance Tomographs using SAT (Extended Abstract)

  • Carsten Sinz
  • Wolfgang Küchlin

Large-scale medical systems—like magnetic resonance tomographs—are manufactured with a steadily growing number of product options. Different model lines can be equipped with large numbers of supplementary equipment options like (gradient) coils, amplifiers, magnets or imaging devices. The diversity in service and maintenance procedures, which may be different for each of the many product instances, grows accordingly. Therefore, instead of having one common on-line service handbook for all medical devices, SIEMENS fragments the on-line documentation into small (help) packages, out of which a suitable subset is selected for each individual product instance. Selection of the packages is controlled by XML documents, but the conditions can be translated into Boolean Boolean formulae. To check whether the existing set of help packages is sufficient for all possible devices and service cases, we developed the HelpChecker tool. HelpChecker uses both SAT- and BDD-based methods to check the consistency and completeness of the on-line documentation and to generate small (counter-)examples for cases where verification conditions are violated.

Details

SAT Conference 2004 Conference Paper

Visualizing the Internal Structure of SAT Instances (Preliminary Report)

  • Carsten Sinz

Modern algorithms for the SAT problem reveal an almost tractable behavior on “real-world” instances. This is frequently contributed to the fact that these instances possess an internal “structure” that hard problem instances do not exhibit. However, little is known about this internal structure. We therefore propose a visualization of the instance’s variable interaction graph (and of its dynamic change during a run of a SAT-solver) as a first step of an empirical research program to analyze the problem structure. We present first results of such an analysis on instances of bounded model checking benchmark problems.

Details