Search

The belief revision process involves several problems considered hard. One of the crucial problems is how to represent to the knowledge base K to consider, as well as how to represent and to add new information , which may even be contradictory to the knowledge base. In this work, both the knowledge base and the new information are in conjunctive normal form. Each clause of a conjunctive normal form is encoded by a string consisting of: 0, 1, *, representing the falsifying assignments of the clause. To use the falsifying assignments of the clauses allows to perform efficiently different logical operators among conjunctive forms. Our belief revision process (K * ) between conjunctive forms is based on solving first the propositional inference, i.e. K = . Based on to count falsifying assignments represented by tertiary chains, an algorithmic proposal is made that allows to determine in a practical way, when (K E ( K * )) is inconsistent. Finally, the time-complexity analysis of our algorithmic proposal is carried out.

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.

An inference approach is proposed by formulating reasoning processes as particular evolutions of Petri nets. It can be used to design an intelligent agent that executes tasks in a given environment. First, a symbol Petri net is defined to represent a Boolean variable describing a distinct aspect of an environment. Second, a propositional logic sentence in a conjunctive normal form, which may express some background knowledge or a sequence of percepts made by an agent, is formulated as a linear constraint, called as a semantic constraint. Third, an algorithm is constructed to design monitor places enforcing semantic constraints on symbol Petri nets, and its resultant net is called a knowledge Petri net representing relevant knowledge. Fourth, a reasoning algorithm is presented based on a newly defined transition-firing rule of the knowledge Petri net, and can be used to infer or reveal hidden facts. The proposed inference algorithm is efficient since its time computational complexity is proven to be polynomial with respect to the number of Boolean variables. The wumpus world problem is taken as an example to illustrate and verify it.

Context logic (CL), a logical language similar in style to description logics but with a more cognitive motivation as a logical language of cognition, was developed since 2007 to provide a new approach to the symbol grounding problem, a key problem for reliable intelligent environments and other intelligent sensory systems. CL is a three-layered integrated hierarchy of languages: a relational base layer with the expressiveness of propositional logic (CLA), a quantifier-free decidable language (CL0), and an expressive language with full quantification (CL1). As was shown in 2018, the core CLA reasoning can be implemented on a variant of Kanerva’s Vector Symbolic Architecture, the activation bit vector machine (ABVM), shedding new light on the fundamental cognitive faculties of symbol grounding and imagery, but the system raised two questions: first, the core reasoning algorithm was a classical EXPTIME reasoner; second, fundamental aspects for a learning algorithm were sketched but not presented with a full algorithm. This paper addresses those two questions. We present a probabilistic linear time algorithm for reasoning over conjunctive normal form (CNF) CLA formulae together with a dual probabilistic linear time algorithm for learning CLA statements by collecting experienced snapshots in a disjunctive normal form (DNF).

To enhance the user’s privacy in electronic ID, anonymous credential systems have been researched. In the anonymous credential system, a trusted issuing organization first issues a certificate certifying the user’s attributes to a user. Then, in addition to the possession of the certificate, the user can anonymously prove only the necessary attributes. Previously, an anonymous credential system was proposed, where CNF (Conjunctive Normal Form) formulas on attributes can be proved. The advantage is that the attribute proof in the authentication has the constant size for the number of attributes that the user owns and the size of the proved formula. Thus, various expressive logical relations on attributes can be efficiently verified. However, the previous system has a limitation: the proved CNF formulas cannot include any negation. Therefore, in this paper, we propose an anonymous credential system with constant-size attribute proofs such that the user can prove CNF formulas with negations. For the proposed system, we extend the previous accumulator for the limited CNF formulas to verify CNF formulas with negations.

In Model-Based Diagnosis (MBD), we concern ourselves with the health and safety of physical and software systems. Although we often use different knowledge representations and algorithms, some tools like satisfiability (SAT) solvers and temporal logics, are used in both domains. In this paper we introduce Finite Trace Next Logic (FTNL) models of sequential circuits and propose an enhanced algorithm for computing minimal-cardinality diagnoses. Existing state-of-the-art satisfiability algorithms for minimal diagnosis use Sorting Networks (SNs) for constraining the cardinality of the diagnostic candidates. In our approach we exploit Multi-Operand Adders (MOAs). Based on extensive tests with ISCAS-89 circuits, we found that MOAs enable Conjunctive Normal Form (CNF) encodings that are significantly more compact. These encodings lead to 19.7 to 67.6 times fewer variables and 18.4 to 62 times fewer clauses. For converting an FTNL model to CNF, we could achieve a speed-up ranging from 6.2 to 22.2. Using SNs fosters 3.4 to 5.5 times faster on-line satisfiability checking though. This makes MOAs preferable for applications where RAM and off-line time are more limited than on-line CPU time.

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.

