Search

In this paper, we discuss the copy complexity of Horn formulas with respect to unit resolution. A Horn formula is a boolean formula in conjunctive normal form (CNF) with at most one positive literal per clause. Horn formulas find applications in a number of domains, such as program verification (abstract interpretation) and logic programming (answer set programming). Quantified Horn clauses are used extensively in temporal verification of universal properties. Resolution is one of the oldest proof systems (refutation systems) for the boolean satisfiability problem (SAT), when the input is presented in conjunctive normal form (CNF). It is both sound and complete, although inefficient, when compared to other stronger proof systems for boolean formulas. Despite its inefficiency, the simple nature of resolution makes it an integral part of several theorem provers. Unit resolution is a restricted form of resolution in which each resolution step needs to use a clause with only one literal (unit literal clause). While not complete for general CNF formulas, unit resolution is complete for Horn formulas. Read-once resolution is a form of resolution in which each clause (input or derived) may be used in at most one resolution step. As with unit resolution, read-once resolution is incomplete in general and complete for Horn clauses. This paper focuses on a combination of unit resolution and read-once resolution called unit read-once resolution. Unit read-once resolution is incomplete for Horn clauses. In this paper, we study the copy complexity problem in Horn formulas with respect to unit read-once resolution. Briefly, the copy complexity of a formula with respect to unit read-once resolution, is the smallest number k, such that replicating each clause k times guarantees the existence of a unit read-once resolution refutation (UROR). This paper focuses on two problems related to the copy complexity of Horn formulas with respect to unit read-once resolution. We first relate the copy complexity of Horn formulas with respect to unit read-once resolution to the copy complexity of the corresponding Horn constraint system with respect to the addition rule. We also examine a form of copy complexity in which we permit replication of derived clauses, in addition to the input clauses. Finally, we provide a polynomial time algorithm for the problem of checking if a 2-CNF formula has a UROR.

Propositional logic, with the aid of SAT solvers, has become capable of solving a range of important and complicated problems. Expanding this range, to contain additional varieties of problems, is subject to the complexity resulting from encoding counting constraints in conjunctive normal form (CNF). Due to the limitation of the expressive power of propositional logic, generally, such an encoding increases the numbers of variables and clauses excessively. This work eliminates the indicated drawback by interpolating constraint symbols and the set of natural numbers $${\mathbb {N}}$$ into the alphabet of propositional logic and adjusting the underlying language accordingly. In the extended logic counting constraints are naturally formulated, while many important aspects, such as Boolean nature and the soundness and completeness theorems, are kept preserved.

In this paper we discuss conversion methods from the conjunctive normal form (CNF) to the algebraic normal form (ANF) of a Boolean function. Whereas the reverse conversion has been studied before, the CNF to ANF conversion has been achieved predominantly via a standard method which tends to produce many polynomials of high degree. Based on a block-building mechanism, we design a new blockwise algorithm for the CNF to ANF conversion which is geared towards producing fewer and lower degree polynomials. In particular, we look for as many linear polynomials as possible in the converted system and check that our algorithm finds them. As an application, we suggest a new algebraic extension of the resolution calculus which is tailored to the output of the standard CNF to ANF conversion algorithm. Experiments show that the ANF produced by our algorithm outperforms the standard conversion in “real life” examples originating from cryptographic attacks, and that our algebraic resolution algorithm solves some SAT instances which are notoriously hard for SAT solvers.

In this paper, we analyze Boolean formulas in conjunctive normal form (CNF) from the perspective of read-once resolution (ROR) refutation schemes. A read-once (resolution) refutation is one in which each clause is used at most once. Derived clauses can be used as many times as they are deduced. However, clauses in the original formula can only be used as part of one derivation. It is well known that ROR is not complete; that is, there exist unsatisfiable formulas for which no ROR exists. Likewise, the problem of checking if a 3CNF formula has a read-once refutation is NP-complete. This paper is concerned with a variant of satisfiability called not-all-equal satisfiability (NAE-satisfiability). A CNF formula is NAE-satisfiable if it has a satisfying assignment in which at least one literal in each clause is set to false. It is well known that the problem of checking NAE-satisfiability is NP-complete. Clearly, the class of CNF formulas which are NAE-satisfiable is a proper subset of satisfiable CNF formulas. It follows that traditional resolution cannot always find a proof of NAE-unsatisfiability. Thus, traditional resolution is not a sound procedure for checking NAE-satisfiability. In this paper, we introduce a variant of resolution called NAE-resolution which is a sound and complete procedure for checking NAE-satisfiability in CNF formulas. The focus of this paper is on a variant of NAE-resolution called read-once NAE-resolution in which each clause (input or derived) can be part of at most one NAE-resolution step. Our principal result is that read-once NAE-resolution is a sound and complete procedure for 2CNF formulas. Furthermore, we provide an algorithm to determine the smallest such NAE-resolution in polynomial time. This is in stark contrast to the corresponding problem concerning 2CNF formulas and ROR refutations. We also show that the problem of checking whether a 3CNF formula has a read-once NAE-resolution is NP-complete.

