The expressive power of 2-cnfs, conjunctive normal forms with two literals per clause, is shown to be severely limited compared to 3-cnfs.

There have been several conscious efforts made by different stakeholders in the area of nanoscience and nanotechnology to increase the awareness of social and ethical issues (SEI) among its practitioners. But so far, little has been done at the laboratory level to integrate a SEI component into the laboratory orientation schedule of practitioners. Since the laboratory serves as the locus of activities of the scientific community, it is important to introduce SEI there to stimulate thinking and discussion of SEI among (...) practitioners, which would eventually contribute toward the responsible development of this technology. In this article, through an example (at the Cornell NanoScale Science and Technology Facility (CNF), practitioners of which represent a section of the nano researchers’ community in the USA), it is shown how a SEI component can be incorporated into the laboratory orientation schedule of the practitioners from diverse disciplinary and institutional backgrounds. Results show that, at CNF, the practitioners enjoyed the discussion since most of them learned about SEI for the first time in their professional career. At the same time, some of them were also knowledgeable about SEI and contributed to the debates. Moreover, the SEI orientation had significant positive impact on the scientific community enabling them to self-reflect upon their own research and its implications for the wider society. This article also describes the efforts that were undertaken to disseminate this form of SEI orientation to other 13 USA universities within the National Nanotechnology Infrastructure Network (NNIN, one of the biggest networks funded from National Science Foundation for Nanotechnology research, of which CNF is a part). As a result of this effort, most of the NNIN sites have already started or were in the process of integrating a SEI component into their nanofabrication laboratories to make their users aware of SEI, ensuring eventual robust socio-technical integration in the NNIN laboratories. In the future, this form of SEI orientation can also be disseminated to other nanofabrication laboratories in the USA. (shrink)

We prove an exponential lower bound on the size of proofs in the proof system operating with ordered binary decision diagrams introduced by Atserias, Kolaitis and Vardi [2]. In fact, the lower bound applies to semantic derivations operating with sets defined by OBDDs. We do not assume any particular format of proofs or ordering of variables, the hard formulas are in CNF. We utilize (somewhat indirectly) feasible interpolation. We define a proof system combining resolution and the OBDD proof system.

We address in this paper the problem of counting the models of a propositional theory under incremental changes to its literals. Specifcally, we show that if a propositional theory Δ is in a special form that we call smooth, deterministic, decomposable negation normal form (sd-DNNF), then for any consistent set of literals S, we can simultaneously count (in time linear in the size of Δ) the models of Δ ∪ S and the models of every theory Δ ∪ T where (...) T results from adding, removing or flipping a literal in S. We present two results relating to the time and space complexity of compiling propositional theories into sd-DNNF. First, we show that if a conjunctive normal form (CNF) has a bounded treewidth, then it can be compiled into an sd-DNNF in time and space which are linear in its size. Second, we show that sd-DNNF is a strictly more space efficient representation than Free Binary Decision Diagrams (FBDDs). Finally, we discuss some applications of the counting results to truth maintenance systems, belief revision, and model-based diagnosis. (shrink)

How can we find any satisfying assignment for a Boolean formula that has many satisfying assignments? There exists an obvious randomized algorithm for solving this problem: one can just pick an assignment at random and check the truth value of the formula for this assignment, this is iterated until a satisfying assignment occurs. Does there exist a polynomial-time deterministic algorithm that solves the same problem? This paper presents such an algorithm and shows that its worst-case running time is linear when (...) input formulas are in k-CNF and a fraction of satisfying assignments is greater than a constant. This algorithm is almost the same as the algorithm proposed by Monien and Speckenmeyer in the early 1980s for less than 2n steps 3-SAT decision.Another result of this paper is that if a formula in k-CNF has many satisfying assignments, then there exists a short satisfying assignment, i.e. an assignment of truth values to a small number of variables. The proposed algorithm yields just such a short satisfying assignment. We also show that there exist formulas in general CNF having many satisfying assignments, that have no short satisfying assignments. (shrink)