Alloy is a declarative modeling language based on a first-order relational logic. Its constraint-based analysis has enabled a wide range of applications in software engineering, including configuration synthesis, bug finding, test-case generation, and security analysis. Certain types of analysis tasks in these domains involve finding an optimal solution. For example, in a network configuration problem, instead of finding any valid configuration, it may be desirable to find one that is most permissive (i.e., it permits a maximum number of packets). Due to its dependence on SAT, however, Alloy cannot be used to specify and analyze these types of problems. We propose AlloyMax, an extension of Alloy with a capability to express and analyze problems with optimal solutions. AlloyMax introduces (1) a small addition of language constructs that can be used to specify a wide range of problems that involve optimality and (2) a new analysis engine that leverages a Maximum Satisfiability (MaxSAT) solver to generate optimal solutions. To enable this new type of analysis, we show how a specification in a first-order relational logic can be translated into an input format of MaxSAT solvers—namely, a Boolean formula in weighted conjunctive normal form (WCNF). We demonstrate the applicability and scalability of AlloyMax on a benchmark of problems. To our knowledge, AlloyMax is the first approach to enable analysis with optimality in a relational modeling language, and we believe that AlloyMax has the potential to bring a wide range of new applications to Alloy.

Logic obfuscation is introduced as a pivotal defense mechanism against emerging hardware threats on Integrated Circuits (ICs) such as reverse engineering (RE) and intellectual property (IP) theft. The effectiveness of logic obfuscation is challenged by recently introduced Boolean satisfiability (SAT) attack and it's variants. A plethora of counter measures have been proposed to thwart the SAT attacks. Irrespective of the implemented defenses, large power, performance and area (PPA) overheads are seen to be indispensable. In contrast, we propose a neural network-based cognitive SAT to SAT-hard clause translator under the constraints of minimal PPA overheads while preserving the original functionality with impenetrable security. Our proposed method is incubated with a SAT-hard clause generator that translates the existing conjunctive normal form (CNF) through minimal perturbations such as inclusion of pair of inverters or buffers or adding new lightweight SAT-hard block depending on the provided CNF. For efficient SAT-hard clause generation, the proposed method is equipped with a multi-layer neural network that first learns the dependencies of features (literals and clauses), followed by a long-short-term-memory (LSTM) network to validate and backpropagate the SAT-hardness for better learning and translation. For a fair comparison with the state-of-the-art, we evaluate our proposed technique on ISCAS'85 benchmarks. It is seen to successfully defend against multiple state-of-the-art SAT attacks devised for hardware RE. In addition, we also evaluate our proposed technique's empirical performance against MiniSAT, Lingeling and Glucose SAT solvers that form the base for numerous existing deobfuscation SAT attacks.

A k-CNF (conjunctive normal form) formula is a regular (k, s)-CNF one if every variable occurs s times in the formula, where k ⩾ 2 and s > 0 are integers. Regular (3, s)-CNF formulas have some good structural properties, so carrying out a probability analysis of the structure for random formulas of this type is easier than conducting such an analysis for random 3-CNF formulas. Some subclasses of the regular (3, s)-CNF formula have also characteristics of intractability that differ from random 3-CNF formulas. For this purpose, we propose strictly d-regular (k, 2s)-CNF formula, which is a regular (k, 2s)-CNF formula for which d ⩾ 0 is an even number and each literal occurs $$s - {d \over 2}$$ or $$s + {d \over 2}$$ times (the literals from a variable x are x and ¬x, where x is positive and ¬x is negative). In this paper, we present a new model to generate strictly d-regular random (k, 2s)-CNF formulas, and focus on the strictly d-regular random (3, 2s)-CNF formulas. Let F be a strictly d-regular random (3, 2s)-CNF formula such that 2s > d. We show that there exists a real number s0 such that the formula F is unsatisfiable with high probability when s > s0, and present a numerical solution for the real number s0. The result is supported by simulated experiments, and is consistent with the existing conclusion for the case of d = 0. Furthermore, we have a conjecture: for a given d, the strictly d-regular random (3, 2s)-SAT problem has an SAT-UNSAT (satisfiable-unsatisfiable) phase transition. Our experiments support this conjecture. Finally, our experiments also show that the parameter d is correlated with the intractability of the 3-SAT problem. Therefore, our research maybe helpful for generating random hard instances of the 3-CNF formula.