A major problem in computational learning theory is whether the class of formulas in conjunctive normal form (CNF) is efficiently learnable. Although it is known that this class cannot be polynomially learned using either membership or equivalence queries alone, it is open whether the CNF class can be polynomially learned using both types of queries. One of the most important results concerning a restriction of the CNF class is that propositional Horn formulas are polynomial time learnable in Angluin’s exact learning model with membership and equivalence queries. In this work, we push this boundary and show that the class of multivalued dependency formulas (MVDF), which non-trivially extends propositional Horn, is polynomially learnable from interpretations. We then provide a notion of reduction between learning problems in Angluin’s model, showing that a transformation of the algorithm suffices to efficiently learn multivalued database dependencies from data relations. We also show via reductions that our main result extends well known previous results and allows us to find alternative solutions for them.

We consider the satisfiability problem (SAT) for Boolean formulas given in conjunctive normal form with the restriction that each clause contains three literals (3-CNF). Generation of random formulas with a fixed clause length is widely used in empirical studies. An interesting phenomenon of this method is the repeatedly confirmed linear dependence of the number of clauses in the formula on the number of Boolean variables at the point of the “phase transition” from satisfiable to unsatisfiable formulas (when the fraction of unsatisfiable formulas becomes prevailing). We propose and study a method for generating random formulas that has a smaller coefficient (3.49) of proportionality between the number of clauses and the number of variables at the point of the “phase transition” (for the previously known generation method this coefficient is 4.23).

Many combinatorial problems in various fields can be translated to Maximum Satisfiability (MaxSAT) problems. Although the general problem is $\mathcal {N}\mathcal {P}$ -hard, more and more practical problems may be solved due to the significant effort which has been devoted to the development of efficient solvers. The art of constraints encoding is as important as the art of devising algorithms for MaxSAT. In this paper, we present several encoding methods of pseudo-Boolean constraints into Boolean satisfiability problems in Conjunctive Normal Form (CNF) formula, which are based on the idea of modular arithmetic and only generate auxiliary variables for each unique combination of weights. These techniques are efficient in encoding and solving MaxSAT problems. In particular, our solvers won the partial MaxSAT industrial category from 2010 through 2012 and ranked second in the 2017 main weighted track of the MaxSAT evaluation. We prove the correctness and the pseudo-polynomial space complexity of our encodings and also give a heuristics of the base selection for modular arithmetic. Our experimental results show that our encoding compactly encodes the constraints, and the obtained clauses are efficiently handled by a state-of-the-art SAT solver.

Issues related to the construction of efficient algorithms for intractable discrete problems are studied. Enumeration problems are considered. Their intractability has two aspects—exponential growth of the number of their solutions with increasing problem size and the complexity of finding (enumerating) these solutions. The basic enumeration problem is the dualization of a monotone conjunctive normal form or the equivalent problem of finding irreducible coverings of Boolean matrices. For the latter problem and its generalization for the case of integer matrices, asymptotics for the typical number of solutions are obtained. These estimates are required, in particular, to prove the existence of asymptotically optimal algorithms for monotone dualization and its generalizations.

Recent work in weighted model counting proposed a unifying framework for dynamic-programming algorithms. The core of this framework is a project-join tree: an execution plan that specifies how Boolean variables are eliminated. We adapt this framework to compute exact literal-weighted projected model counts of propositional formulas in conjunctive normal form. Our key conceptual contribution is to define gradedness on project-join trees, a novel condition requiring irrelevant variables to be eliminated before relevant variables. We prove that building graded project-join trees can be reduced to building standard project-join trees and that graded project-join trees can be used to compute projected model counts. The resulting tool ProCount is competitive with the state-of-the-art tools \(\texttt {D4}_{\texttt {P}}\), projMC, and reSSAT, achieving the shortest solving time on 131 benchmarks of 390 benchmarks solved by at least one tool, from 849 benchmarks in total.

The article explores the satisfiability of conjunctive normal forms used in modeling systems.The problems of CNF preprocessing are considered.The analysis of particular methods for reducing this formulas, which have polynomial input complexity is given.

In this paper, we discuss the copy complexity of unit resolution with respect to Horn formulas. A Horn formula is a boolean formula in conjunctive normal form (CNF) with at most one positive literal per clause. Horn formulas find applications in a number of domains such as program verification and logic programming. Resolution as a proof system for boolean formulas is both sound and complete. However, resolution is considered an inefficient proof system when compared to other stronger proof systems for boolean formulas. Despite this inefficiency, the simple nature of resolution makes it an integral part of several theorem provers. Unit resolution is a restricted form of resolution in which each resolution step needs to use a clause with only one literal (unit literal clause). While not complete for general CNF formulas, unit resolution is complete for Horn formulas. A read-once resolution (ROR) refutation is a refutation in which each clause (input or derived) may be used at most once in the derivation of a refutation. As with unit resolution, ROR refutation is incomplete in general and complete for Horn clauses. This paper focuses on a combination of unit resolution and read-once resolution called Unit read-once resolution (UROR). UROR is incomplete for Horn clauses. In this paper, we study the copy complexity problem in Horn formulas under UROR. Briefly, the copy complexity of a formula under UROR is the smallest number k such that replicating each clause k times guarantees the existence of a UROR refutation. This paper focuses on two problems related to the copy complexity of unit resolution. We first relate the copy complexity of unit resolution for Horn formulas to the copy complexity of the addition rule in the corresponding Horn constraint system. We also examine a form of copy complexity where we permit replication of derived clauses, in addition to the input clauses. Finally, we provide a polynomial time algorithm for the problem of checking if a 2-CNF formula has a UROR refutation.

