Arrow Research search

Author name cluster

Nachum Dershowitz

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.

29 papers
2 author rows

Possible papers

29

AAAI Conference 2021 Conference Paper

Computational Visual Ceramicology: Matching Image Outlines to Catalog Sketches

  • Barak Itkin
  • Lior Wolf
  • Nachum Dershowitz

Field archeologists are called upon to identify potsherds, for which they rely on their professional experience and on reference works. We have developed a recognition method starting from images captured on site, which relies on the shape of the sherd’s fracture outline. The method sets up a new target for deep-learning, integrating information from points along inner and outer surfaces to learn about shapes. Training the classifiers required tackling multiple challenges that arose on account of our working with real-world archeological data: paucity of labeled data; extreme imbalance between instances of different categories; and the need to avoid neglecting rare classes and to take note of minute distinguishing features of some classes. The scarcity of training data was overcome by using synthetically-produced virtual potsherds and by employing multiple data-augmentation techniques. A novel form of training loss allowed us to overcome classification problems caused by under-populated classes and inhomogeneous distribution of discriminative features.

PDF Details

LPAR Conference 2018 Conference Paper

Graph Path Orderings

  • Nachum Dershowitz
  • Jean-Pierre Jouannaud

We define well-founded rewrite orderings on graphs and show that they can be used to show termination of a set of graph rewrite rules by verifying all their cyclic extensions. We then introduce the graph path ordering inspired by the recursive path ordering on terms and show that it is a well-founded rewrite ordering on graphs for which checking termination of a finite set of graph rewrite rules is decidable. Our ordering applies to arbitrary finite, directed, labeled, ordered multigraphs, hence provides a building block for rewriting with graphs, which should impact the many areas in which computations take place on graphs.

Details

SAT Conference 2015 Conference Paper

Hints Revealed

  • Jonathan Kalechstain
  • Vadim Ryvchin
  • Nachum Dershowitz

Abstract We propose a notion of hints, clauses that are not necessarily consistent with the input formula. The goal of adding hints is to speed up the SAT solving process. For this purpose, we provide an efficient general mechanism for hint addition and removal. When a hint is determined to be inconsistent, a hint-based partial resolution-graph of an unsatisfiable core is used to reduce the search space. The suggested mechanism is used to boost performance by adding generated hints to the input formula. We describe two specific hint-suggestion methods, one of which increases performance by 30% on satisfiable SAT ’13 competition instances and solves 9 instances not solved by the baseline solver.

Details

CSL Conference 2013 Conference Paper

Res Publica: The Universal Model of Computation (Invited Talk)

  • Nachum Dershowitz

We proffer a model of computation that encompasses a broad variety of contemporary generic models, such as cellular automata---including dynamic ones, and abstract state machines---incorporating, as they do, interaction and parallelism. We ponder what it means for such an intertwined system to be effective and note that the suggested framework is ideal for representing continuous-time and asynchronous systems.

Details

CSL Conference 2010 Conference Paper

Exact Exploration and Hanging Algorithms

  • Andreas Blass
  • Nachum Dershowitz
  • Yuri Gurevich

Abstract Recent analysis of sequential algorithms resulted in their axiomatization and in a representation theorem stating that, for any sequential algorithm, there is an abstract state machine (ASM) with the same states, initial states and state transitions. That analysis, however, abstracted from details of intra-step computation, and the ASM, produced in the proof of the representation theorem, may and often does explore parts of the state unexplored by the algorithm. We refine the analysis, the axiomatization and the representation theorem. Emulating a step of the given algorithm, the ASM, produced in the proof of the new representation theorem, explores exactly the part of the state explored by the algorithm. That frugality pays off when state exploration is costly. The algorithm may be a high-level specification, and a simple function call on the abstraction level of the algorithm may hide expensive interaction with the environment. Furthermore, the original analysis presumed that state functions are total. Now we allow state functions, including equality, to be partial so that a function call may cause the algorithm as well as the ASM to hang. Since the emulating ASM does not make any superfluous function calls, it hangs only if the algorithm does.

Details

SAT Conference 2007 Conference Paper

Towards a Better Understanding of the Functionality of a Conflict-Driven SAT Solver

  • Nachum Dershowitz
  • Ziyad Hanna
  • Alexander Nadel

Abstract We show that modern conflict-driven SAT solvers implicitly build and prune a decision tree whose nodes are associated with flipped variables. Practical usefulness of conflict-driven learning schemes, like 1UIP or All UIP, depends on their ability to guide the solver towards refutations associated with compact decision trees. We propose an enhancement of 1UIP that is empirically helpful for real-world industrial benchmarks.

Details

SAT Conference 2006 Conference Paper

A Scalable Algorithm for Minimal Unsatisfiable Core Extraction

  • Nachum Dershowitz
  • Ziyad Hanna
  • Alexander Nadel

Abstract We propose a new algorithm for minimal unsatisfiable core extraction, based on a deeper exploration of resolution-refutation properties. We provide experimental results on formal verification benchmarks confirming that our algorithm finds smaller cores than suboptimal algorithms; and that it runs faster than those algorithms that guarantee minimality of the core. (A more complete version of this paper may be found at arXiv. org/pdf/cs. LO/0605085.)