When creating benchmarks for satisfiability (SAT) solvers, we need Conjunctive Normal Form (CNF) instances that are easy to build but hard to solve. A recent development in the search for such methods has led to the Balanced SAT algorithm, which can create k -CNF instances with m clauses of high difficulty, for arbitrary k and m . In this article, we introduce the No-Triangle CNF algorithm, a CNF instance generator based on the cluster coefficient graph statistic. We empirically compare the two algorithms by fixing the arity and the number of variables, but varying the number of clauses. We find that the hardest instances produced by each method belong to different constrainedness regions. In the 3-CNF case, for example, hard No-Triangle CNF instances reside in the highly-constrained region (many clauses), while Balanced SAT instances obtained from the same parameters are easy to solve. This allows us to generate difficult instances where existing algorithms fail to do so.

Logic obfuscation emerged as an efficient solution to strengthen the security of integrated circuits (ICs) from multiple threats including reverse engineering and intellectual property (IP) theft. Emergence of Boolean Satisfiability (SAT) attacks and its variants have shown to circumvent the security mechanisms such as obfuscation and a plethora of its variants. A plethora of advanced security defenses to thwart the SAT attacks are introduced. Despite the effectiveness, the imposed overheads in terms of area and power are unacceptably high. In contrast, our current work focuses on devising an iterative, dynamic and intelligent SAT-hard clause generator for a given SAT-prone problem, termed as SATConda. The SATConda is a SAT-hard clause generator that utilizes a bipartite propagation based neural network model. The utilized model comprises multiple layers of artificial neural networks to extract the dependencies of literals and variables, followed by long short term memory (LSTM) networks to validate the SAT hardness. The SATConda is trained with conjunctive normal form (CNF) of the IC netlist that are both SAT solvable and SAT-hard. Further, the SATConda is equipped with a SAT-clause generator to convert a CNF from satisfiable (SAT) to unsatisfiable (unSAT) with minor perturbation (which translates to minor overheads) so that the SAT-attack cannot decrypt the keys. To the best of our knowledge, no previous work has been reported on neural network based SAT-hard clause or CNF translator for circuit obfuscation. We evaluate our proposed SATConda's empirical performance against MiniSAT, Lingeling and Glucose SAT solvers on ISCAS'85 benchmark circuits.

The enumeration of the maximal satisfiable subsets (MSSes) or the minimal correction subsets (MCSes) of conjunctive normal form (CNF) formulas is a cornerstone task in various AI domains. This paper presents an algorithm that enumerates all MCSes with SAT oracles. Our algorithm is simple because it follows a plain algorithm without any techniques that decrease the number of calls to a SAT oracle. The experimental results show that our proposed method is more efficient than state-of-the-art MCS enumerators on average to deal with Partial-MaxSAT instances.

Author name disambiguation (AND) algorithms identify a unique author entity record from all similar or same publication records in scholarly or similar databases. Typically, a clustering method is used that requires calculation of similarities between each possible record pair. However, the total number of pairs grows quadratically with the size of the author database making such clustering difficult for millions of records. One remedy is a blocking function that reduces the number of pairwise similarity calculations. Here, we introduce a new way of learning blocking schemes by using a conjunctive normal form (CNF) in contrast to the disjunctive normal form (DNF). We demonstrate on PubMed author records that CNF blocking reduces more pairs while preserving high pairs completeness compared to the previous methods that use a DNF and that the computation time is significantly reduced. In addition, we also show how to ensure that the method produces disjoint blocks so that much of the AND algorithm can be efficiently paralleled. Our CNF blocking method is tested on the entire PubMed database of 80 million author mentions and efficiently removes 82.17% of all author record pairs in 10 minutes.

It is useful to have general-purpose solution methods that can be applied to a wide range of problems, rather than relying on the development of clever, intricate algorithms for each specific problem. Integer Linear Programming is the most widely-used such general-purpose solution method. It is successful in a wide range of problems. However, there are some problems in computational biology where integer linear programming has had only limited success. In this paper, we explore an alternate, general-purpose solution method: SAT-solving, i.e., constructing Boolean formulas in conjunctive normal form (CNF) that encode a problem instance, and using a SAT-solver to determine if the CNF formula is satisfiable or not. In three hard problems examined, we were very surprised to find the SAT-solving approach was dramatically better than the ILP approach in two problems; and a little slower, but more robust, in the third problem. We also re-examined and confirmed an earlier result on a fourth problem, using current ILP and SAT-solvers. These results should encourage further efforts to exploit SAT-solving in computational biology.