A Boolean function given in a conjunctive normal form is Horn if every clause contains at most one positive literal, and it is pure Horn if every clause contains exactly one positive literal. Due to their computational tractability, Horn functions are studied extensively in many areas of computer science and mathematics such as combinatorics, artificial intelligence, database theory, algebra and logic. The present paper considers the problem of finding minimal representations of pure Horn functions. We give a new proof for a recent min–max result of Boros et al. regarding body-minimal representations. The proof is algorithmic and finds the so called Guigues–Duquenne basis. We also describe a new construction that combines two existing representations into a third one.

This paper provides new results on the application of semidefinite optimization to satisfiability by studying the connection between semidefinite optimization and minimal unsatisfiability. We use a semidefinite least squares problem to assign weights to the clauses of a propositional formula in conjunctive normal form. We then show that these weights are a measure of the necessity of each clause in rendering the formula unsatisfiable, the weight of a necessary clause is strictly greater than the weight of any unnecessary clause. In particular, we show the following results: first, if a formula is minimal unsatisfiable, then all of its clauses have the same weight; second, if a clause does not belong to any minimal unsatisfiable subformula, then its weight is zero. An additional contribution of this paper is a demonstration of how the infeasibility of a semidefinite optimization problem can be tested using a semidefinite least squares problem by extending an earlier result for linear optimization. The connection between the semidefinite least squares problem and Farkas’ Lemma for semidefinite optimization is also discussed.

Given a Boolean formula ϕ(x) in conjunctive normal form (CNF), the density of states counts the number of variable assignments that violate exactly e clauses, for all values of e. Thus, the density of states is a histogram of the number of unsatisfied clauses over all possible assignments. This computation generalizes both maximum-satisfiability (MAX-SAT) and model counting problems and not only provides insight into the entire solution space, but also yields a measure for the hardness of the problem instance. Consequently, in real-world scenarios, this problem is typically infeasible even when using state-of-the-art algorithms. While finding an exact answer to this problem is a computationally intensive task, we propose a novel approach for estimating density of states based on the concentration of measure inequalities. The methodology results in a quadratic unconstrained binary optimization (QUBO), which is particularly amenable to quantum annealing-based solutions. We present the overall approach and compare results from the D-Wave quantum annealer against the best-known classical algorithms such as the Hamze-de Freitas-Selby (HFS) algorithm and satisfiability modulo theory (SMT) solvers.

Satisfying spin-assignments of triangulations of a surface are states of minimum energy of the antiferromagnetic Ising model on triangulations which correspond (via geometric duality) to perfect matchings in cubic bridgeless graphs. In this work we show that it is NP -complete to decide whether or not a triangulation of a surface admits a satisfying spin-assignment, and that it is # P -complete to determine the number of such assignments. Our results imply that the determination of even the entropy of the Ising model on triangulations at the thermodynamical limit is already # P -hard.The aforementioned claims are derived via elaborate (and atypical) reductions that map a Boolean formula in conjunctive normal form into triangulations of orientable closed surfaces. Moreover, the novel reduction technique enables us to prove that even very constrained versions of # MaxCut are already # P -hard.

Many NP-hard problems are commonly expressed with pseudo-Boolean (PB) constraints, which is a linear arithmetic constraint over Boolean variables. Conjunctive Normal Form (CNF) encoding always plays an important role in solving these constraints. In this paper, we propose Weighted Modulo Totalizer (WMTO) which is a hybrid CNF encoding of PB constraints between Modulo Totalizer (MTO) and Weighted Totalizer (WTO). WMTO uses less clauses and auxiliary variables than each of them. Our experimental results show that WMTO encodes the constraints compactly and the obtained clauses are efficiently handled by a state-of-the-art SAT solver

State-of-the-art procedures for evaluating quantified Boolean formulas often expect input formulas in prenex conjunctive normal form (PCNF). We study dependency schemes as a means of reordering the quantifier prefix of a PCNF formula while preserving its truth value. Dependency schemes associate each formula with a binary relation on its variables (the dependency relation) that imposes constraints on certain operations manipulating the formula's quantifier prefix. We prove that known dependency schemes support a stronger reordering operation than was previously known. We present an algorithm that, given a formula and its dependency relation, computes a compatible reordering with a minimum number of quantifier alternations. In combination with a dependency scheme that can be computed in polynomial time, this yields a polynomial time heuristic for reducing the number of quantifier alternations of an input formula. The resolution-path dependency scheme is the most general dependency scheme introduced so far. Using an interpretation of resolution paths as directed paths in a formula's implication graph, we prove that the resolution-path dependency relation can be computed in polynomial time.

It was previously established that almost every Boolean function of n variables with k zeros, where k is at most log2n–log2log2n + 1, can be associated with a Boolean function of 2k–1–1 variables with k zeros (complete function) such that the complexity of implementing the original function in the class of disjunctive normal forms is determined only by the complexity of implementing the complete function. An asymptotically tight bound is obtained for the minimum possible number of literals contained in the disjunctive normal forms of the complete function.