Details

LPAR Conference 2006 Conference Paper

Boolean Rings for Intersection-Based Satisfiability

  • Nachum Dershowitz
  • Jieh Hsiang
  • Guan-Shieng Huang
  • Daher Kaiss

Abstract A potential advantage of using a Boolean-ring formalism for propositional formulæ is the large measure of simplification it facilitates. We propose a combined linear and binomial representation for Boolean-ring polynomials with which one can easily apply Gaussian elimination and Horn-clause methods to advantage. We demonstrate that this framework, with its enhanced simplification, is especially amenable to intersection-based learning, as in recursive learning and the method of Stålmarck. Experiments support the idea that problem variables can be eliminated and search trees can be shrunk by incorporating learning in the form of Boolean-ring saturation.

Details

SAT Conference 2005 Conference Paper

A Clause-Based Heuristic for SAT Solvers

  • Nachum Dershowitz
  • Ziyad Hanna
  • Alexander Nadel

Abstract We propose a new decision heuristic for DPLL-based propositional SAT solvers. Its essence is that both the initial and the conflict clauses are arranged in a list and the next decision variable is chosen from the top-most unsatisfied clause. Various methods of initially organizing the list and moving the clauses within it are studied. Our approach is an extension of one used in Berkmin, and adopted by other modern solvers, according to which only conflict clauses are organized in a list, and a literal-scoring-based secondary heuristic is used when there are no more unsatisfied conflict clauses. Our approach, implemented in the 2004 version of zChaff solver and in a generic Chaff-based SAT solver, results in a significant performance boost on hard industrial benchmarks.

Details

SAT Conference 2005 Conference Paper

Bounded Model Checking with QBF

  • Nachum Dershowitz
  • Ziyad Hanna
  • Jacob Katz

Abstract Current algorithms for bounded model checking (BMC) use SAT methods for checking satisfiability of Boolean formulas. These BMC methods suffer from a potential memory explosion problem. Methods based on the validity of Quantified Boolean Formulas (QBF) allow an exponentially more succinct representation of the checked formulas, but have not been widely used, because of the lack of an efficient decision procedure for QBF. We evaluate the usage of QBF in BMC, using general-purpose SAT and QBF solvers. We also present a special-purpose decision procedure for QBF used in BMC, and compare our technique with the methods using general-purpose SAT and QBF solvers on real-life industrial benchmarks. Our procedure performs much better for BMC than the general-purpose QBF solvers, without incurring the space overhead of propositional SAT.

Details

LPAR Conference 2005 Conference Paper

The Four Sons of Penrose

  • Nachum Dershowitz

Abstract We distill Penrose’s argument against the “artificial intelligence premiss”, and analyze its logical alternatives. We then clarify the different positions one can take in answer to the question raised by the argument, skirting the issue of introspection per se.

Details

SAT Conference 2004 Conference Paper

Boolean Ring Satisfiability

  • Nachum Dershowitz
  • Jieh Hsiang
  • Guan-Shieng Huang
  • Daher Kaiss

We propose a method for testing satisfiability based on Boolean rings. It makes heavy use of simplification, but avoids the potential size increase associated with application of the distributive law by employing a combined linear and binomial representation. Several complexity results suggest why the method may be relatively effective in many cases. The framework is also amenable to learning from intersections, as in Stålmarck’s method. Some experiments have been undertaken.

Details

MFCS Conference 1997 Invited Paper

When are Two Rewrite Systems More than None?

  • Nachum Dershowitz

Abstract It is important for programs to have modular correctness properties. We look at non-deterministic programs expressed as term-rewriting systems (which compute normal forms of input terms) and consider the case where individual systems share constructors, but not defined symbols. We present some old and new sufficient conditions under which termination (existence of normal forms, regardless of computation strategy) and confluence (uniqueness) are preserved by such combinations.

Details

AAAI Conference 1990 Conference Paper

Inductive Synthesis of Equational Programs

  • Nachum Dershowitz

An equational approach to the synthesis of functional and logic programs is taken. Typically, a target program contains equations that are only true in the standard model of the given domain rules. To synthesize such programs, induction is necessary. We propose heuristics for generalizing from a sequence of deductive consequences. These are combined with rewrite-based methods of inductive proof to derive provably correct programs. a survey of rewriting, see (Dershowitz & Jouannaud 1990); for completion and its applications, see (Dershowitz 1989). Consider the following toy system S for addition and doubling (d) of natural numbers in unary notation: x+0 + x x + S(Y) + s(x+y) d(x) + x+x

PDF Details

FOCS Conference 1979 Conference Paper

Orderings for Term-Rewriting Systems

  • Nachum Dershowitz

Methods of proving that a term-rewriting system terminates are presented. They are based on the notion of "simplification orderings", orderings in which any term that is homeomorphically embeddable in another is smaller than the other. A particularly useful class of simplification orderings, the "recursive path orderings", is defined. Several examples of the use of such orderings in termination proofs are given.

Details