We develop an idea originally proposed by Michel and Van Hentenryck of how to perform bit-vector constraint propagation on the word level. Most operations are propagated in constant time, assuming the bit-vector fits in a machine word. In contrast, bit-vector SMT solvers usually solve bit-vector problems by (ultimately) bit-blasting, that is, mapping the resulting operations to conjunctive normal form clauses, and using SAT technology to solve them. Bit-blasting generates intermediate variables which can be an advantage, as these can be searched on and learnt about. As each approach has advantages, it makes sense to try to combine them. In this paper, we describe an approach to bit-vector solving using word-level propagation with learning. We have designed alternative word-level propagators to Michel and Van Hentenryck’s, and evaluated different variants of the approach. We have also experimented with different approaches to learning and back-jumping in the solver. Based on the insights gained, we have built a portfolio solver, Wombit, which essentially extends the STP bit-vector solver. Using machine learning techniques, the solver makes a judicious up-front decision about whether to use word-level propagation or fall back on bit-blasting.

The Boolean SATisfiability problem (SAT) is of central importance in computer science. Although SAT is known to be NP-complete, progress on the engineering side, especially that of Conflict-Driven Clause Learning (CDCL) and Local Search SAT solvers, has been remarkable. Yet, while SAT solvers aimed at solving industrial-scale benchmarks in Conjunctive Normal Form (CNF) have become quite mature, SAT solvers that are effective on other types of constraints, e.g., cardinality constraints and XORs, are less well studied; a general approach to handling non-CNF constraints is still lacking. In addition, previous work indicated that for specific classes of benchmarks, the running time of extant SAT solvers depends heavily on properties of the formula and details of encoding, instead of the scale of the benchmarks, which adds uncertainty to expectations of running time. To address the issues above, we design FourierSAT, an incomplete SAT solver based on Fourier analysis of Boolean functions, a technique to represent Boolean functions by multilinear polynomials. By such a reduction to continuous optimization, we propose an algebraic framework for solving systems consisting of different types of constraints. The idea is to leverage gradient information to guide the search process in the direction of local improvements. Empirical results demonstrate that FourierSAT is more robust than other solvers on certain classes of benchmarks., The paper was accepted by Thirty-Fourth AAAI Conference on Artificial Intelligence (AAAI 2020). V2 (Feb 24): Typos corrected

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.

The Boolean SATisfiability problem (SAT) is of central importance in computer science. Although SAT is known to be NP-complete, progress on the engineering side—especially that of Conflict-Driven Clause Learning (CDCL) and Local Search SAT solvers—has been remarkable. Yet, while SAT solvers, aimed at solving industrial-scale benchmarks in Conjunctive Normal Form ( CNF ), have become quite mature, SAT solvers that are effective on other types of constraints (e.g., cardinality constraints and XOR s) are less well-studied; a general approach to handling non- CNF constraints is still lacking. To address the issue above, we design FourierSAT , 1 an incomplete SAT solver based on Fourier Analysis (also known as Walsh-Fourier Transform) of Boolean functions, a technique to represent Boolean functions by multilinear polynomials. By such a reduction to continuous optimization, we propose an algebraic framework for solving systems consisting of different types of constraints. The idea is to leverage gradient information to guide the search process in the direction of local improvements. We show this reduction enjoys interesting theoretical properties. Empirical results demonstrate that FourierSAT can be a useful complement to other solvers on certain classes of benchmarks.

LTL is frequently used to express specifications in many domains such as embedded systems or business processes. Witnesses can help to understand why an LTL specification is satisfiable, and a number of approaches exist to make understanding a witness easier. In the case of unsatisfiable specifications unsatisfiable cores (UCs), i.e., parts of an unsatisfiable formula that are themselves unsatisfiable, are a well established means for debugging. However, little work has been done to help understanding a UC of an unsatisfiable LTL formula. In this paper we suggest to enhance a UC of an unsatisfiable LTL formula with additional information about the time points at which the subformulas of the UC are relevant for unsatisfiability. For example, in "(G p) and (X not p)" the first occurrence of "p" is really only "relevant" for unsatisfiability at time point 1 (time starts at time point 0). We present a method to extract such information from the resolution graph of a temporal resolution proof of unsatisfiability of an LTL formula. We implement our method in TRP++, and we experimentally evaluate it. Source code of our tool is available., In Proceedings QAPL 2013, arXiv:1306.2413

Logic obfuscation emerged as an efficient solution to strengthen the security of integrated circuits (ICs) from multiple threats including reverse engineering and intellectual property (IP) theft. Emergence of Boolean Satisfiability (SAT) attacks and its variants have shown to circumvent the security mechanisms such as obfuscation and a plethora of its variants. Considering the size of ICs and the amount of time it takes to validate a defense i.e., obfuscation against SAT attack could range from few ms to days. In contrast, our current work focuses on devising an iterative, dynamic and intelligent SAT-hard clause generator for a given SAT-prone problem. The proposed Machine Learning (ML)-based SAT to unSAT clause translator is a SAT-hard clause generator that utilizes a bipartite propagation based neural network model. The utilized model comprises multiple layers of artificial neural networks to extract the dependencies of literals and variables, followed by long short term memory (LSTM) networks to validate the SAT hardness. The proposed ML-based SAT to unSAT clause translator is trained with conjunctive normal form (CNF) of the IC netlist that are both SAT solvable and SAT-hard. Further, the model is also trained to convert a CNF from satisfiable (SAT) to unsatisfiable (unSAT) form with minor perturbation (which translates to minor overheads) so that the SAT-attack cannot decrypt the keys. To the best of our knowledge, no previous work has been reported on neural network based SAT-hard clause or CNF translator for circuit obfuscation. We evaluate our proposed models's empirical performance against MiniSAT with 300 CNFs.

