MULTIRESOLUTION FOR SAT CHECKING

2001 ◽  
Vol 10 (04) ◽  
pp. 451-481 ◽  
Author(s):  
PHILIPPE CHATALIC ◽  
LAURENT SIMON
Keyword(s):  
Data Structures ◽  
System A ◽  
High Compression ◽  
Polynomial Size ◽  
Hard Problems ◽  
Exponential Size ◽  
Size Data

This paper presents a system based on new operators for handling sets of propositional clauses compactly represented by means of ZBDDs. The high compression power of such data structures allows efficient encodings of structured instances. A specialized operator for the distribution of sets of clauses is introduced and used for performing multiresolution on clause sets. Cut eliminations between sets of clauses of exponential size may then be performed using polynomial size data structures. The ZRES system, a new implementation of the Davis-Putnam procedure of 1960, solves two hard problems for resolution, that are currently out of the scope of the best SAT provers.

Lower Bounds on OBDD Proofs with Several Orders

2021 ◽  
Vol 22 (4) ◽  
pp. 1-30
Author(s):  
Sam Buss ◽  
Dmitry Itsykson ◽  
Alexander Knop ◽  
Artur Riazanov ◽  
Dmitry Sokolov
Keyword(s):  
Lower Bound ◽  
Lower Bounds ◽  
Communication Complexity ◽  
Multiparty Communication ◽  
Constant Degree ◽  
Polynomial Size ◽  
Explicit Constant ◽  
Open Question ◽  
System 1 ◽  
Exponential Size

This article is motivated by seeking lower bounds on OBDD(∧, w, r) refutations, namely, OBDD refutations that allow weakening and arbitrary reorderings. We first work with 1 - NBP ∧ refutations based on read-once nondeterministic branching programs. These generalize OBDD(∧, r) refutations. There are polynomial size 1 - NBP(∧) refutations of the pigeonhole principle, hence 1-NBP(∧) is strictly stronger than OBDD}(∧, r). There are also formulas that have polynomial size tree-like resolution refutations but require exponential size 1-NBP(∧) refutations. As a corollary, OBDD}(∧, r) does not simulate tree-like resolution, answering a previously open question. The system 1-NBP(∧, ∃) uses projection inferences instead of weakening. 1-NBP(∧, ∃ k is the system restricted to projection on at most k distinct variables. We construct explicit constant degree graphs G n on n vertices and an ε > 0, such that 1-NBP(∧, ∃ ε n ) refutations of the Tseitin formula for G n require exponential size. Second, we study the proof system OBDD}(∧, w, r ℓ ), which allows ℓ different variable orders in a refutation. We prove an exponential lower bound on the complexity of tree-like OBDD(∧, w, r ℓ ) refutations for ℓ = ε log n , where n is the number of variables and ε > 0 is a constant. The lower bound is based on multiparty communication complexity.

scholarly journals A Complexity Gap for Tree-Resolution

1999 ◽  
Vol 6 (29) ◽  
Author(s):  
Søren Riis
Keyword(s):  
Predicate Logic ◽  
Proof Complexity ◽  
Polynomial Size ◽  
Combinatorial Principles ◽  
Resolution Proofs ◽  
Symmetrical Group ◽  
Tree Resolution ◽  
Single Proposition ◽  
Exponential Size ◽  
Recent Idea

<p>It is shown that any sequence  psi_n of tautologies which expresses the<br />validity of a fixed combinatorial principle either is "easy" i.e. has polynomial<br />size tree-resolution proofs or is "difficult" i.e requires exponential<br />size tree-resolution proofs. It is shown that the class of tautologies which<br />are hard (for tree-resolution) is identical to the class of tautologies which<br />are based on combinatorial principles which are violated for infinite sets.<br />Actually it is shown that the gap-phenomena is valid for tautologies based<br />on infinite mathematical theories (i.e. not just based on a single proposition).<br />We clarify the link between translating combinatorial principles (or<br />more general statements from predicate logic) and the recent idea of using<br /> the symmetrical group to generate problems of propositional logic.<br />Finally, we show that it is undecidable whether a sequence  psi_n (of the<br />kind we consider) has polynomial size tree-resolution proofs or requires<br />exponential size tree-resolution proofs. Also we show that the degree of<br />the polynomial in the polynomial size (in case it exists) is non-recursive,<br />but semi-decidable.</p><p>Keywords: Logical aspects of Complexity, Propositional proof complexity,<br />Resolution proofs.</p><p> </p>

scholarly journals On the Power of Symmetric Linear Programs

2021 ◽  
Vol 68 (4) ◽  
pp. 1-35
Author(s):  
Albert Atserias ◽  
Anuj Dawar ◽  
Joanna Ochremiak
Keyword(s):  
Blow Up ◽  
Upper And Lower Bounds ◽  
Boolean Circuits ◽  
Linear Programs ◽  
Integer Points ◽  
Relational Structures ◽  
Polynomial Size ◽  
Compare And Contrast ◽  
Exponential Size ◽  
Planted Clique

