China
Africa
Explore chapters and articles related to this topic
Basic Concepts
Published in Michael Pecht, Placement and Routing of Electronic modules, 2020
Guoqing Li, Yeun Tsun Wong, Michael Pecht
Let A1,A2,..., denote Boolean variables (either true or false). Let A¯1,A2¯,...,,..., denote the negation of A1,A2,..., respectively. A literal is either a variable or its negation. A formula in the propositional calculus is an expression that can be constructed using literals and the logical operations AND and OR. An arbitrary logical expression can be expressed in the conjunctive normal form by using Boolean algebra (section 1.1.4). The satisfiability problem (SAT) is to determine if a formula is true for some assignment of truth values to the variables.
Models and Algorithms for Machine Scheduling with Setup Times
Published in Cornelius Leondes, Computer-Aided Design, Engineering, and Manufacturing, 2019
Cook [21] showed that every problem in NP is reducible to the satisfiability problem (a decision problem from Boolean logic). This implies that the satisfiability problem is the “hardest" problem in NP, and it is termed NP-complete in order to distinguish it from “easier” problems. If the satisfiability problem is solvable in polynomial time, so is every other problem in NP (hence, P=NP). On the other hand, if any problem in NP is truly unable to be solved in polynomial time, the satisfiability problem can only be solved in exponential time and P≠NP.
Formal Property Verification
Published in Louis Scheffer, Luciano Lavagno, Grant Martin, EDA for IC System Design, Verification, and Testing, 2018
The Boolean satisfiability problem (SAT) is to determine whether there exists a truth assignment that makes a given Boolean formula true (or equivalently, whether there exists an input pattern that makes the output of a given Boolean circuit one). The first algorithm to solve this classic NP-complete problem was described in 1960 [76], and since then many improvements have been made. The success of recent SAT solvers such as Chaff [39] and Grasp [40] in solving very large problem instances prompted interest in using SAT solvers for model checking. In 1999, the notion of bounded model checking (BMC) using a SAT solver was introduced [41]. As in SMC, the transitions of the system and property automata are characterized by Boolean formulas. By unfolding this representation (i.e., making k consecutive copies, corresponding to consecutive time frames) the question of existence of a counter-example of k steps can be posed as a SAT problem. This made it possible to exploit recent advances in SAT solvers to find counterexamples to properties for systems much larger than can be handled by SMC (typically up to a few thousand registers).
An Efficient Obstacle-Avoiding Rectilinear Steiner Tree Construction Method Using PB-SAT
Published in IETE Journal of Research, 2023
Sudeshna Kundu, Suchismita Roy, Shyamapada Mukherjee
This article proposes a SAT (Satisfiability) based technique to obtain rectilinear Steiner minimum trees in the existence of obstacles. The last few decades have experienced a significant development in the field of Boolean Satisfiability (SAT) representations for determining different problems in Electronic Design Automation (EDA). The application areas generally include FPGA routing [24, 25], global routing [26, 27] and formal verification [28, 29] etc. Recently, the SAT solvers play an important role in handling Pseudo-Boolean (PB) constraints [30]. PB constraints are more compact and expressive and can substitute a large number of conjunctive normal form (CNF) constraints [31]. One more advantage of PB constraints is the capability to state the optimization problems which are conventionally defined as a problem of integer linear programming (ILP). Therefore, PB-SAT solvers are able to solve both optimization and decision-based problems.
A note on the complexity of S4.2
Published in Journal of Applied Non-Classical Logics, 2021
Aggeliki Chalki, Costas D. Koutras, Yorgos Zikos
The problem of determining if a given formula ϕ is satisfiable in a given logic is called the satisfiability problem for the logic , denoted -SAT. Since a formula ϕ is valid iff is not satisfiable, the problem of determining validity is a closely related problem. In this paper we examine the inherent difficulty of determining whether a formula in is satisfiable. The complexity of this problem is determined by quantifying the amount of time and/or space needed to solve it. The inputs we consider are formulae, and hence we are interested in the difficulty of determining whether a formula ϕ is satisfiable as a function of , which denotes the length of ϕ viewed as a string of symbols. The satisfiability problem can be thought as a set membership problem: the problem of determining whether a formula belongs to the set of formulae satisfiable with respect to some class of frames.
An extensible circuit-based SAT solver
Published in Journal of Experimental & Theoretical Artificial Intelligence, 2020
A propositional theory in Conjunctive Normal Form (CNF) over a set of variables is a conjunction of disjunctions of literals, where a literal is either an instance of a variable or its negation. The task in Satisfiability (SAT) is to determine whether a complete assignment to the variables of the theory exists such that all clauses (disjunctions) are satisfied (at least one of the literals of each clause is ). When a literal in a clause is set to it is removed from the clause reducing the clause size. A clause becomes unit under a partial assignment to variables if the clause is left with only one literal, which must be set to as a necessary condition for satisfiability, a phenomenon known as unit propagation. The clause which forces a literal assignment after becoming unit is called antecedent clause of the assigned literal.