Model counting is the #P problem of counting the number of satisfying solutions of a given propositional formula. Here we focus on a restricted variant of this problem, where the input formula is monotone (i.e., there are no negations). A monotone conjunctive normal form (CNF) formula is sufficient for modeling various graph problems, e.g., the vertex covers of a graph. Even for this restricted case, there is no known efficient approximation scheme. We show that the classical Spectra technique that is widely used in network reliability can be adapted for counting monotone CNF formulas. We prove that the proposed algorithm is logarithmically efficient for random monotone 2-CNF instances. Although we do not prove the efficiency of Spectra for k-CNF where k > 2, our experiments show that it is effective in practice for such formulas.

A NP hard problem CNF to DNF conversion is a vast area of research for AI, circuit design, FPGA’s (Miltersen et al. in On converting CNF To DNF, 2003), PLA’s, etc. (Beame in A switching lemma primer, 1994; Kottler and Kaufmann in SArTagnan—a parallel portfolio SAT solver with lockless physical clause sharing, 2011). Optimization and its statistics has become a potential requirement for analysis and behavior of normal form conversion. Various applications are in its requirement like gnome analysis, grid computing, bioinformatics, imaging systems, rough sets require higher variable processing algorithm. Problem statement is—design and implementation of optimal conjunctive normal form to optimal (prime implicants) disjunctive normal form conversion which is an “NP hard problem conversion to an NP complete”. Thus CNF to DNF can only be considered to evaluate best performance for higher variable processing on high end systems. The best-known representations of Boolean functions f are those as disjunctions of terms (DNFs) and as conjunctions of clauses (CNFs) (Beame 1994; Kottler and Kaufmann 2011) (Wegener in The complexity of boolean functions, 1987). It is convenient to define the DNF size of f as the minimal number of terms in a DNF representing f and the CNF size as the minimal number of clauses in a CNF representing f (Kottler and Kaufmann 2011).

The Maximum Satisfiability (MaxSAT) is the problem of determining the maximum number of clauses of a given Boolean formula in Conjunctive Normal Form (CNF) that can be satisfied by an assignment of truth values to the variables of the formula. Many exact solvers for MaxSAT have been developed during recent years, and many of them were presented in the well-known SAT Conference. Algorithms for MaxSAT generally fall into two categories: (1) branch and bound algorithms and (2) algorithms that use successive calls to a SAT solver (SAT-based), which this paper in on. In practical problems, SAT-based algorithms have been shown to be more efficient. This paper provides an experimental investigation to compare the performance of recent SAT-based and branch and bound algorithms on benchmarks of the MaxSAT Evaluations.

In many practical settings it is useful to find a small unsatisfiable subset of a given unsatisfiable set of constraints. We study this problem from a parameterized complexity perspective, taking the size of the unsatisfiable subset as the natural parameter where the set of constraints is either (i) given a set of clauses, i.e., a formula in conjunctive normal Form (CNF), or (ii) as an instance of the Constraint Satisfaction Problem (CSP). In general, the problem is fixed-parameter in tractable. For an instance of the propositional satisfiability problem (SAT), it was known to be W[1]-complete. We establish A[2]-completeness for CSP instances, where A[2]-hardness prevails already for the Boolean case. With these fixed-parameter intractability results for the general case in mind, we consider various restricted classes of inputs and draw a detailed complexity landscape. It turns out that often Boolean CSP and CNF formulas behave similarly, but we also identify notable exceptions to this rule. The main part of this article is dedicated to classes of inputs that are induced by Boolean constraint languages that Schaefer [1978] identified as the maximal constraint languages with a tractable satisfiability problem. We show that for the CSP setting, the problem of finding small unsatisfiable subsets remains fixed-parameter intractable for all Schaefer languages for which the problem is non-trivial. We show that this is also the case for CNF formulas with the exception of the class of bijunctive (Krom) formulas, which allows for an identification of a small unsatisfiable subset in polynomial time. In addition, we consider various restricted classes of inputs with bounds on the maximum number of times that a variable occurs (the degree), bounds on the arity of constraints, and bounds on the domain size. For the case of CNF formulas, we show that restricting the degree is enough to obtain fixed-parameter tractability, whereas for the case of CSP instances, one needs to restrict the degree, the arity, and the domain size simultaneously to establish fixed-parameter tractability. Finally, we relate the problem of finding small unsatisfiable subsets of a set of constraints to the problem of identifying whether a given variable-value assignment is entailed or forbidden already by a small subset of constraints. Moreover, we use the connection between the two problems to establish similar parameterized complexity results also for the latter problem.

Constraint "at most one" is a basic cardinality constraint which requires that at most one of its $n$ boolean inputs is set to $1$. This constraint is widely used when translating a problem into a conjunctive normal form (CNF) and we investigate its CNF encodings suitable for this purpose. An encoding differs from a CNF representation of a function in that it can use auxiliary variables. We are especially interested in propagation complete encodings which have the property that unit propagation is strong enough to enforce consistency on input variables. We show a lower bound on the number of clauses in any propagation complete encoding of the "at most one" constraint. The lower bound almost matches the size of the best known encodings. We also study an important case of 2-CNF encodings where we show a slightly better lower bound. The lower bound holds also for a related "exactly one" constraint., 38 pages, version 3 is significantly reorganized in order to improve readability