We consider families of symmetric linear programs (LPs) that decide a property of graphs (or other relational structures) in the sense that, for each size of graph, there is an LP defining a polyhedral lift that separates the integer points corresponding to graphs with the property from those corresponding to graphs without the property. We show that this is equivalent, with at most polynomial blow-up in size, to families of symmetric Boolean circuits with threshold gates. In particular, when we consider polynomial-size LPs, the model is equivalent to definability in a non-uniform version of fixed-point logic with counting (FPC). Known upper and lower bounds for FPC apply to the non-uniform version. In particular, this implies that the class of graphs with perfect matchings has polynomial-size symmetric LPs, while we obtain an exponential lower bound for symmetric LPs for the class of Hamiltonian graphs. We compare and contrast this with previous results (Yannakakis 1991), showing that any symmetric LPs for the matching and TSP polytopes have exponential size. As an application, we establish that for random, uniformly distributed graphs, polynomial-size symmetric LPs are as powerful as general Boolean circuits. We illustrate the effect of this on the well-studied planted-clique problem.

New Design for a Differentially Pumped Hydration Chamber for a Siemens IA

1971 ◽  
Vol 29 ◽  
pp. 44-45
Author(s):  
R. C. Moretz ◽  
G. G. Hausner ◽  
D. F. Parsons
Keyword(s):  
Electron Microscopy ◽  
Water Vapor ◽  
Electron Diffraction ◽  
Water Vapor Pressure ◽  
Biological Materials ◽  
Thin Membrane ◽  
Reliable System ◽  
System A ◽  
Water Films ◽  
Aperture Opening

Electron microscopy and diffraction of biological materials in the hydrated state requires the construction of a chamber in which the water vapor pressure can be maintained at saturation for a given specimen temperature, while minimally affecting the normal vacuum of the remainder of the microscope column. Initial studies with chambers closed by thin membrane windows showed that at the film thicknesses required for electron diffraction at 100 KV the window failure rate was too high to give a reliable system. A single stage, differentially pumped specimen hydration chamber was constructed, consisting of two apertures (70-100μ), which eliminated the necessity of thin membrane windows. This system was used to obtain electron diffraction and electron microscopy of water droplets and thin water films. However, a period of dehydration occurred during initial pumping of the microscope column. Although rehydration occurred within five minutes, biological materials were irreversibly damaged. Another limitation of this system was that the specimen grid was clamped between the apertures, thus limiting the yield of view to the aperture opening.

High-resolution electron microscopy of Cu2O surfaces

1986 ◽  
Vol 44 ◽  
pp. 396-397
Author(s):  
V. Castano ◽  
W. Krakow
Keyword(s):  
High Resolution ◽  
Natural Extension ◽  
High Resolution Electron Microscopy ◽  
Point Of View ◽  
Initial Oxidation ◽  
System A ◽  
Resolution Electron ◽  
Surface Reconstructions ◽  
Atomic Surface ◽  
Au Thin Films

In non-UHV microscope environments atomic surface structure has been observed for flat-on for various orientations of Au thin films and edge-on for columns of atoms in small particles. The problem of oxidation of surfaces has only recently been reported from the point of view of high resolution microscopy revealing surface reconstructions for the Ag2O system. A natural extension of these initial oxidation studies is to explore other materials areas which are technologically more significant such as that of Cu2O, which will now be described.

Twin boundary structure of a Y-Ba-Cu-O superconductor

1989 ◽  
Vol 47 ◽  
pp. 168-169
Author(s):  
Yimei Zhu ◽  
Masaki Suenaga ◽  
R. L. Sabatini ◽  
Youwen Xu
Keyword(s):  
Twin Boundary ◽  
Fine Particles ◽  
Imaging Techniques ◽  
Fine Powder ◽  
Orthorhombic Phase ◽  
Boundary Structure ◽  
Crystallographic Axis ◽  
System A ◽  
High Resolution Structure ◽  
Electron Microscopes

The (110) twin structure of YBa2Cu3O7 superconductor oxide, which is formed to reduce the strain energy of the tetragonal to orthorhombic phase transformation by alternating the a-b crystallographic axis across the boundary, was extensively investigated. Up to now the structure of the twin boundary still remained unclear. In order to gain insight into the nature of the twin boundary in Y-Ba-Cu-O system, a study using electron diffraction techniques including optical and computed diffractograms, as well as high resolution structure imaging techniques with corresponding computer simulation and processing was initiated.Bulk samples of Y-Ba-Cu-O oxide were prepared as described elsewhere. TEM specimens were produced by crushing bulk samples into a fine powder, dispersing the powder in acetone, and suspending the fine particles on a holey carbon grid. The electron microscopy during this study was performed on both a JEOL 2000EX and 2000FX electron microscopes operated at 200 kV.

Speech Therapy Services in a Large School System: A Six-Year Overview

1976 ◽  
Vol 7 (4) ◽  
pp. 207-219 ◽  
Author(s):  
Constance P. DesRoches
Keyword(s):  
School System ◽  
Speech Therapy ◽  
Factors Affecting ◽  
Case Load ◽  
Number Of Children ◽  
School Population ◽  
System A ◽  
Therapy Services ◽  
And Shifts ◽  
Selection Factors

A statistical review provides analysis of four years of speech therapy services of a suburban school system which can be used for comparison with other school system programs. Included are data on the percentages of the school population enrolled in therapy, the categories of disabilities and the number of children in each category, the sex and grade-level distribution of those in therapy, and shifts in case-load selection. Factors affecting changes in case-load profiles are identified and discussed.

Sign in / Sign up

Export Citation Format

Share Document