Quasi-classical logic is a propositional logic for reasoning under inconsistency pointed out recently in the literature [3] [21]. Compared with several other paraconsistent logics, it has the nice feature that no special attention needs to be paid to a special form of premises. However, only few is known about its computational behaviour up to now. In this paper, we fill this gap by pointing out a linear time translation that maps every instance of the quasi-classical entailment problem for CNF formulas (...) into an instance of the classical entailment problem. This enables us to show that quasi-classical entailment for CNF formulas is “only” coNP -complete, take advantage of all existing automated reasoning techniques for classical entailment in order to improve quasi-classical inference from the practical side. Especially, tractable classes of formulas for quasi-classical entailment are pointed out. (shrink)

Few disputes in the annals of US environmentalism enjoy the pedigree of the conservation-preservation debate. Yet, although many scholars have written extensively on the meaning and history of conservation and preservation in American environmental thought and practice, the resonance of these concepts outside the academic literature has not been sufficiently examined. Given the significance of the ideals of conservation and preservation in the justification of environmental policy and management, however, we believe that a more detailed analysis of the real-world use (...) and understanding of these ideas is needed. In this paper, we describe the results of a qualitative, semantic study of the concepts of conservation and preservation undertaken in the context of the Chattahoochee National Forest (CNF), located in northern Georgia (USA). Thirty in-depth interviews were conducted with scientists and north Georgia residents either interested or involved in the future management of the forest. Respondents were asked to define conservation and preservation in their own words and to indicate which approach they felt was more appropriate for the management of the CNF. Qualitative content analysis was used to elicit a set of recurring themes for each foundational concept. Taken together, these themes help to flesh out the meaning of conservation and preservation for citizens and scientists today, and illustrate the evolving nature of two of the more significant and venerable ideas animating US environmental policy and management. (shrink)

The canonical pair of a proof system P is the pair of disjoint NP sets where one set is the set of all satisfiable CNF formulas and the other is the set of CNF formulas that have P-proofs bounded by some polynomial. We give a combinatorial characterization of the canonical pairs of depth d Frege systems. Our characterization is based on certain games, introduced in this article, that are parametrized by a number k, also called the depth. We show that (...) the canonical pair of a depth d Frege system is polynomially equivalent to the pair (Ad+2,Bd+2) where Ad+2 (respectively, Bd+1) are depth d+1 games in which Player I (Player II) has a positional winning strategy. Although this characterization is stated in terms of games, we will show that these combinatorial structures can be viewed as generalizations of monotone Boolean circuits. In particular, depth 1 games are essentially monotone Boolean circuits. Thus we get a generalization of the monotone feasible interpolation for Resolution, which is a property that enables one to reduce the task of proving lower bounds on the size of refutations to lower bounds on the size of monotone Boolean circuits. However, we do not have a method yet for proving lower bounds on the size of depth d games for d>1. (shrink)

We give a new characterization of the strict $$\forall {\Sigma^b_j}$$ sentences provable using $${\Sigma^b_k}$$ induction, for 1 ≤ j ≤ k. As a small application we show that, in a certain sense, Buss’s witnessing theorem for strict $${\Sigma^b_k}$$ formulas already holds over the relatively weak theory PV. We exhibit a combinatorial principle with the property that a lower bound for it in constant-depth Frege would imply that the narrow CNFs with short depth j Frege refutations form a strict hierarchy with (...) j, and hence that the relativized bounded arithmetic hierarchy can be separated by a family of $$\forall {\Sigma^b_1}$$ sentences. (shrink)

This paper presents a nonlinear trajectory controller with improved performances for a general model of the waverider based on feedback linearization theory and composite nonlinear feedback technique. First, a nonlinear controller is presented using the dynamic inversion and CNF technique for the MIMO Model, and the robust stability of the proposed controller is proved. Then, the nonlinear model is established on the basis of hypersonic aerodynamic principle, and the dynamic characteristics are analyzed accordingly, and the periodic trajectory is designed and (...) optimized in combination with a fuel optimization problem. Furthermore, the nonlinear controller is applied to the trajectory tracking of the waverider model, and the general design steps are provided the flight controller using this nonlinear control method. Finally, an illustrative example is given to verify the effectiveness of the nonlinear controller of the waverider, and the flight performances are improved accordingly, including system stability, robustness, and tracking ability. (shrink)