The practical success of Boolean Satisfiability (SAT) solvers stems from the CDCL (Conflict-Driven Clause Learning) approach to SAT solving. However, from a propositional proof complexity perspective, CDCL is no more powerful than the resolution proof system, for which many hard examples exist. This paper proposes a new problem transformation, which enables reducing the decision problem for formulas in conjunctive normal form (CNF) to the problem of solving maximum satisfiability over Horn formulas. Given the new transformation, the paper proves a polynomial bound on the number of MaxSAT resolution steps for pigeonhole formulas. This result is in clear contrast with earlier results on the length of proofs of MaxSAT resolution for pigeonhole formulas. The paper also establishes the same polynomial bound in the case of modern core-guided MaxSAT solvers. Experimental results, obtained on CNF formulas known to be hard for CDCL SAT solvers, show that these can be efficiently solved with modern MaxSAT solvers.

Modern solvers for quantified Boolean formulas (QBF) not only decide the satisfiability of a formula, but also return a set of Skolem functions representing a model for a true QBF. Unfortunately, in combination with a preprocessor this ability is lost for many preprocessing techniques. A preprocessor rewrites the input formula to an equi-satisfiable formula which is often easier to solve than the original formula. Then the Skolem functions returned by the solver represent a solution for the preprocessed formula, but not necessarily for the original encoding.

We consider logic-based argumentation in which an argument is a pair (Φ, α), where the support Φ is a minimal consistent set of formulae taken from a given knowledge base (usually denoted by Δ) that entails the claim α (a formula). We study the complexity of three central problems in argumentation: the existence of a support Φ⊆Δ, the verification of a support, and the relevance problem (given ψ, is there a support Φ such that ψ ∈ Φ?). When arguments are given in the full language of propositional logic, these problems are computationally costly tasks: the verification problem is DP-complete; the others are Σ p 2 -complete. We study these problems in Schaefer's famous framework where the considered propositional formulae are in generalized conjunctive normal form. This means that formulae are conjunctions of constraints built upon a fixed finite set of Boolean relations Γ (the constraint language). We show that according to the properties of this language Γ, deciding whether there exists a support for a claim in a given knowledge base is either polynomial, NP-complete, coNP-complete, or Σ p 2 -complete. We present a dichotomous classification, P or DP-complete, for the verification problem and a trichotomous classification for the relevance problem into either polynomial, NP-complete, or Σ p 2 -complete. These last two classifications are obtained by means of algebraic tools.

Designing algorithms capable of efficiently constructing minimal models of Conjunctive Normal Form theories (CNFs) is an important task in AI. This paper provides new results along this research line and presents new algorithms for performing minimal model finding and checking over positive propositional CNFs and model minimization over propositional CNFs. A CNF is positive if each of its clauses has at least a positive literal. An algorithmic schema, called the Generalized Elimination Algorithm (GEA) is presented, that computes a minimal model of any positive CNF. The schema generalizes the Elimination Algorithm (EA) [5], which computes a minimal model of positive head-cycle-free (HCF) CNF theories. While the EA always runs in polynomial time in the size of the input HCF CNF, the complexity of the GEA depends on the complexity of the specific eliminating operator invoked therein, which may in general turn out to be exponential. Therefore, a specific eliminating operator is defined by which the GEA computes, in polynomial time, a minimal model for a class of CNF that strictly includes head-elementary-set-free (HEF) CNF theories [14], which form, in their turn, a strict superset of HCF theories. Furthermore, in order to deal with the high complexity associated with recognizing HEF theories, an ''incomplete'' variant of the GEA (called IGEA) is proposed: the resulting schema, once instantiated with an appropriate elimination operator, always constructs a model of the input CNF, which is guaranteed to be minimal if the input theory is HEF. In the light of the above results, the main contribution of this work is the enlargement of the tractability frontier for the minimal model finding and checking and the model minimization problems.

In this paper we define disjunctive and conjunctive normal forms of De Morgan functions and prove a functional completeness theorem for these functions.

The PPSZ algorithm by Paturi, Pudlak, Saks, and Zane [J. ACM, 52 (2005), pp. 337--364] is the fastest known algorithm for Unique $k$-SAT, where the input formula does not have more than one satisfying assignment. For $k\geq 5$ the same bounds hold for general $k$-SAT. We show that this is also the case for k=3,4, using a slightly modified PPSZ algorithm. We do the analysis by defining a cost for satisfiable conjunctive normal form formulas, which we prove to decrease in each PPSZ step by a certain amount. This improves our previous best bounds with Moser and Scheder [Proceedings of STACS, 2011, pp. 237--248] for 3-SAT to $O(1.308^n)$ and for 4-SAT to $O(1.469^n)$. Furthermore, our analysis is much simpler than the existing analysis of PPSZ for general $k$-SAT.

