Search results for "CNF"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
120	Stefan Szeider	Generalizations of matched CNF formulas.	Ann. Math. Artif. Intell.	2005	DBLP DOI BibTeX RDF	matched formula, deficiency, biclique cover, P 2 -completeness, NP-completeness, bipartite graph, polynomial hierarchy, SAT problem
100	Eugene Goldberg	Testing satisfiability of CNF formulas by computing a stable set of points.	Ann. Math. Artif. Intell.	2005	DBLP DOI BibTeX RDF	stable set of points, symmetric CNF formulas, satisfiability problem
100	Miroslav N. Velev	Efficient translation of boolean formulas to CNF in formal verification of microprocessors.	ASP-DAC	2004	DBLP DOI BibTeX RDF
90	Pascal Koiran, Klaus Meer	On the Expressive Power of CNF Formulas of Bounded Tree- and Clique-Width.	WG	2008	DBLP DOI BibTeX RDF
90	Rafiq Muhammad 0006, Peter J. Stuckey	A Stochastic Non-CNF SAT Solver.	PRICAI	2006	DBLP DOI BibTeX RDF
90	Zhaohui Fu, Yinlei Yu, Sharad Malik	Considering Circuit Observability Don't Cares in CNF Satisfiability.	DATE	2005	DBLP DOI BibTeX RDF
90	Miroslav N. Velev	Exploiting Signal Unobservability for Efficient Translation to CNF in Formal Verification of Microprocessors.	DATE	2004	DBLP DOI BibTeX RDF
79	Alexandra Goultiaeva, Vicki Iverson, Fahiem Bacchus	Beyond CNF: A Circuit-Based QBF Solver.	SAT	2009	DBLP DOI BibTeX RDF
79	Panagiotis Manolios, Daron Vroon 0001	Efficient Circuit to CNF Conversion.	SAT	2007	DBLP DOI BibTeX RDF
79	Eugene Goldberg	Testing Satisfiability of CNF Formulas by Computing a Stable Set of Points.	CADE	2002	DBLP DOI BibTeX RDF
72	Ramamohan Paturi, Pavel Pudlák, Michael E. Saks, Francis Zane	An improved exponential-time algorithm for k-SAT.	J. ACM	2005	DBLP DOI BibTeX RDF	CNF satisfiability, randomized algorithms
72	Tianyan Deng, Daoyun Xu	Hardness of Approximation Algorithms on k-SAT and (k, s)-SAT Problems.	ICYCS	2008	DBLP DOI BibTeX RDF
72	Miroslav N. Velev	Comparison of schemes for encoding unobservability in translation to SAT.	ASP-DAC	2005	DBLP DOI BibTeX RDF
69	Yinlei Yu, Cameron Brien, Sharad Malik	Exploiting Circuit Reconvergence through Static Learning in CNF SAT Solvers.	VLSI Design	2008	DBLP DOI BibTeX RDF
62	Tianyan Deng, Daoyun Xu	NP-Completeness of (k-SAT, r-UNk-SAT) and (LSAT>=k, r-UNLSAT>=k).	FAW	2008	DBLP DOI BibTeX RDF	PCP theorem, linear CNF formula, LSAT, minimal unsatisfiable(MU) formula, NP-completeness, reduction
61	Dominik Scheder, Philipp Zumstein	How Many Conflicts Does It Need to Be Unsatisfiable?	SAT	2008	DBLP DOI BibTeX RDF	unsatisfiable formulas, Lovász Local Lemma, satisfiability, conflict graph
61	Zhaohui Fu, Sharad Malik	Extracting Logic Circuit Structure from Conjunctive Normal Form Descriptions.	VLSI Design	2007	DBLP DOI BibTeX RDF
61	Ashish Sabharwal, Carlos Ansótegui, Carla P. Gomes, Justin W. Hart, Bart Selman	QBF Modeling: Exploiting Player Symmetry for Simplicity and Efficiency.	SAT	2006	DBLP DOI BibTeX RDF
61	Christian Thiffault, Fahiem Bacchus, Toby Walsh	Solving Non-clausal Formulas with DPLL Search.	CP	2004	DBLP DOI BibTeX RDF
61	Enrico Giunchiglia, Roberto Sebastiani	Applying the Davis-Putnam Procedure to Non-clausal Formulas.	AI*IA	1999	DBLP DOI BibTeX RDF
59	Stefan Porschen, Ewald Speckenmeyer, Bert Randerath	On Linear CNF Formulas.	SAT	2006	DBLP DOI BibTeX RDF	linear CNF formula, edge colouring, linear hypergraph, NP-completeness, satisfiability, latin square
59	Malay K. Ganai, Pranav Ashar, Aarti Gupta, Lintao Zhang, Sharad Malik	Combining strengths of circuit-based and CNF-based algorithms for a high-performance SAT solver.	DAC	2002	DBLP DOI BibTeX RDF	boolean constraint propagation (BCP), bounded model checking (BMC), conjunctive normal form (CNF), boolean satisfiability (SAT)
59	Felip Manyà, Ramón Béjar, Gonzalo Escalada-Imaz	The satisfiability problem in regular CNF-formulas.	Soft Comput.	1998	DBLP DOI BibTeX RDF	Multiple-valued regular CNF-formulas, benchmarks, threshold, satisfiability problem
59	Lintao Zhang	On Subsumption Removal and On-the-Fly CNF Simplification.	SAT	2005	DBLP DOI BibTeX RDF
52	Fadi A. Aloul, Igor L. Markov, Karem A. Sakallah	Shatter: efficient symmetry-breaking for boolean satisfiability.	DAC	2003	DBLP DOI BibTeX RDF	clause learning, logic simplification, routing, symmetries, SAT, CNF, backtrack search, graph automorphism
51	Fadi A. Aloul, Arathi Ramani, Karem A. Sakallah, Igor L. Markov	Solution and Optimization of Systems of Pseudo-Boolean Constraints.	IEEE Trans. Computers	2007	DBLP DOI BibTeX RDF	Pseudo Boolean (PB), Max-ONE, Global Routing, Conjunctive Normal Form (CNF), Backtrack Search, Integer Linear Programming (ILP), Max-SAT, Boolean Satisfiability (SAT)
51	Fadi A. Aloul, Karem A. Sakallah, Igor L. Markov	Efficient Symmetry Breaking for Boolean Satisfiability.	IEEE Trans. Computers	2006	DBLP DOI BibTeX RDF	clause learning, satisfiability (SAT), symmetries, conjunctive normal form (CNF), Backtrack Search, graph automorphism
51	Albert Atserias	On sufficient conditions for unsatisfiability of random formulas.	J. ACM	2004	DBLP DOI BibTeX RDF	Random CNF formulas, propositional resolution, satisfiability, datalog, phase transitions, pebble games
51	Niklas Eén, Alan Mishchenko, Niklas Sörensson	Applying Logic Synthesis for Speeding Up SAT.	SAT	2007	DBLP DOI BibTeX RDF
51	Dimitris Achlioptas, Assaf Naor, Yuval Peres	On the Maximum Satisfiability of Random Formulas.	FOCS	2003	DBLP DOI BibTeX RDF
51	Ryan Williams 0001	Algorithms for quantified Boolean formulas.	SODA	2002	DBLP BibTeX RDF
49	Stefan Porschen, Ewald Speckenmeyer	A CNF Class Generalizing Exact Linear Formulas.	SAT	2008	DBLP DOI BibTeX RDF	CNF satisfiability, exact linear formula, fibre-transversal, hypergraph
49	Daniel Johannsen, Igor Razgon, Magnus Wahlström	Solving SAT for CNF Formulas with a One-Sided Restriction on Variable Occurrences.	SAT	2009	DBLP DOI BibTeX RDF
49	Albert Atserias	Definability on a Random 3-CNF Formula.	LICS	2005	DBLP DOI BibTeX RDF
49	Vijay Durairaj, Priyank Kalla	Guiding CNF-SAT search via efficient constraint partitioning.	ICCAD	2004	DBLP DOI BibTeX RDF
49	Evguenii I. Goldberg, Yakov Novikov	Verification of Proofs of Unsatisfiability for CNF Formulas.	DATE	2003	DBLP DOI BibTeX RDF
49	Bernhard Beckert, Reiner Hähnle, Felip Manyà	The 2-SAT Problem of Regular Signed CNF Formulas.	ISMVL	2000	DBLP DOI BibTeX RDF	signed logic, NP-completeness, SAT, Many-valued logic
41	Clifford R. Johnson	Automating the DNA computer: solving n-Variable 3-SAT problems.	Nat. Comput.	2008	DBLP DOI BibTeX RDF	SAT Computation, DNA Computation, Molecular Computation, Natural Computing
41	Endre Boros, Khaled M. Elbassioni, Kazuhisa Makino	On Berge Multiplication for Monotone Boolean Dualization.	ICALP (1)	2008	DBLP DOI BibTeX RDF
41	Yexin Zheng, Michael S. Hsiao, Chao Huang	SAT-based equivalence checking of threshold logic designs for nanotechnologies.	ACM Great Lakes Symposium on VLSI	2008	DBLP DOI BibTeX RDF	SAT, nanotechnology, equivalence checking, threshold logic
41	Dimitris Achlioptas, Assaf Naor, Yuval Peres	On the maximum satisfiability of random formulas.	J. ACM	2007	DBLP DOI BibTeX RDF	Maximum satisfiability
41	Louay Bazzi	Polylogarithmic Independence Can Fool DNF Formulas.	FOCS	2007	DBLP DOI BibTeX RDF
41	Fahiem Bacchus	GAC Via Unit Propagation.	CP	2007	DBLP DOI BibTeX RDF
41	Sumathi Gopal, Sanjoy Paul, Dipankar Raychaudhuri	Leveraging MAC-layer information for single-hop wireless transport in the Cache and Forward Architecture of the Future Internet.	COMSWARE	2007	DBLP DOI BibTeX RDF
41	Clifford R. Johnson	Automating the DNA Computer: Solving n-Variable 3-SAT Problems.	DNA	2006	DBLP DOI BibTeX RDF
41	Mark Chavira, Adnan Darwiche	Encoding CNFs to Empower Component Analysis.	SAT	2006	DBLP DOI BibTeX RDF
41	Daijue Tang, Sharad Malik	Solving Quantified Boolean Formulas with Circuit Observability Don't Cares.	SAT	2006	DBLP DOI BibTeX RDF
41	Jinbo Huang, Adnan Darwiche	Using DPLL for Efficient OBDD Construction.	SAT (Selected Papers	2004	DBLP DOI BibTeX RDF
41	Miroslav N. Velev	Comparative Study of Strategies for Formal Verification of High-Level Processors.	ICCD	2004	DBLP DOI BibTeX RDF
40	Pei Hu, Guiming Luo, Chongyuan Yin	Computation of Satisfiability Degree Based on CNF.	FSKD (6)	2009	DBLP DOI BibTeX RDF	satisfiability degree computation, horn abduction, CNF
39	Amin Coja-Oghlan, Uriel Feige, Alan M. Frieze, Michael Krivelevich, Dan Vilenchik	On smoothed k-CNF formulas and the Walksat algorithm.	SODA	2009	DBLP DOI BibTeX RDF
39	Marijn Heule, Hans van Maaren	Aligning CNF- and Equivalence-Reasoning.	SAT (Selected Papers	2004	DBLP DOI BibTeX RDF
39	Michael Alekhnovich, Eli Ben-Sasson	Linear Upper Bounds for Random Walk on Small Density Random 3-CNF.	FOCS	2003	DBLP DOI BibTeX RDF
39	Peter Bro Miltersen, Jaikumar Radhakrishnan, Ingo Wegener	On Converting CNF to DNF.	MFCS	2003	DBLP DOI BibTeX RDF
39	Michael Langberg, Amir Pnueli, Yoav Rodeh	The ROBDD Size of Simple CNF Formulas.	CHARME	2003	DBLP DOI BibTeX RDF
39	Olivier Bailleux, Yacine Boufkhad	Efficient CNF Encoding of Boolean Cardinality Constraints.	CP	2003	DBLP DOI BibTeX RDF
39	Alfredo Cruz	PLAtestGA: A CNF-Satisfiability Problem for the Generation of Test Vectors for Missing Faults in VLSI Circuits.	ISMIS	2000	DBLP DOI BibTeX RDF
39	Ramón Béjar, Felip Manyà	A Comparison of Systematic and Local Search Algorithms for Regular CNF Formulas.	ESCQARU	1999	DBLP DOI BibTeX RDF
36	Thomas Delacroix	Choisir un encodage CNF de contraintes de cardinalité performant pour SAT(Choosing an efficient CNF encoding of cardinality constraints for SAT).	CNIA+RJCIA	2018	DBLP BibTeX RDF
36	Martin Lange, Hans Leiß	To CNF or not to CNF? An Efficient Yet Presentable Version of the CYK Algorithm.	Informatica Didact.	2009	DBLP BibTeX RDF
36	Carlos Ansótegui, Felip Manyà	Mapping Many-Valued CNF Formulas to Boolean CNF Formulas.	ISMVL	2005	DBLP DOI BibTeX RDF
32	Romanelli Lodron Zuim, José T. de Sousa, Claudionor José Nunes Coelho Jr.	A fast SAT solver algorithm best suited to reconfigurable hardware.	SBCCI	2006	DBLP DOI BibTeX RDF	formal verification, SAT, CNF, DPLL
31	Yoonna Oh, Maher N. Mneimneh, Zaher S. Andraus, Karem A. Sakallah, Igor L. Markov	AMUSE: a minimally-unsatisfiable subformula extractor.	DAC	2004	DBLP DOI BibTeX RDF	minimally-unsatisfiable subformula (MUS), diagnosis, conjunctive normal form (CNF), boolean satisfiability (SAT)
31	Ramón Béjar, Felip Manyà	Phase Transitions in the Regular Random 3-SAT Problem.	ISMIS	1999	DBLP DOI BibTeX RDF	regular CNF formulas, benchmarks, satisfiability, threshold, Multiple-valued logics, phase transitions
31	Paul Beame, Trinh Huynh, Toniann Pitassi	Hardness amplification in proof complexity.	STOC	2010	DBLP DOI BibTeX RDF	communication complexity, proof complexity
31	Heidi Gebauer	Disproof of the Neighborhood Conjecture with Implications to SAT.	ESA	2009	DBLP DOI BibTeX RDF
31	Marta Arias, José L. Balcázar	Canonical Horn Representations and Query Learning.	ALT	2009	DBLP DOI BibTeX RDF
31	Stefan Porschen, Tatjana Schmidt, Ewald Speckenmeyer	On Some Aspects of Mixed Horn Formulas.	SAT	2009	DBLP DOI BibTeX RDF	Mixed Horn formula, polynomial time reduction, NP-completeness, satisfiability, exact algorithm
31	Khaled M. Elbassioni, Kazuhisa Makino, Imran Rauf	On the Readability of Monotone Boolean Formulae.	COCOON	2009	DBLP DOI BibTeX RDF
31	Himanshu Jain, Edmund M. Clarke	Efficient SAT solving for non-clausal formulas using DPLL, graphs, and watched cuts.	DAC	2009	DBLP DOI BibTeX RDF	NNF, verification, Boolean satisfiability, DPLL
31	Igor Razgon, Barry O'Sullivan	Almost 2-SAT Is Fixed-Parameter Tractable (Extended Abstract).	ICALP (1)	2008	DBLP DOI BibTeX RDF
31	Daniel Lopez-Escogido, Jose Torres-Jimenez, Eduardo Rodriguez-Tello, Nelson Rangel-Valdez	Strength Two Covering Arrays Construction Using a SAT Representation.	MICAI	2008	DBLP DOI BibTeX RDF
31	Florian Lonsing, Armin Biere	Nenofex: Expanding NNF for QBF Solving.	SAT	2008	DBLP DOI BibTeX RDF
31	Ian Davidson, S. S. Ravi	The complexity of non-hierarchical clustering with instance and cluster level constraints.	Data Min. Knowl. Discov.	2007	DBLP DOI BibTeX RDF	Non-hierarchical clustering, Complexity, Constraints
31	Fadi A. Zaraket, Adnan Aziz, Sarfraz Khurshid	Sequential Circuits for Relational Analysis.	ICSE	2007	DBLP DOI BibTeX RDF
31	Masaki Yamamoto 0001	Generating Instances for MAX2SAT with Optimal Solutions.	Theory Comput. Syst.	2006	DBLP DOI BibTeX RDF
31	Evgeny Dantsin, Alexander Wolpert	MAX-SAT for Formulas with Constant Clause Density Can Be Solved Faster Than in O(s2) Time.	SAT	2006	DBLP DOI BibTeX RDF
31	Jan Johannsen	The Complexity of Pure Literal Elimination.	J. Autom. Reason.	2005	DBLP DOI BibTeX RDF	pure literal, computational complexity, completeness
31	Michael Alekhnovich	Lower bounds for k-DNF resolution on random 3-CNFs.	STOC	2005	DBLP DOI BibTeX RDF	random 3CNF, res(k), resolution
31	Stefan Porschen, Ewald Speckenmeyer	Worst Case Bounds for Some NP-Complete Modified Horn-SAT Problems.	SAT (Selected Papers	2004	DBLP DOI BibTeX RDF	(hidden) Horn formula, quadratic formula, minimal vertex cover, NP-completeness, satisfiability, fixed-parameter tractability
31	Michael R. Fellows, Stefan Szeider, Graham Wrightson	On Finding Short Resolution Refutations and Small Unsatisfiable Subsets.	IWPEC	2004	DBLP DOI BibTeX RDF
31	Zbigniew Lonc, Miroslaw Truszczynski	Computing Minimal Models, Stable Models, and Answer Sets.	ICLP	2003	DBLP DOI BibTeX RDF
31	Thomas Eiter, Kazuhisa Makino	Generating All Abductive Explanations for Queries on Propositional Horn Theories.	CSL	2003	DBLP DOI BibTeX RDF	Horn theories, polynomial total time computation, NP-hardness, abduction, propositional logic, Computational logic
31	Aarti Gupta, Zijiang Yang 0006, Pranav Ashar, Anubhav Gupta 0001	SAT-Based Image Computation with Application in Reachability Analysis.	FMCAD	2000	DBLP DOI BibTeX RDF
31	Ramón Béjar, Felip Manyà	Solving Combinatorial Problems with Regular Local Search Algorithms.	LPAR	1999	DBLP DOI BibTeX RDF
31	Ken Satoh	Analysis of Case-Based Representability of Boolean Functions by Monotone Theory.	ALT	1998	DBLP DOI BibTeX RDF
31	Jun Gu, Qian-Ping Gu	Average Time Complexity of the SAT 1.2 Algorithm.	ISAAC	1994	DBLP DOI BibTeX RDF
28	Olivier Bailleux, Yacine Boufkhad, Olivier Roussel	New Encodings of Pseudo-Boolean Constraints into CNF.	SAT	2009	DBLP DOI BibTeX RDF	Pseudo-Boolean, SAT translation
28	Stéphane Lescuyer, Sylvain Conchon	Improving Coq Propositional Reasoning Using a Lazy CNF Conversion Scheme.	FroCoS	2009	DBLP DOI BibTeX RDF
28	Gilles Audemard, Lakhdar Sais	Circuit Based Encoding of CNF Formula.	SAT	2007	DBLP DOI BibTeX RDF
28	Christopher Condrat, Priyank Kalla	A Gröbner Basis Approach to CNF-Formulae Preprocessing.	TACAS	2007	DBLP DOI BibTeX RDF
28	HyoJung Han, Fabio Somenzi	Alembic: An Efficient Algorithm for CNF Preprocessing.	DAC	2007	DBLP DOI BibTeX RDF
28	Stefan Porschen	A CNF Formula Hierarchy over the Hypercube.	Australian Conference on Artificial Intelligence	2007	DBLP DOI BibTeX RDF	hypercube formula, variable closure, satisfiability, hypergraph, transversal
28	Khaled M. Elbassioni	On the Complexity of the Multiplication Method for Monotone CNF/DNF Dualization.	ESA	2006	DBLP DOI BibTeX RDF
28	Hans van Maaren, Linda van Norden	Correlations between Horn fractions, satisfiability and solver performance for fixed density random 3-CNF instances.	Ann. Math. Artif. Intell.	2005	DBLP DOI BibTeX RDF	Horn, satisfiability, density, 3-SAT
28	Roman Gershman, Ofer Strichman	Cost-Effective Hyper-Resolution for Preprocessing CNF Formulas.	SAT	2005	DBLP DOI BibTeX RDF
28	Carsten Sinz	Towards an Optimal CNF Encoding of Boolean Cardinality Constraints.	CP	2005	DBLP DOI BibTeX RDF
28	Carlos Ansótegui, Ramón Béjar, Alba Cabiscol, Felip Manyà	The Interface between P and NP in Signed CNF Formulas.	ISMVL	2004	DBLP DOI BibTeX RDF
28	Paul T. Darga, Mark H. Liffiton, Karem A. Sakallah, Igor L. Markov	Exploiting structure in symmetry detection for CNF.	DAC	2004	DBLP DOI BibTeX RDF	abstract algebra, partition refinement, symmetry, backtrack search, graph automorphism, boolean satisfiability (SAT)
28	Richard Ostrowski, Éric Grégoire, Bertrand Mazure, Lakhdar Sais	Recovering and Exploiting Structural Knowledge from CNF Formulas.	CP	2002	DBLP DOI BibTeX RDF	propositional reasoning and search, SAT, Boolean logic