Probabilistic Boolean Networks (PBNs) have been previously proposed so as to gain insights into complex dy- namical systems. However, identification of large networks and of the underlying discrete Markov Chain which describes their temporal evolution, still remains a challenge. In this paper, we introduce an equivalent representation for the PBN, the Stochastic Conjunctive Normal Form (SCNF), which paves the way to a scalable learning algorithm and helps predict long- run dynamic behavior of large-scale systems. Moreover, SCNF allows its efficient sampling so as to statistically infer multi- step transition probabilities which can provide knowledge on the activity levels of individual nodes in the long run., Comment: 16 pages

EPIA Conference on Artificial Intelligence (19th. 2019. Vila Real, Portugal), This research is supported by the Spanish Government under project TIN2016-79190-R and by the Principality of Asturias under grant IDI/2018/000176. This work is also supported by FCT grants ABSOLV (PTDC/CCI-COM/28986/2017) and FaultLocker (PTDC/CCI-COM/29300/2017).

The Boolean satisfiability problem (SAT) remains a central problem to theoretical as well as practical computer science. Recently, the need to trust the results obtained by SAT solvers has led to research in formalizing these. Nevertheless, tools in the ecosystem of SAT problems (such as preprocessors, model counters, etc.) would need to be verified as well in order for the results to be trusted. In this paper we explore a step towards a formalized symmetry breaking tool for SAT: formalizing SAT symmetry breaking for formulas in conjunctive normal form (CNF) using the Prototype Verification System (PVS).

To enhance the user’s privacy in electronic ID, anonymous credential systems have been researched. In the anonymous credential system, a trusted issuing organization first issues a certificate certifying the user’s attributes to a user. Then, in addition to the possession of the certificate, the user can anonymously prove only the necessary attributes. Previously, an anonymous credential system was proposed, where CNF (Conjunctive Normal Form) formulas on attributes can be proved. The advantage is that the attribute proof in the authentication has the constant size for the number of attributes that the user owns and the size of the proved formula. Thus, various expressive logical relations on attributes can be efficiently verified. However, the previous system has a limitation: the proved CNF formulas cannot include any negation. Therefore, in this paper, we propose an anonymous credential system with constant-size attribute proofs such that the user can prove CNF formulas with negations. For the proposed system, we extend the previous accumulator for the limited CNF formulas to verify CNF formulas with negations.

Algebraic Normal Form (ANF) and Conjunctive Normal Form (CNF) are commonly used to encode problems in Boolean algebra. ANFs are typically solved via Gr"obner basis algorithms, often using more memory than is feasible; while CNFs are solved using SAT solvers, which cannot exploit the algebra of polynomials naturally. We propose a paradigm that bridges between ANF and CNF solving techniques: the techniques are applied in an iterative manner to emph{learn facts} to augment the original problems. Experiments on over 1,100 benchmarks arising from four different applications domains demonstrate that learnt facts can significantly improve runtime and enable more benchmarks to be solved., To Appear in Proceedings of DATE 2019

In Software-Defined Networking (SDN) it is important to efficiently partition the rule table into sub-tables and distribute them to the multiple switches over the network. In this paper we proposed an optimal rule table distribution strategy by applying satisfiability (SAT)-based approach. N-coloring problem for partitioning is formulated as conjunctive normal form (CNF), and by repeatedly running SAT solver we can obtain maximum number of partitions.