In this paper, we analyze boolean formulas in conjunctive normal form CNF from the perspective of read-once resolution ROR refutation. A read-once resolution refutation is one in which each input clause is used at most once. It is well-known that read-once resolution is not complete, i.e., there exist unsatisfiable formulas for which no read-once resolution exists. Likewise, the problem of checking if a 3CNF formula has a read-once refutation is NP-complete. This paper is concerned with a variant of satisfiability called Not-All-Equal Satisfiability NAE-Satisfiability. NAE-Satisfiability is the problem of checking whether an arbitrary CNF formula has a satisfying assignment in which at least one literal in each clause is set to false. It is well-known that NAE-satisfiability is NP-complete. Clearly, the class of CNF formulas which are NAE-satisfiable is a proper subset of the class of satisfiable CNF formulas. It follows that traditional resolution cannot always find a proof of NAE-unsatisfiability. Thus, traditional resolution is not a sound procedure for checking NAE-satisfiability. In this paper, we introduce a variant of resolution called NAE-resolution, which is a sound and complete procedure for checking NAE-satisfiability in CNF formulas. We focus on a variant of NAE-resolution called read-once NAE-resolution, in which each input clause can be part of at most one NAE-resolution step. Our principal result is that read-once NAE-resolution is a sound and complete procedure for checking the NAE-satisfiability of 2CNF formulas; we also provide a polynomial time algorithm to determine the shortest read-once NAE-resolution of a 2CNF formula. Finally, we establish that the problem of checking whether a 3CNF formula has a read-once NAE-resolution is NP-complete.

Knowledge compilation is a process of adding more information to a knowledge base in order to make it easier to deduce facts from the compiled base than from the original one. One type of knowledge compilation occurs when the knowledge in question is represented by a Boolean formula in conjunctive normal form (CNF). The goal of knowledge compilation in this case is to add clauses to the input CNF until a logically equivalent propagation complete CNF is obtained. A CNF is called propagation complete if after any partial substitution of truth values all logically entailed literals can be inferred from the resulting CNF formula by unit propagation. The key to this type of knowledge compilation is the ability to generate so-called empowering clauses. A clause is empowering for a CNF if it is an implicate and for some partial substitution of truth values it enlarges the set of entailed literals inferable by unit propagation. In this paper we study several complexity issues related to empowering implicates, propagation completeness, and its relation to resolution proofs. We show several results: (a) given a CNF and a clause it is co-NP complete to decide whether the clause is an empowering implicate of the CNF, (b) given a CNF it is NP-complete to decide whether there exists an empowering implicate for it and thus it is co-NP complete to decide whether a CNF is propagation complete, and (c) there exist CNFs to which an exponential number of clauses must be added to make them propagation complete.

International audience; We propose a “formula slicing” method for finding inductive invariants. It is based on the observation that many loops in the program affect only a small part of the memory, and many invariants which were valid before a loop are still valid after.Given a precondition of the loop, obtained from the preceding program fragment, we weaken it until it becomes inductive. The weakening procedure is guided by counterexamples-to-induction given by an SMT solver. Our algorithm applies to programs with arbitrary loop structure, and it computes the strongest invariant in an abstract domain of weakenings of preconditions. We call this algorithm “formula slicing”, as it effectively performs “slicing” on formulas derived from symbolic execution.We evaluate our algorithm on the device driver benchmarks from the International Competition on Software Verification (SV-COMP), and we show that it is competitive with the state-of-the-art verification techniques.

In this chapter, we focus on a novel two-level logic representation. We define Majority Normal Form (MNF), as an alternative to the traditional Disjunctive Normal Form (DNF) and the Conjunctive Normal Form (CNF). After a brief investigation on the MNF expressive power, we study the problem of MNF-SATisfiability (MNF-SAT). We prove that MNF-SAT is NP-complete, as its CNF-SAT counterpart. However, we show practical restrictions on MNF formula whose satisfiability can be decided in polynomial time. We finally propose a simple algorithm to solve MNF-SAT, based on the intrinsic functionality of two-level majority logic. Although an automated MNF-SAT solver is still under construction, manual examples already demonstrate promising opportunities.

It follows from known results in the literature that least and greatest fixed-points of monotone polynomials on Heyting algebras—that is, the algebraic models of the Intuitionistic Propositional Calculus—always exist, even when these algebras are not complete as lattices. The reason is that these extremal fixed-points are definable by formulas of the IPC . Consequently, the μ-calculus based on intuitionistic logic is trivial, every μ-formula being equivalent to a fixed-point free formula. In the first part of this article, we give an axiomatization of least and greatest fixed-points of formulas, and an algorithm to compute a fixed-point free formula equivalent to a given μ-formula. The axiomatization of the greatest fixed-point is simple. The axiomatization of the least fixed-point is more complex, in particular every monotone formula converges to its least fixed-point by Kleene’s iteration in a finite number of steps, but there is no uniform upper bound on the number of iterations. The axiomatization yields a decision procedure for the μ-calculus based on propositional intuitionistic logic. The second part of the article deals with closure ordinals of monotone polynomials on Heyting algebras and of intuitionistic monotone formulas; these are the least numbers of iterations needed for a polynomial/formula to converge to its least fixed-point. Mirroring the elimination procedure, we show how to compute upper bounds for closure ordinals of arbitrary intuitionistic formulas. For some classes of formulas, we provide tighter upper bounds that, in some cases, we prove exact.

Most of the popular efficient proof search calculi work on formulae that are in clausal form, i.e. in disjunctive or conjunctive normal form. Hence, most state-of-the-art fully automated theorem provers require a translation of the input formula into clausal form in a preprocessing step. Translating a proof in clausal form back into a more readable non-clausal proof of the original formula is not straightforward. This paper presents a non-clausal theorem prover for classical first-order logic. It is based on a non-clausal connection calculus and implemented with a few lines of Prolog code. By working entirely on the original structure of the input formula, the resulting non-clausal proofs are not only shorter, but can also be more easily translated into, e.g., sequent proofs. Furthermore, a non-clausal proof search is more suitable for some non-classical logics.

