No abstract available.
Cited By
- Niemetz A, Preiner M and Biere A (2017). Propagation based local search for bit-precise reasoning, Formal Methods in System Design, 51:3, (608-636), Online publication date: 1-Dec-2017.
- Matsak E Representing Logical Inference Steps with Digital Circuits Proceedings of the Symposium on Human Interface 2009 on Human Interface and the Management of Information. Information and Interaction. Part II: Held as part of HCI International 2009, (178-184)
- Arithmetic Circuits Verification without Looking for Internal Equivalences Proceedings of the Sixth ACM/IEEE International Conference on Formal Methods and Models for Co-Design, (7-16)
- Lai C, Huang C and Khoo K Improving constant-coefficient multiplier verification by partial product identification Proceedings of the conference on Design, automation and test in Europe, (813-818)
- Lonsing F and Biere A Nenofex Proceedings of the 11th international conference on Theory and applications of satisfiability testing, (196-210)
- Nam G, Aloul F, Sakallah K and Rutenbar R (2004). A Comparative Study of Two Boolean Formulations of FPGA Detailed Routing Constraints, IEEE Transactions on Computers, 53:6, (688-696), Online publication date: 1-Jun-2004.
- Kravets V and Sakallah K Resynthesis of multi-level circuits under tight constraints using symbolic optimization Proceedings of the 2002 IEEE/ACM international conference on Computer-aided design, (687-693)
- Espejo J, Entrena L, San Millán E and Oliás E Functional extension of structural logic optimization techniques Proceedings of the 2001 Asia and South Pacific Design Automation Conference, (467-472)
- Zhao Y, Malik S, Moskewicz M and Madigan C Accelerating boolean satisfiability through application specific processing Proceedings of the 14th international symposium on Systems synthesis, (244-249)
- Goldberg E, Prasad M and Brayton R Using SAT for combinational equivalence checking Proceedings of the conference on Design, automation and test in Europe, (114-121)
- Espejo J, Entrena L, San Millán E and Olias E Generalized reasoning scheme for redundancy addition and removal logic optimization Proceedings of the conference on Design, automation and test in Europe, (391-397)
- Kunz W, Marques-Silva J and Malik S SAT and ATPG Logic Synthesis and Verification, (309-341)
- Stoffel D and Kunz W Verification of integer multipliers on the arithmetic bit level Proceedings of the 2001 IEEE/ACM international conference on Computer-aided design, (183-189)
- Moskewicz M, Madigan C, Zhao Y, Zhang L and Malik S Chaff Proceedings of the 38th annual Design Automation Conference, (530-535)
- Whittemore J, Kim J and Sakallah K SATIRE Proceedings of the 38th annual Design Automation Conference, (542-545)
- Marques-Silva J and Sakallah K Boolean satisfiability in electronic design automation Proceedings of the 37th Annual Design Automation Conference, (675-680)
- Kravets V and Sakallah K Constructive library-aware synthesis using symmetries Proceedings of the conference on Design, automation and test in Europe, (208-215)
- Marques-Silva J and Glass T Combinational equivalence checking using satisfiability and recursive learning Proceedings of the conference on Design, automation and test in Europe, (33-es)
- Guerra e Silva L, Silveira L and Marques-Silva J Algorithms for solving Boolean satisfiability in combinational circuits Proceedings of the conference on Design, automation and test in Europe, (107-es)
- Bose S, Agrawal P and Agrawal V (1998). Deriving Logic Systems for Path Delay Test Generation, IEEE Transactions on Computers, 47:8, (829-846), Online publication date: 1-Aug-1998.
- Stoffel D and Kunz W Record & play Proceedings of the 1997 IEEE/ACM international conference on Computer-aided design, (394-399)
Recommendations
Clausal Proofs for Pseudo-Boolean Reasoning
Tools and Algorithms for the Construction and Analysis of SystemsAbstractWhen augmented with a Pseudo-Boolean (PB) solver, a Boolean satisfiability (SAT) solver can apply apply powerful reasoning methods to determine when a set of parity or cardinality constraints, extracted from the clauses of the input formula, has ...
Circuit-Width Based Heuristic for Boolean Reasoning
ATS '04: Proceedings of the 13th Asian Test SymposiumBinary decision diagram (BDD) and Boolean satisfiability (SAT) are two common techniques of logic circuit-based Boolean reasoning. Since circuit-width is a good measure of circuit complexity, in this paper, a circuit-width based heuristic for Boolean ...
A satisfiability procedure for quantified boolean formulae
The renesse issue on satisfiabilityWe present a satisfiability tester QSAT for quantified Boolean formulae and a restriction QSATCNF of QSAT to unquantified conjunctive normal form formulae. QSAT makes use of procedures which replace subformulae of a formula by equivalent formulae. By a ...