Static verification techniques leverage Boolean formula satisfiability solvers such as SAT and SMT solvers that operate on conjunctive normal form and first order logic formulae, respectively, to validate programs. They force bounds on variable ranges and execution time and translate the program and its specifications into a Boolean formula. They are limited to programs of relatively low complexity for the following reasons. (1) A small increase in the bounds can cause a large increase in the size of the translated formula. (2) Boolean satisfiability solvers are restricted to using optimizations that apply at the level of the formula. Finally, (3) the Boolean formulae often need to be regenerated with higher bounds to ensure the correctness of the translation. We present a method that uses And-Inverter-Graph (AIG) sequential circuits, and AIG synthesis and verification frameworks to validate programs. An AIG is a Boolean formula with memory elements, logically complete negated conjunction gates, and a hierarchical structure. Encoding the validation problem of a program as an AIG (1) typically provides a more succinct representation than a Boolean formulae encoding with no memory elements, (2) preserves the high-level structure of the program, and (3) enables the use of a number of powerful automated analysis techniques that have no counterparts for other Boolean formulae such as CNF. Our method takes an imperative program with a first order logic specification consisting of a precondition and a postcondition pair, and a bound on the program variable ranges, and produces an AIG with a designated output that is ${true}$ when the program violates the specification. Our method uses AIG synthesis reduction techniques to reduce the AIG, and then uses AIG verification techniques to check the satisfiability of the designated output. The results show that our method can validate designs that are not possible with other state of the art techniques, and with bounds that are an order of magnitude larger.

Many Automated Theorem Prover (ATP) systems for different logical forms, and translators for translating different logical forms from one to another, have been developed and are now available. Some logical forms are more expressive than others, and it is easier to express problems in those forms. On the other hand, the ATP systems for less expressive forms have been tested for many years, and are more powerful and reliable. There is a trade-off between expressivity of a logical form, and power and reliability of the available ATP systems. Different ATP systems and translators can be combined to solve a problem expressed in a logic. In this research, an experiment has been designed and carried out to compare all different possible ways of trying to solve a problem. The possibilities are either to use an ATP system for the original form, or translate the problem to a less expressive form. If the problem is translated to a less expressive form, then again the same two possibilities are available, until no further translation is possible. No translator was available to translate from Conjunctive Normal Form to Description Logic, which sits between Effectively Propositional Logic and Propositional Logic in terms of expressivity. A translation procedure for translating Conjunctive Normal Form to Description Logic, and its implementation as Saffron are presented. Additionally, this research includes a survey of different logical forms. Propositional Logic, Description Logic, First Order Form, Conjunctive Normal Form, Effectively Propositional, Typed First order Form - monomorphic, Typed First order Form - polymorphic, Typed Higher order Form - monomorphic. The properties, syntax, and semantics of each logical form are briefly described. For each form, the most popular ATP systems and translators for translating to a less expressive forms are introduced.

We present an experimental study of the effects of quantifier alternations on the evaluation of quantified Boolean formula (QBF) solvers. The number of quantifier alternations in a QBF in prenex conjunctive normal form (PCNF) is directly related to the theoretical hardness of the respective QBF satisfiability problem in the polynomial hierarchy. We show empirically that the performance of solvers based on different solving paradigms substantially varies depending on the numbers of alternations in PCNFs. In related theoretical work, quantifier alternations have become the focus of understanding the strengths and weaknesses of various QBF proof systems implemented in solvers. Our results motivate the development of methods to evaluate orthogonal solving paradigms by taking quantifier alternations into account. This is necessary to showcase the broad range of existing QBF solving paradigms for practical QBF applications. Moreover, we highlight the potential of combining different approaches and QBF proof systems in solvers.

© 2018, International Association for Cryptologic Research. We carry out a systematic study of the GGH15 graded encoding scheme used with general branching programs. This is motivated by the fact that general branching programs are more efficient than permutation branching programs and also substantially more expressive in the read-once setting. Our main results are as follows: Proofs. We present new constructions of private constrained PRFs and lockable obfuscation, for constraints (resp. functions to be obfuscated) that are computable by general branching programs. Our constructions are secure under LWE with subexponential approximation factors. Previous constructions of this kind crucially rely on the permutation structure of the underlying branching programs. Using general branching programs allows us to obtain more efficient constructions for certain classes of constraints (resp. functions), while posing new challenges in the proof, which we overcome using new proof techniques.Attacks. We extend the previous attacks on indistinguishability obfuscation (iO) candidates that use GGH15 encodings. The new attack simply uses the rank of a matrix as the distinguisher, so we call it a “rank attack”. The rank attack breaks, among others, the iO candidate for general read-once branching programs by Halevi, Halevi, Shoup and Stephens-Davidowitz (CCS 2017).Candidate Witness Encryption and iO. Drawing upon insights from our proofs and attacks, we present simple candidates for witness encryption and iO that resist the existing attacks, using GGH15 encodings. Our candidate for witness encryption crucially exploits the fact that formulas in conjunctive normal form (CNFs) can be represented by general, read-once branching programs.

