Arrow Research search

Author name cluster

Anton Belov

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.

14 papers
2 author rows

Possible papers

14

ICRA Conference 2018 Conference Paper

Performance Indicator for Benchmarking Force-Controlled Robots

  • Roland Behrens
  • Anton Belov
  • Maik Poggendorf
  • Felix Penzlin
  • Magnus Hanses
  • Emily Jantz
  • Norbert Elkmann

Robot-based sensitive assembly is a recent and growing trend in robotics. Force-controlled robots are expected to interact with an unknown environment using solely force feedback information. In general, the exact contact is difficult to predict due to various impact factors, such as the dynamics of the interaction, work-piece stiffness and geometry, the robot's configuration, and the efficiency of the control algorithm. Currently, there is no general indicator for evaluating the performance of a force-controlled robot. This work presents a concept of such a performance indicator. In order to test the proposed concept for comparison, an experimental setup is presented that simulates a contour-following task under force control. This setup is used to test two robots with different force-controllers and control principles, namely direct force and impedance control. The results indicate good applicability of the proposed performance indicator to benchmark force-controlled robots, and this is extensively discussed.

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

AIJ Journal 2014 Journal Article

Algorithms for computing minimal equivalent subformulas

  • Anton Belov
  • Mikoláš Janota
  • Inês Lynce
  • Joao Marques-Silva

Knowledge representation and reasoning using propositional logic is an important component of AI systems. A propositional formula in Conjunctive Normal Form (CNF) may contain redundant clauses — clauses whose removal from the formula does not affect the set of its models. Identification of redundant clauses is important because redundancy often leads to unnecessary computation, wasted storage, and may obscure the structure of the problem. A formula obtained by the removal of all redundant clauses from a given CNF formula F is called a Minimal Equivalent Subformula (MES) of F. This paper proposes a number of efficient algorithms and optimization techniques for the computation of MESes. Previous work on MES computation proposes a simple algorithm based on iterative application of the definition of a redundant clause, similar to the well-known deletion-based approach for the computation of Minimal Unsatisfiable Subformulas (MUSes). This paper observes that, in fact, most of the existing algorithms for the computation of MUSes can be adapted to the computation of MESes. However, some of the optimization techniques that are crucial for the performance of the state-of-the-art MUS extractors cannot be applied in the context of MES computation, and thus the resulting algorithms are often not efficient in practice. To address the problem of efficient computation of MESes, the paper develops a new class of algorithms that are based on the iterative analysis of subsets of clauses, and a lightweight pruning technique based on the computation of backbones. The experimental results, obtained on representative problem instances, confirm the effectiveness of the proposed methods. The experimental results also reveal that many CNF instances obtained from the practical applications of SAT exhibit a large degree of redundancy.

Details DOI

SAT Conference 2014 Conference Paper

MUS Extraction Using Clausal Proofs

  • Anton Belov
  • Marijn J. H. Heule
  • João Marques-Silva 0001

Abstract Recent work introduced an effective method for extraction of reduced unsatisfiable cores of CNF formulas as a by-product of validation of clausal proofs emitted by conflict-driven clause learning SAT solvers. In this paper, we demonstrate that this method for trimming CNF formulas can also benefit state-of-the-art tools for the computation of a Minimal Unsatisfiable Subformula (MUS). Furthermore, we propose a number of techniques that improve the quality of trimming, and demonstrate a significant positive impact on the performance of MUS extractors from the improved trimming.

Details

IJCAI Conference 2013 Conference Paper

On Computing Minimal Correction Subsets

  • Joao Marques-Silva
  • Federico Heras
  • Mikolas Janota
  • Alessandro Previti
  • Anton Belov

A set of constraints that cannot be simultaneously satisfied is over-constrained. Minimal relaxations and minimal explanations for over-constrained problems find many practical uses. For Boolean formulas, minimal relaxations of over-constrained problems are referred to as Minimal Correction Subsets (MCSes). MCSes find many applications, including the enumeration of MUSes. Existing approaches for computing MCSes either use a Maximum Satisfiability (MaxSAT) solver or iterative calls to a Boolean Satisfiability (SAT) solver. This paper shows that existing algorithms for MCS computation can be inefficient, and so inadequate, in certain practical settings. To address this problem, this paper develops a number of novel techniques for improving the performance of existing MCS computation algorithms. More importantly, the paper proposes a novel algorithm for computing MCSes. Both the techniques and the algorithm are evaluated empirically on representative problem instances, and are shown to yield the most efficient and robust solutions for MCS computation.

PDF Details DOI

SAT Conference 2013 Conference Paper

Parallel MUS Extraction

  • Anton Belov
  • Norbert Manthey
  • João Marques-Silva 0001

Abstract Parallelization is a natural direction towards the improvements in the scalability of algorithms for the computation of Minimally Unsatisfiable Subformulas (MUSes), and group-MUSes, of CNF formulas. In this paper we propose and analyze a number of approaches to parallel MUS computation. Just as it is the case with the parallel CDCL-based SAT solving, the communication, i. e. the exchange of learned clauses between the solvers running in parallel, emerges as an important component of parallel MUS extraction algorithms. However, in the context of MUS computation the communication might be unsound. We argue that the assumption-based approach to the incremental CDCL-based SAT solving is the key enabling technology for effective sound communication in the context of parallel MUS extraction, and show that fully unrestricted communication is possible in this setting. Furthermore, we propose a number of techniques to improve the quality of communication, as well as the quality of job distribution in the parallel MUS extractor. We evaluate the proposed techniques empirically on industrially-relevant instances of both plain and group MUS problems, and demonstrate significant (up to an order of magnitude) improvements due to the parallelization.