Resolution and cut-free LK are the most popular propositional systems used for logical automated reasoning. The question whether or not resolution and cut-free LK have the same efficiency on the system of CNF formulas has been asked and studied since 1960 425–467). It was shown in Cook and Reckhow, J. Symbolic Logic 44 36–50 that tree resolution has super-polynomial speed-up over cut-free LK. Naturally, the current issue is whether or not resolution and cut-free LK expressed as directed acyclic graphs have (...) the same efficiency. In this paper, we introduce a new algorithm to eliminate atomic cuts and show that cut-free LK polynomially simulates resolution when the input formula is expressed as a k-CNF formula. As a corollary, we show that regular resolution does not polynomially simulate cut-free LK . We also show that cut-free LK polynomially simulates regular resolution. (shrink)

(although the FOF, unlike the CNF, is still a theorem). The correct version of Problem 62 is (following the format of (Pelletier, 1986)): Natural FOF Negated Conclusion CNF (Ax)r(Pet~(Px m Pf(x))) m Pf(f(x))] Pet Px+ P f(f(x)) + -Pa..

In 2004 Atserias, Kolaitis, and Vardi proposed $\text {OBDD}$ -based propositional proof systems that prove unsatisfiability of a CNF formula by deduction of an identically false $\text {OBDD}$ from $\text {OBDD}$ s representing clauses of the initial formula. All $\text {OBDD}$ s in such proofs have the same order of variables. We initiate the study of $\text {OBDD}$ based proof systems that additionally contain a rule that allows changing the order in $\text {OBDD}$ s. At first we consider a proof (...) system $\text {OBDD}$ that uses the conjunction rule and the rule that allows changing the order. We exponentially separate this proof system from $\text {OBDD}$ proof system that uses only the conjunction rule. We prove exponential lower bounds on the size of $\text {OBDD}$ refutations of Tseitin formulas and the pigeonhole principle. The first lower bound was previously unknown even for $\text {OBDD}$ proofs and the second one extends the result of Tveretina et al. from $\text {OBDD}$ to $\text {OBDD}$.In 2001 Aguirre and Vardi proposed an approach to the propositional satisfiability problem based on $\text {OBDD}$ s and symbolic quantifier elimination $ algorithms). We augment these algorithms with the operation of reordering of variables and call the new scheme $\text {OBDD}$ algorithms. We notice that there exists an $\text {OBDD}$ algorithm that solves satisfiable and unsatisfiable Tseitin formulas in polynomial time, but we show that there are formulas representing systems of linear equations over $\mathbb {F}_2$ that are hard for $\text {OBDD}$ algorithms. Our hard instances are satisfiable formulas representing systems of linear equations over $\mathbb {F}_2$ that correspond to checksum matrices of error correcting codes. (shrink)

Atserias, Galesi, and Pudlák have shown that the monotone sequent calculus MLK quasipolynomially simulates proofs of monotone sequents in the full sequent calculus LK . We generalize the simulation to the fragment MCLK of LK which can prove arbitrary sequents, but restricts cut-formulas to be monotone. We also show that MLK as a refutation system for CNFs quasipolynomially simulates LK.

This book constitutes the refereed proceedings of the 12th International Conference on Theory and Applications of Satisfiability Testing, SAT 2009, held in Swansea, UK, in June/July 2009. The 34 revised full papers presented together with 11 revised short papers and 2 invited talks were carefully selected from 86 submissions. The papers are organized in topical sections on applications of SAT, complexity theory, structures for SAT, resolution and SAT, translations to CNF, techniques for conflict-driven SAT Solvers, solving SAT by local search, (...) hybrid SAT solvers, automatic adaption of SAT solvers, stochastic approaches to SAT solving, QBFs and their representations, optimization algorithms, distributed and parallel solving. (shrink)