This paper presents algorithms, both for probabilistic satisfiability and for coherence checking, that rely on reduction to integer programming. That is, we verify whether probabilistic assessments can be satisfied by standard probability measures (Kolmogorovian setting) or by full conditional probabilities (de Finettian coherence setting), and in both cases verify satisfiability or coherence using integer programming techniques. We present an empirical evaluation of our method, the results of which show evidence of phase transitions. Paper offers solution to probabilistic satisfiability (PSAT) problems.Proposed solution by reduction to integer linear programming.Paper presents several variants of PSAT.Paper deals with coherence checking by integer programming.Paper shows empirical evidence of phase transition in PSAT.

Interpolation-based model checking (ITP) McMillan (in CAV, 2003) is an efficient and complete model checking procedure. However, for large problems, interpolants generated by ITP might become extremely large, rendering the procedure slow or even intractable. In this work we present a novel technique for interpolant generation in the context of model checking. The main novelty of our work is that we generate small interpolants in conjunctive normal form (CNF) using a twofold procedure: first we propose an algorithm that exploits resolution refutation properties to compute an interpolant approximation. Then we introduce an algorithm that takes advantage of inductive reasoning to turn the interpolant approximation into an interpolant. Unlike ITP, our approach maintains only the relevant subset of the resolution refutation. In addition, the second part of the procedure exploits the properties of the model checking problem at hand, in contrast to the general-purpose algorithm used in ITP. We developed a new interpolation-based model checking algorithm, called CNF-ITP. Our algorithm takes advantage of the smaller interpolants and exploits the fact that the interpolants are given in CNF. We integrated our method into a SAT-based model checker and experimented with a representative subset of the HWMCC'12 benchmark set. Our experiments show that, overall, the interpolants generated by our method are 117 times smaller than those generated by ITP. Our CNF-ITP algorithm outperforms ITP, and at times solves problems that ITP cannot solve. We also compared CNF-ITP to the successful IC3 Bradely (in VMCAI, volume 6538 of lecture notes in computer science, 2011) algorithm. We found that CNF-ITP outperforms IC3 Bradely (in VMCAI, volume 6538 of lecture notes in computer science, 2011) in a large number of cases.

Branch decomposition is a prominent method for structurally decomposing a graph, a hypergraph, or a propositional formula in conjunctive normal form. The width of a branch decomposition provides a measure of how well the object is decomposed. For many applications, it is crucial to computing a branch decomposition whose width is as small as possible. We propose an approach based on Boolean Satisfiability (SAT) to finding branch decompositions of small width. The core of our approach is an efficient SAT encoding that determines with a single SAT-call whether a given hypergraph admits a branch decomposition of a certain width. For our encoding, we propose a natural partition-based characterization of branch decompositions. The encoding size imposes a limit on the size of the given hypergraph. To break through this barrier and to scale the SAT approach to larger instances, we develop a new heuristic approach where the SAT encoding is used to locally improve a given candidate decomposition until a fixed-point is reached. This new SAT-based local improvement method scales now to instances with several thousands of vertices and edges.

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

We present the latest major release version 6.0 of the quantified Boolean formula (QBF) solver DepQBF, which is based on QCDCL. QCDCL is an extension of the conflict-driven clause learning (CDCL) paradigm implemented in state of the art propositional satisfiability (SAT) solvers. The Q-resolution calculus (QRES) is a QBF proof system which underlies QCDCL. QCDCL solvers can produce QRES proofs of QBFs in prenex conjunctive normal form (PCNF) as a byproduct of the solving process. In contrast to traditional QCDCL based on QRES, DepQBF 6.0 implements a variant of QCDCL which is based on a generalization of QRES. This generalization is due to a set of additional axioms and leaves the original Q-resolution rules unchanged. The generalization of QRES enables QCDCL to potentially produce exponentially shorter proofs than the traditional variant. We present an overview of the features implemented in DepQBF and report on experimental results which demonstrate the effectiveness of generalized QRES in QCDCL.

Recent work on searchable symmetric encryption (SSE) has focused on increasing its expressiveness. A notable example is the OXT construction (Cash et al., CRYPTO ’13) which is the first SSE scheme to support conjunctive keyword queries with sub-linear search complexity. While OXT efficiently supports disjunctive and boolean queries that can be expressed in searchable normal form, it can only handle arbitrary disjunctive and boolean queries in linear time. This motivates the problem of designing expressive SSE schemes with worst-case sub-linear search; that is, schemes that remain highly efficient for any keyword query.

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.

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.

GSAT is a well-known satisfiability search algorithm for conjunctive normal forms. GSAT uses some random functions. One of such functions is a function of starting population of truth assignments for the variables of conjunctive normal form. In this paper, we consider a method of artificial physics optimization for computing a function of starting population.