Details

LPAR Conference 2013 Conference Paper

SAT-Based Preprocessing for MaxSAT

  • Anton Belov
  • António Morgado 0001
  • João Marques-Silva 0001

Abstract State-of-the-art algorithms for industrial instances of MaxSAT problem rely on iterative calls to a SAT solver. Preprocessing is crucial for the acceleration of SAT solving, and the key preprocessing techniques rely on the application of resolution and subsumption elimination. Additionally, satisfiability-preserving clause elimination procedures are often used. Since MaxSAT computation typically involves a large number of SAT calls, we are interested in whether an input instance to a MaxSAT problem can be preprocessed up-front, i. e. prior to running the MaxSAT solver, rather than (or, in addition to) during each iterative SAT solver call. The key requirement in this setting is that the preprocessing has to be sound, i. e. so that the solution can be reconstructed correctly and efficiently after the execution of a MaxSAT algorithm on the preprocessed instance. While, as we demonstrate in this paper, certain clause elimination procedures are sound for MaxSAT, it is well-known that this is not the case for resolution and subsumption elimination. In this paper we show how to adapt these preprocessing techniques to MaxSAT. To achieve this we recast the MaxSAT problem in a recently introduced labelled-CNF framework, and show that within the framework the preprocessing techniques can be applied soundly. Furthermore, we show that MaxSAT algorithms restated in the framework have a natural implementation on top of an incremental SAT solver. We evaluate the prototype implementation of a MaxSAT algorithm WMSU1 in this setting, demonstrate the effectiveness of preprocessing, and show overall improvement with respect to non-incremental versions of the algorithm on some classes of problems.

Details

SAT Conference 2012 Conference Paper

On Efficient Computation of Variable MUSes

  • Anton Belov
  • Alexander Ivrii
  • Arie Matsliah
  • João Marques-Silva 0001

Abstract In this paper we address the following problem: given an unsatisfiable CNF formula \({\mathcal{F}}\), find a minimal subset of variables of \({\mathcal{F}}\) that constitutes the set of variables in some unsatisfiable core of \({\mathcal{F}}\). This problem, known as variable MUS (VMUS) computation problem, captures the need to reduce the number of variables that appear in unsatisfiable cores. Previous work on computation of VMUSes proposed a number of algorithms for solving the problem. However, the proposed algorithms lack all of the important optimization techniques that have been recently developed in the context of (clausal) MUS computation. We show that these optimization techniques can be adopted for VMUS computation problem and result in multiple orders magnitude speed-ups on industrial application benchmarks. In addition, we demonstrate that in practice VMUSes can often be computed faster than MUSes, even when state-of-the-art optimizations are used in both contexts.

Details

IJCAI Conference 2011 Conference Paper

Depth-Driven Circuit-Level Stochastic Local Search for SAT

  • Anton Belov
  • Matti J
  • auml; rvisalo
  • Zbigniew Stachniak

We develop a novel circuit-level stochastic local search (SLS) method D-CRSat for Boolean satisfiability by integrating a structure-based heuristic into the recent CRSat algorithm. D-CRSat significantly improves on CRSat on real-world application benchmarks on which other current CNF and circuit-level SLS methods tend to perform weakly. We also give an intricate proof of probabilistically approximate completeness for D-CRSat, highlighting key features of the method.

PDF Details DOI

SAT Conference 2011 Conference Paper

Minimally Unsatisfiable Boolean Circuits

  • Anton Belov
  • João Marques-Silva 0001

Abstract Automated reasoning tasks in many real-world domains involve analysis of redundancies in unsatisfiable instances of SAT. In CNF-based instances, some of the redundancies can be captured by computing a minimally unsatisfiable subset of clauses (MUS). However, the notion of MUS does not apply directly to non-clausal instances of SAT, particularly those that are represented as Boolean circuits. In this paper we identify certain types of redundancies in unsatisfiable Boolean circuits, and propose a number of algorithms to compute minimally unsatisfiable, that is, irredundant, subcircuits.

Details

SAT Conference 2010 Conference Paper

Improved Local Search for Circuit Satisfiability

  • Anton Belov
  • Zbigniew Stachniak

Abstract In this paper we describe a significant improvement to the justificationbased local search algorithm for circuit satisfiability proposed by Järvisalo et al [7]. By carefully combining local search with Boolean Constraint Propagation we achieve multiple orders of magnitude reduction in run-time on industrial and structured benchmark circuits, and, in some cases, performance comparable with complete SAT solvers.

Details

SAT Conference 2009 Conference Paper

Improving Variable Selection Process in Stochastic Local Search for Propositional Satisfiability

  • Anton Belov
  • Zbigniew Stachniak

Abstract This paper considers two methods for speeding-up stochastic local search SAT procedures. The first method aims at using the search history (represented by additional formulas derived at every state of the search process) to constrain the selection of candidate variables used to navigate through the search space of truth-value assignments. The second method uses the search history to allow multiple modifications of the current truth-value assignment in a single search step. Empirical studies of these two methods have demonstrated their effectiveness on structured and industrial SAT instances.

Details

SAT Conference 2008 Conference Paper

Speeding-Up Non-clausal Local Search for Propositional Satisfiability with Clause Learning

  • Zbigniew Stachniak
  • Anton Belov

Abstract In this paper we discuss search heuristics for non-clausal stochastic local search procedures for propositional satisfiability. These heuristics are based on a new method for variable selection as well as a novel clause learning technique for dynamic input formula simplification as well as for guiding the search for a model.

Details