International audience; We determine the complexity of an optimization problem related to information theory. Taking a conjunctive propositional formula over some finite set of Boolean relations as input, we seek a satisfying assignment of the formula having minimal Hamming distance to a given assignment that is not required to be a model (NearestSolution, NSol). We obtain a complete classification with respect to the relations admitted in the formula. For two classes of constraint languages we present polynomial time algorithms; otherwise, we prove hardness or completeness concerning the classes APX, poly-APX, NPO, or equivalence to well-known hard optimization problems.

Satisfiability modulo theory (SMT) consists in testing the satisfiability of first-order formulas over linear integer or real arithmetic, or other theories. In this survey, we explain the combination of propositional satisfiability and decision procedures for conjunctions known as DPLL(T), and the alternative “natural domain” approaches. We also cover quantifiers, Craig interpolants, polynomial arithmetic, and how SMT solvers are used in automated software analysis.

Transforming a planning instance into a propositional formula \(\phi \) to be solved by a SAT solver is a common approach in AI planning. In the context of multiagent planning, this approach causes the distributed SAT problem: given \(\phi \) distributed among agents –each agent knows a part of \(\phi \) but no agent knows the whole \(\phi \)–, check if \(\phi \) is SAT or UNSAT by message passing. On the other hand, Asynchronous Backtracking (ABT) is a complete distributed constraint satisfaction algorithm, so it can be directly used to solve distributed SAT. Clause learning is a technique, commonly used in centralized SAT solvers, that can be applied to enhance ABT efficiency when used for distributed SAT. We prove that ABT with clause learning remains correct and complete. Experiments on several planning benchmarks show very substantial benefits for ABT with clause learning.

2QBF is a special form \(\forall \varvec{x} \exists \varvec{y}.\phi \) of the quantified Boolean formula (QBF) restricted to only two quantification layers, where \(\phi \) is a quantifier-free formula. Despite its restricted form, it provides a framework for a wide range of applications, such as artificial intelligence, graph theory, synthesis, etc. In this work, we overview two main 2QBF challenges in terms of solving and certification. We contribute several improvements to existing solving approaches and study how the corresponding approaches affect certification. We further conduct an extensive experimental comparison on both competition and application benchmarks to demonstrate strengths of the proposed methodology.

The partial string avoidability problem is stated as follows: given a finite set of strings with possible “holes” (wildcard symbols), determine whether there exists a two-sided infinite string containing no substrings from this set, assuming that a hole matches every symbol. The problem is known to be NP-hard and in PSPACE, and this article establishes its PSPACE-completeness. Next, string avoidability over the binary alphabet is interpreted as a version of conjunctive normal form satisfiability problem, where each clause has infinitely many shifted variants. Non-satisfiability of these formulas can be proved using variants of classical propositional proof systems, augmented with derivation rules for shifting proof lines (such as clauses, inequalities, polynomials, etc.). First, it is proved that there is a particular formula that has a short refutation in Resolution with a shift rule but requires classical proofs of exponential size. At the same time, it is shown that exponential lower bounds for classical proof systems can be translated for their shifted versions. Finally, it is shown that superpolynomial lower bounds on the size of shifted proofs would separate NP from PSPACE; a connection to lower bounds on circuit complexity is also established.

Finding small unsatisfiable subformulas (unsat cores) of infeasible propositional SAT problems is an active area of research. Analogous investigations in the polynomial algebra domain are, however, somewhat lacking. This paper investigates an algorithmic approach to identify a small unsatisfiable core of a set of polynomials, where the corresponding polynomial ideal is found to have an empty variety. We show that such a core can be identified by employing extensions of the Buchberger’s algorithm. By further analyzing S-polynomial reductions, we identify certain conditions that are helpful in ascertaining whether or not a polynomial from the given generating set is a part of the unsat core. Our algorithm cannot guarantee a minimal unsat core; the paper describes an approach to refine the identified core. Experiments are performed on a variety of instances using a computer-algebra implementation of our algorithm.

The computational complexity of discrete problems concerning the enumeration of solutions is addressed. The concept of an asymptotically efficient algorithm is introduced for the dualization problem, which is formulated as the problem of constructing irreducible coverings of a Boolean matrix. This concept imposes weaker constraints on the number of “redundant” algorithmic steps as compared with the previously introduced concept of an asymptotically optimal algorithm. When the number of rows in a Boolean matrix is no less than the number of columns (in which case asymptotically optimal algorithms for the problem fail to be constructed), algorithms based on the polynomialtime-delay enumeration of “compatible” sets of columns of the matrix is shown to be asymptotically efficient. A similar result is obtained for the problem of searching for maximal conjunctions of a monotone Boolean function defined by a conjunctive normal form.

With $G_k(n)$ the number of functions of $n$ boolean variables definable by $k$-SAT formulae, we prove that $G_3(n)$ is asymptotic to $2^{n+\binom{n}{3}}$. This is a strong form of the case $k=3$ of a conjecture of Bollob\'as, Brightwell and Leader stating that for fixed $k$, $\log_2 G_k(n)\sim \binom{n}{k}$., Comment: 51 pages