Testing of digital circuits seems to be a completely mastered part of the design flow, but Constrained Test Patterns Generation (CTPG) is still a highly evolving branch of digital circuits testing. Our previous research on CTPG proved that we can benefit from an implicit representation of test patterns set. The set of test patterns is implicitly represented as a Boolean formula satisfiability problem in CNF, like in common SAT-based ATPGs. However, the CTPG process can be much more memory or time consuming than common TPG, thus some techniques of speeding up the constrained SAT-based test patterns generation are described and analyzed into detail in this paper. These techniques are experimentally evaluated on a real SAT-based algorithm performing a test compression based on overlapping of test patterns. Experiments are performed on ISCAS'85, '89 and ITC'99 benchmark circuits. Results of the experiments are discussed and recommendations for further development of similar SAT-based tools for CTPG are given.

International audience; Building a meaningful model of biological regulatory network is usually done by specifying the components (e.g. the genes) and their interactions, by guessing the values of parameters, by comparing the predicted behaviors to the observed ones, and by modifying in a trial-error process both architecture and parameters in order to reach an optimal fitness. We propose here a different approach to construct and analyze biological models avoiding the trial-error part, where structure and dynamics are represented as formal constraints. We apply the method to Hopfield-like networks, a formalism often used in both neural and regulatory networks modeling. The aim is to characterize automatically the set of all models consistent with all the available knowledge (about structure and behavior). The available knowledge is formalized into formal constraints. The latter are compiled into Boolean formula in conjunctive normal form and then submitted to a Boolean satisfiability solver. This approach allows to formulate a wide range of queries, expressed in a high level language, and possibly integrating formalized intuitions. In order to explore its potential, we use it to find cycles for 3-nodes networks and to determine the flower morphogenesis regulatory network of Arabidopsis thaliana. Applications of this technique are numerous and concern the building of models from data as well as the design of biological networks possessing specified behaviors.

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.

We study the parametrisation of QBF resolution calculi by dependency schemes. One of the main problems in this area is to understand for which dependency schemes the resulting calculi are sound. Towards this end we propose a semantic framework for variable independence based on ‘exhibition’ by QBF models, and use it to express a property of dependency schemes called full exhibition that is known to be sufficient for soundness in Q-resolution. Introducing a generalised form of the long-distance resolution rule, we propose a complete parametrisation of classical long-distance Q-resolution, and show that full exhibition remains sufficient for soundness. We demonstrate that our approach applies to the current research frontiers by proving that the reflexive resolution path dependency scheme is fully exhibited.

Reasoning with bit-vectors arises in a variety of applications in verification and cryptography. Michel and Van Hentenryck have proposed an interesting approach to bit-vector constraint propagation on the word level. Each of the operations except comparison are constant time, assuming the bit-vector fits in a machine word. In contrast, bit-vector SMT solvers usually solve bit-vector problems by bit-blasting, that is, mapping the resulting operations to conjunctive normal form clauses, and using SAT technology to solve them. This also means generating intermediate variables which can be an advantage, as these can be searched on and learnt about. Since each approach has advantages it is important to see whether we can benefit from these advantages by using a word-level propagation approach with learning. In this paper we describe an approach to bit-vector solving using word-level propagation with learning. We provide alternative word-level propagators to Michel and Van Hentenryck, and give the first empirical evaluation of their approach that we are aware of. We show that, with careful engineering, a word-level propagation based approach can compete with (or complement) bit-blasting.

Quantitative Information Flow Analysis (QIF) measures the loss of an attacker’s uncertainty about the confidential information (pre-image) inside a software system after observing the system outputs (image). In this paper, we supplement the SAT-based QIF analysis for deterministic and terminating C programs, by introducing three algorithms for counting the pre-images and images, which utilizes advantages of incremental SAT solvers. Our tool sharpPI is competitive to mql, quail and chimp. An implementation is provided under http://formal.iti.kit.edu/sharpPI.

Given an inconsistent set of constraints, an often studied problem is to compute an irreducible subset of the constraints which, if relaxed, enable the remaining constraints to be consistent. In the case of unsatisfiable propositional formulas in conjunctive normal form, such irreducible sets of constraints are referred to as Minimal Correction Subsets (MCSes). MCSes find a growing number of applications, including the approximation of maximum satisfiability and as an intermediate step in the enumeration of minimal unsatisfiability. A number of efficient algorithms have been proposed in recent years, which exploit a wide range of insights into the MCS extraction problem. One open question is to find the best worst-case number of calls to a SAT oracle, when the calls to the oracle are kept simple, and given reasonable definitions of simple SAT oracle calls. This paper develops novel algorithms for computing MCSes which, in specific settings, are guaranteed to require asymptotically fewer than linear calls to a SAT oracle, where the oracle calls can be viewed as simple. The experimental results, obtained on existing problem instances, demonstrate that the new algorithms contribute to improving the state of the art.