Asymptotic estimates for the typical number of irreducible coverings and the typical length of an irreducible covering of a Boolean matrix are obtained in the case when the number of rows is no less than the number of columns. As a consequence, asymptotic estimates are obtained for the typical number of maximal conjunctions and the typical rank of a maximal conjunction of a monotone Boolean function of variables defined by a conjunctive normal form of clauses. Similar estimates are given for the number of irredundant coverings and the length of an irredundant covering of an integer matrix (for the number of maximal conjunctions and the rank of a maximal conjunction of a two-valued logical function defined by its zero set). Results obtained previously in this area are overviewed.

We consider the problem of the verification of the implementability of a system of partially specified Boolean functions by a multiblock structure in which each block is also determined by a system of partially specified Boolean functions. A method for the solution of the problem by reducing it to the problem of the verification of the satisfiability of a conjunctive normal form that is the union of two the permissible conjunctive normal form of the multiblock structure with the prohibitive conjunctive normal form of the system of partially specified Boolean functions is proposed. Implicative methods for the construction of resolution conjunctive normal forms of multiblock structures with functional indeterminacy are proposed and studied.

Boolean formulas have been widely studied in the field of learning theory. We focus on the model of learning with queries, and study a restriction of the class of k-quasi-Horn formulas, that is, conjunctive normal form formulas where the number of unnegated literals per clause is at most k. This class is known to be as hard to learn as the general class CNF of conjunctive normal form formulas. By imposing some constraints, we define a fragment of this logic that can be learned using only membership queries. Also we prove that none of these constraints makes by itself the class learnable.

In order to more efficiently realize Boolean functions by using neural networks, we propose a binary product-unit neural network (BPUNN) and a binary π-ς neural network (BPSNN). The network weights can be determined by one-step training. It is shown that the addition " σ," the multiplication " π," and two kinds of special weighting operations in BPUNN and BPSNN can implement the logical operators " ∨," " ∧," and " ¬" on Boolean algebra 〈Z(2),∨,∧,¬,0,1〉 (Z(2)={0,1}), respectively. The proposed two neural networks enjoy the following advantages over the existing networks: 1) for a complete truth table of N variables with both truth and false assignments, the corresponding Boolean function can be realized by accordingly choosing a BPUNN or a BPSNN such that at most 2(N-1) hidden nodes are needed, while O(2(N)), precisely 2(N) or at most 2(N), hidden nodes are needed by existing networks; 2) a new network BPUPS based on a collaboration of BPUNN and BPSNN can be defined to deal with incomplete truth tables, while the existing networks can only deal with complete truth tables; and 3) the values of the weights are all simply -1 or 1, while the weights of all the existing networks are real numbers. Supporting numerical experiments are provided as well. Finally, we present the risk bounds of BPUNN, BPSNN, and BPUPS, and then analyze their probably approximately correct learnability.

Circumscription is one of the most important formalisms for reasoning with incomplete information. It is equivalent to reasoning under the extended closed world assumption, which allows to conclude that the facts derivable from a given knowledge base are all facts that satisfy a given property. In this paper, we study the computational complexity of several formalizations of inference in propositional circumscription for the case that the knowledge base is described by a propositional theory using only a restricted set of Boolean functions. To systematically cover all possible sets of Boolean functions, we use Post’s lattice. With its help, we determine the complexity of circumscriptive inference for all but two possible classes of Boolean functions. Each of these problems is shown to be either $\protect \ensuremath {\mathrm {\Pi ^{\mathrm{p}}_{2}}}$ -complete, coNP-complete, or solvable in logspace. In particular, we show that in the general case, unless P=NP, only literal theories admit polynomial-time algorithms, while for some restricted variants the tractability border is the same as for classical propositional inference.

The average sensitivity of a Boolean function is the expectation, given a uniformly random input, of the number of input bits which when flipped change the output of the function. Answering a question by O'Donnell, we show that every Boolean function represented by a k-CNF (or a k-DNF) has average sensitivity at most k. This bound is tight since the parity function on k variables has average sensitivity k.

We consider the problem of generalising boolean formulas in conjunctive normal form by allowing non-boolean variables, with the goal of maintaining combinatorial properties. Requiring that a literal involves only a single variable, the most general form of literals are the wellknown “signed literals”, corresponding to unary constraints in CSP. However we argue that only the restricted form of “negative monosigned literals” and the resulting generalised clause-sets, corresponding to “sets of no-goods” in the AI literature, maintain the essential properties of boolean conjunctive normal forms. In this first part of a mini-series of two articles, we build up a solid foundation for (generalised) clause-sets, including the notion of autarky systems, the interplay between autarkies and resolution, and basic notions of (DP-)reductions. As a basic combinatorial parameter of generalised clause-sets we introduce the (generalised) notion of deficiency, which in the boolean case is the difference between the number of clauses and the number of variables. Autarky theory plays a fundamental role here, and we concentrate especially on matching autarkies (based on matching theory). A natural task is to determine the structure of (matching) lean clause-sets, which do not admit non-trivial (matching) autarkies. A central result is the computation of the lean kernel (the largest lean subset) of a (generalised) clause-set in polynomial time for bounded maximal deficiency.