Search results for "CNF"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
28	Kazuo Iwama, Daisuke Kawai, Shuichi Miyazaki, Yasuo Okabe, Jun Umemoto	Parallelizing Local Search for CNF Satisfiability Using Vectorization and PVM.	WAE	2000	DBLP DOI BibTeX RDF
28	Ewald Speckenmeyer	Classes of CNF-Formulas with Backtracking Trees of Exponential or Linear Average Order for Exact-Satisfiability.	MFCS	1988	DBLP DOI BibTeX RDF
22	Evangelos Triantaphyllou, Jennifer Austin-Rodriguez	Optimization in Boolean Classification Problems.	Encyclopedia of Optimization	2009	DBLP DOI BibTeX RDF	Inductive inference problem, Boolean classification problem, Minimum number of clauses, One clause at a time approach, OCAT, GRASP approach, Randomized heuristics, Missing information, Unclassifiable examples, SAT, Learning algorithm, Medical diagnosis, Conjunctive normal form, CNF, Satisfiability problem, Disjunctive normal form, DNF
22	Vetle I. Torvik, Evangelos Triantaphyllou	Inference of Monotone Boolean Functions.	Encyclopedia of Optimization	2009	DBLP DOI BibTeX RDF	Isotone Boolean function, Antitone Boolean function, Boolean function inference problem, Free distributive lattice, Interactive learning of Boolean functions, Shannon function, Hansel theorem, Hansel chain, Sequential Hansel chains question-asking strategy, Binary search-Hansel chains question-asking strategy, Boolean function, Conjunctive normal form, CNF, Binary search, Classification problem, Disjunctive normal form, DNF, Monotone Boolean function
22	Salvador Nieto Sánchez, Evangelos Triantaphyllou	Optimization in Classifying Text Documents.	Encyclopedia of Optimization	2009	DBLP DOI BibTeX RDF	Indexing terms, Context descriptors, Document surrogate, Principle of least effort, PLE, One clause at a time algorithm, OCAT, Indexing vocabulary, Optimal indexing vocabulary, Semantic analysis methodologies, Word patterns, Text classification, Document classification, Computational linguistics, Vector space model, Keywords, Conjunctive normal form, CNF, Disjunctive normal form, DNF, VSM
22	HoonSang Jin, Fabio Somenzi	Prime clauses for fast enumeration of satisfying assignments to boolean circuits.	DAC	2005	DBLP DOI BibTeX RDF	AllSAT, minimal satisfying assignment, SAT, CNF
22	Fadi A. Aloul, Igor L. Markov, Karem A. Sakallah	FORCE: a fast and easy-to-implement variable-ordering heuristic.	ACM Great Lakes Symposium on VLSI	2003	DBLP DOI BibTeX RDF	partitioning, placement, SAT, BDDs, hypergraph, CNF, pre-processing, backtrack search, variable order
22	Fadi A. Aloul, Brian D. Sierawski, Karem A. Sakallah	Satometer: how much have we searched?	DAC	2002	DBLP DOI BibTeX RDF	conflict diagnosis, search progress, search space coverage, SAT, BDDs, CNF, backtrack search, ZBDDs
22	Fadi A. Aloul, Arathi Ramani, Igor L. Markov, Karem A. Sakallah	Solving difficult SAT instances in the presence of symmetry.	DAC	2002	DBLP DOI BibTeX RDF	difficult, faster, search, symmetry, SAT, CNF, speed-up, instances
22	Jun Gu	Global Optimization for Satisfiability (SAT) Problem.	IEEE Trans. Knowl. Data Eng.	1994	DBLP DOI BibTeX RDF	global optimization algorithms, VLSI engineering, DNF local search methods, Universal SAT problem model, UniSAT, discrete SAT problem, Boolean space, unconstrained global optimization problem, real space, direct correspondence, global minimum point, backtracking/resolution procedures, optimisation, inference, inference mechanisms, search problems, automated reasoning, formal logic, CNF, conjunctive normal form, computing theory, satisfiability problem, SAT problem, mathematical logic
22	Nader H. Bshouty	Exact Learning via the Monotone Theory (Extended Abstract)	FOCS	1993	DBLP DOI BibTeX RDF	Monotone theory, decision trees, boolean function, learnability, membership, CNF, equivalence queries, DNF, exact learning, concept classes
21	Thomas Stibor	Foundations of r-contiguous matching in negative selection for anomaly detection.	Nat. Comput.	2009	DBLP DOI BibTeX RDF	k-CNF satisfiability, Anomaly detection, Artificial immune systems, Negative selection
21	Daniele Pretolani	Probability logic and optimization SAT: The PSAT and CPA models.	Ann. Math. Artif. Intell.	2005	DBLP DOI BibTeX RDF	CNF formulas, ideal matrices, probability, logic, directed graphs, propositional satisfiability
21	Eli Ben-Sasson, Prahladh Harsha, Sofya Raskhodnikova	Some 3CNF properties are hard to test.	STOC	2003	DBLP DOI BibTeX RDF	CNF formulas, lower bounds, property testing, sublinear algorithms, locally testable codes
21	Jun Gu, Qian-Ping Gu, Ding-Zhu Du	Convergence Properties of Optimization Algorithms for the SAT Problem.	IEEE Trans. Computers	1996	DBLP DOI BibTeX RDF	satisfiability (SAT) problem, convergence ratio, time complexity, optimization algorithm, nonlinear programming, Conjunctive normal form (CNF)
21	Paul Beame, Toniann Pitassi	Simplified and Improved Resolution Lower Bounds.	FOCS	1996	DBLP DOI BibTeX RDF	resolution lower bounds, randomly generated formulas, random formulas, randomly chosen 3-CNF formula, lower bounds, computability, pigeonhole principle
21	László Lovász 0001, Moni Naor, Ilan Newman, Avi Wigderson	Search Problems in the Decision Tree Model (Preliminary Version)	FOCS	1991	DBLP DOI BibTeX RDF	Boolean decision tree model, CNF search, complexities, randomness, search problems, determinism, nondeterminism
20	Marcus Fontoura, Suhas Sadanandan, Jayavel Shanmugasundaram, Sergei Vassilvitskii, Erik Vee, Srihari Venkatesan, Jason Y. Zien	Efficiently evaluating complex boolean expressions.	SIGMOD Conference	2010	DBLP DOI BibTeX RDF	dewey, interval, boolean expressions, pub/sub
20	Daniel Tille, Rolf Drechsler	A fast untestability proof for SAT-based ATPG.	DDECS	2009	DBLP DOI BibTeX RDF
20	Sama Goliaei, Saeed Jalili	An Optical Wavelength-Based Solution to the 3-SAT Problem.	OSC	2009	DBLP DOI BibTeX RDF	Wavelength-Based Approach, 3-SAT Problem, NP- Complete, Optical Computing, Unconventional Computing
20	Heidi Gebauer, Robin A. Moser, Dominik Scheder, Emo Welzl	The Lovász Local Lemma and Satisfiability.	Efficient Algorithms	2009	DBLP DOI BibTeX RDF
20	Chris Calabro, Ramamohan Paturi	k-SAT Is No Harder Than Decision-Unique-k-SAT.	CSR	2009	DBLP DOI BibTeX RDF	unique satisfiability, independent set, quantified Boolean formulas, hitting set, k-SAT, exponential complexity
20	Nadia Creignou, Hervé Daudé, Uwe Egly, Raphaël Rossignol	(1, 2)-QSAT: A Good Candidate for Understanding Phase Transitions Mechanisms.	SAT	2009	DBLP DOI BibTeX RDF
20	Robin A. Moser	A constructive proof of the Lovász local lemma.	STOC	2009	DBLP DOI BibTeX RDF	bounded occurrence sat instances, hypergraph colouring, derandomization, Lovasz local lemma
20	Cédric Piette, Youssef Hamadi, Lakhdar Sais	Efficient Combination of Decision Procedures for MUS Computation.	FroCoS	2009	DBLP DOI BibTeX RDF
20	Roman Gershman, Maya Koifman, Ofer Strichman	An approach for extracting a small unsatisfiable core.	Formal Methods Syst. Des.	2008	DBLP DOI BibTeX RDF	Unsatisfiable core, SAT, Resolution
20	Nadia Creignou, Heribert Vollmer	Boolean Constraint Satisfaction Problems: When Does Post's Lattice Help?.	Complexity of Constraints	2008	DBLP DOI BibTeX RDF
20	Konstantinos Georgiou, Periklis A. Papakonstantinou	Complexity and Algorithms for Well-Structured k-SAT Instances.	SAT	2008	DBLP DOI BibTeX RDF
20	Xiuqin Wang, Guangsheng Ma, Hao Wang	A Novel Method for All Solutions SAT Problem.	SNPD	2008	DBLP DOI BibTeX RDF	All Solutions, Observability Don't Cares, Circuit Structure, Boolean Satisfiability
20	Cédric Piette	Let the Solver Deal with Redundancy.	ICTAI (1)	2008	DBLP DOI BibTeX RDF
20	Arthur Choi, Noah Zaitlen, Buhm Han, Knot Pipatsrisawat, Adnan Darwiche, Eleazar Eskin	Efficient Genome Wide Tagging by Reduction to SAT.	WABI	2008	DBLP DOI BibTeX RDF
20	Thomas Eiter, Kazuhisa Makino	On computing all abductive explanations from a propositional Horn theory.	J. ACM	2007	DBLP DOI BibTeX RDF	Horn theories, dualization problem, polynomial total-time computation, NP-hardness, Abduction, model-based reasoning, propositional logic, tractability, prime implicates, characteristic set, enumeration algorithms
20	Lengning Liu, Miroslaw Truszczynski	Satisfiability Testing of Boolean Combinations of Pseudo-Boolean Constraints using Local-search Techniques.	Constraints An Int. J.	2007	DBLP DOI BibTeX RDF	Pseudo-Boolean constraints, Boolean satisfiability, Stochastic local search
20	Youshen Xia, Mohamed S. Kamel	Novel Cooperative Neural Fusion Algorithms for Image Restoration and Image Fusion.	IEEE Trans. Image Process.	2007	DBLP DOI BibTeX RDF
20	Thomas Stibor	Phase Transition and the Computational Complexity of Generating r -Contiguous Detectors.	ICARIS	2007	DBLP DOI BibTeX RDF
20	Chi-An Wu, Ting-Hao Lin, Chih-Chun Lee, Chung-Yang Huang	QuteSAT: a robust circuit-based SAT solver for complex circuit structure.	DATE	2007	DBLP DOI BibTeX RDF
20	Qingshun Zhang, Daoyun Xu	The Existence of Unsatisfiable Formulas in k-LCNF for k>=3.	TAMC	2007	DBLP DOI BibTeX RDF
20	Clifford R. Johnson	Modeling Non-specific Binding in Gel-Based DNA Computers.	DNA	2007	DBLP DOI BibTeX RDF
20	Marina Langlois, Robert H. Sloan, György Turán	Horn Upper Bounds and Renaming.	SAT	2007	DBLP DOI BibTeX RDF
20	Miroslav N. Velev	Exploiting hierarchy and structure to efficiently solve graph coloring as SAT.	ICCAD	2007	DBLP DOI BibTeX RDF
20	Shoham Ben-David, Richard J. Trefler, Grant E. Weddell	Bounded Model Checking with Description Logic Reasoning.	TABLEAUX	2007	DBLP DOI BibTeX RDF
20	Sachoun Park, Gihwon Kwon	SAT based Verification Tool for Labeled Transition System.	SERA	2007	DBLP DOI BibTeX RDF	Formal Verification, Labeled Transition System, Bounded Model checking, Linear Temporal Logic
20	Roman Gershman, Maya Koifman, Ofer Strichman	Deriving Small Unsatisfiable Cores with Dominators.	CAV	2006	DBLP DOI BibTeX RDF
20	Allen Van Gelder	Preliminary Report on Input Cover Number as a Metric for Propositional Resolution Proofs.	SAT	2006	DBLP DOI BibTeX RDF
20	Joshua Buresh-Oppenheim, David G. Mitchell	Minimum Witnesses for Unsatisfiable 2CNFs.	SAT	2006	DBLP DOI BibTeX RDF
20	Josep Argelich, Xavier Domingo, Chu Min Li, Felip Manyà, Jordi Planes	Towards Solving Many-Valued MaxSAT.	ISMVL	2006	DBLP DOI BibTeX RDF
20	Lionel Paris, Richard Ostrowski, Pierre Siegel, Lakhdar Sais	Computing Horn Strong Backdoor Sets Thanks to Local Search.	ICTAI	2006	DBLP DOI BibTeX RDF
20	Jakob Nordström	Narrow proofs may be spacious: separating space and width in resolution.	STOC	2006	DBLP DOI BibTeX RDF	pebbling contradiction, lower bound, resolution, space, separation, proof complexity, width, pebble game
20	Olgierd Unold	Playing a Toy-Grammar with GCS.	IWINAC (2)	2005	DBLP DOI BibTeX RDF
20	Andrea Ferrara, Guoqiang Pan, Moshe Y. Vardi	Treewidth in Verification: Local vs. Global.	LPAR	2005	DBLP DOI BibTeX RDF
20	Jinbo Huang	MUP: a minimal unsatisfiability prover.	ASP-DAC	2005	DBLP DOI BibTeX RDF
20	Panagiotis Manolios, Sudarshan K. Srinivasan	A Parameterized Benchmark Suite of Hard Pipelined-Machine-Verification Problems.	CHARME	2005	DBLP DOI BibTeX RDF
20	Josep Argelich, Felip Manyà	Solving Over-Constrained Problems with SAT.	CP	2005	DBLP DOI BibTeX RDF
20	Steven Perron	A Propositional Proof System for Log Space.	CSL	2005	DBLP DOI BibTeX RDF
20	HoonSang Jin, Mohammad Awedh, Fabio Somenzi	CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking.	CAV	2004	DBLP DOI BibTeX RDF
20	Daniel Král	Locally satisfiable formulas.	SODA	2004	DBLP BibTeX RDF
20	HoonSang Jin, Fabio Somenzi	CirCUs: A Hybrid Satisfiability Solver.	SAT (Selected Papers	2004	DBLP DOI BibTeX RDF
20	Kavita Ravi, Fabio Somenzi	Minimal Assignments for Bounded Model Checking.	TACAS	2004	DBLP DOI BibTeX RDF
20	Jinbo Huang, Adnan Darwiche	Toward Good Elimination Orders for Symbolic SAT Solving.	ICTAI	2004	DBLP DOI BibTeX RDF
20	Luca Trevisan	A Note on Approximate Counting for k-DNF.	APPROX-RANDOM	2004	DBLP DOI BibTeX RDF
20	Rajat Arora, Michael S. Hsiao	Enhancing SAT-based Bounded Model Checking using Sequential Logic Implications.	VLSI Design	2004	DBLP DOI BibTeX RDF
20	Martin Fränzle, Christian Herde	Efficient SAT Engines for Concise Logics: Accelerating Proof Search for Zero-One Linear Constraint Systems.	LPAR	2003	DBLP DOI BibTeX RDF	non-clausal propositional logic, zero-one linear constraint systems, Satisfiability, proof search, acceleration techniques
20	K. Subramani 0001	On Clausal Equivalence and Hull Inclusion.	ICTCS	2003	DBLP DOI BibTeX RDF
20	Stefan Porschen, Bert Randerath, Ewald Speckenmeyer	Linear Time Algorithms for Some Not-All-Equal Satisfiability Problems.	SAT	2003	DBLP DOI BibTeX RDF
20	Carlos Ansótegui, Felip Manyà	New Logical and Complexity Results for Signed-SAT.	ISMVL	2003	DBLP DOI BibTeX RDF
20	Marta Arias, Roni Khardon, Rocco A. Servedio	Polynomial Certificates for Propositional Classes.	COLT	2003	DBLP DOI BibTeX RDF
20	Stefan Szeider	Minimal Unsatisfiable Formulas with Bounded Clause-Variable Difference are Fixed-Parameter Tractable.	COCOON	2003	DBLP DOI BibTeX RDF
20	Chris Calabro, Russell Impagliazzo, Valentine Kabanets, Ramamohan Paturi	The Complexity of Unique k-SAT: An Isolation Lemma for k-CNFs.	CCC	2003	DBLP DOI BibTeX RDF
20	Fadi A. Aloul, Arathi Ramani, Igor L. Markov, Karem A. Sakallah	Generic ILP versus specialized 0-1 ILP: an update.	ICCAD	2002	DBLP DOI BibTeX RDF
20	Stefan Szeider	NP-Completeness of Refutability by Literal-Once Resolution.	IJCAR	2001	DBLP DOI BibTeX RDF
20	Lefteris M. Kirousis, Phokion G. Kolaitis	The Complexity of Minimal Satisfiability Problems.	STACS	2001	DBLP DOI BibTeX RDF
20	Eli Ben-Sasson, Nicola Galesi	Space Complexity of Random Formulae in Resolution.	CCC	2001	DBLP DOI BibTeX RDF
20	Juan Luis Esteban, Jacobo Torán	Space Bounds for Resolution.	STACS	1999	DBLP DOI BibTeX RDF
20	Ramamohan Paturi, Pavel Pudlák, Francis Zane	Satisfiability Coding Lemma.	FOCS	1997	DBLP DOI BibTeX RDF	satisfying assignments, satisfying assignment, Satisfiability Coding Lemma, computability, randomized algorithm, satisfiability, deterministic algorithm, conjunctive normal form, Boolean formulae
20	Kazuo Iwama	Complexity of Finding Short Resolution Proofs.	MFCS	1997	DBLP DOI BibTeX RDF
20	Jae-Young Chang, Sang-goo Lee	An optimization of disjunctive queries: union-pushdown.	COMPSAC	1997	DBLP DOI BibTeX RDF	disjunctive query optimization, disjunctive predicates, plan generation, union-pushdown, performance analysis, query processing, query optimizers
20	Tai Joon Park, Allen Van Gelder	Partitioning Methods for Satisfiability Testing on Large Formulas.	CADE	1996	DBLP DOI BibTeX RDF
20	Nader H. Bshouty, Richard Cleve, Sampath Kannan, Christino Tamon	Oracles and Queries that are Sufficient for Exact Learning (Extended Abstract).	COLT	1994	DBLP DOI BibTeX RDF
20	Der-Shung Yang, Gunnar Blix, Larry A. Rendell	The Replication Problem: A Constructive Induction Approach.	EWSL	1991	DBLP DOI BibTeX RDF	Empirical learning, constructive induction
20	Andreas Flögel, Marek Karpinski, Hans Kleine Büning	Subclasses of Quantified Boolean Formulas.	CSL	1990	DBLP DOI BibTeX RDF
18	Nadia Creignou, Oscar Defrain, Frédéric Olive, Simon Vilmin	On the enumeration of signatures of XOR-CNF's.	CoRR	2024	DBLP DOI BibTeX RDF
18	Guoxia Nie, Daoyun Xu, Xi Wang, Zaijun Zhang	Exact satisfiability and phase transition analysis of the regular (k, d)-CNF formula.	Frontiers Comput. Sci.	2024	DBLP DOI BibTeX RDF
18	Boubacar Diarra, Karine Guillouard, Meryem Ouzzif, Philippe Merle, Jean-Bernard Stefani	In-Depth Analysis of Kubernetes Manifest Verification Tools for Robust CNF Deployment.	ICIN	2024	DBLP DOI BibTeX RDF
18	Evgeny Dantsin, Alexander Wolpert	An Isomorphism-Invariant Distance Function on Propositional Formulas in CNF.	J. Satisf. Boolean Model. Comput.	2023	DBLP DOI BibTeX RDF
18	Wissal Attaoui, Essaid Sabir, Halima Elbiaze, Mohsen Guizani	VNF and CNF Placement in 5G: Recent Advances and Future Trends.	IEEE Trans. Netw. Serv. Manag.	2023	DBLP DOI BibTeX RDF
18	Dmitry Sokolov 0001	Random (log n)-CNF are Hard for Cutting Planes (Again).	Electron. Colloquium Comput. Complex.	2023	DBLP BibTeX RDF
18	Gabriele Masina, Giuseppe Spallitta, Roberto Sebastiani	On CNF Conversion for SAT Enumeration.	CoRR	2023	DBLP DOI BibTeX RDF
18	Petr Savický	On CNF formulas irredundant with respect to unit clause propagation.	CoRR	2023	DBLP DOI BibTeX RDF
18	Hu Xiaobo, Shengyuan Xu, Tu Yinzi, Xiutao Feng	CNF Characterization of Sets over ℤ2n and Its Applications in Cryptography.	IACR Cryptol. ePrint Arch.	2023	DBLP BibTeX RDF
18	Francisco Miguel García-Olmedo, Jesús García-Miranda, Pedro González-Rodelas	Mathematical Foundation of a Functional Implementation of the CNF Algorithm.	Algorithms	2023	DBLP DOI BibTeX RDF
18	Kun He 0011, Kewen Wu 0001, Kuan Yang	Improved Bounds for Sampling Solutions of Random CNF Formulas.	SODA	2023	DBLP DOI BibTeX RDF
18	Elias Kuiter, Sebastian Krieter, Chico Sundermann, Thomas Thüm, Gunter Saake	Tseitin or not Tseitin? The Impact of CNF Transformations on Feature-Model Analyses.	Software Engineering	2023	DBLP BibTeX RDF
18	Vinicius Ferreira, João Bastos, André Martins, Paulo Araújo, Nicolás F. Lori, João Faria, António Costa 0001, Helena Fernández López	NETEDGE MEP: A CNF-based Multi-access Edge Computing Platform.	ISCC	2023	DBLP DOI BibTeX RDF
18	Gabriele Masina, Giuseppe Spallitta, Roberto Sebastiani	On CNF Conversion for Disjoint SAT Enumeration.	SAT	2023	DBLP DOI BibTeX RDF
18	Guillaume Petiot	Improved Encoding of Possibilistic Networks in CNF Using Quine-McCluskey Algorithm.	ICAART (3)	2023	DBLP DOI BibTeX RDF
18	Sibylle Möhle	An Abstract CNF-to-d-DNNF Compiler Based on Chronological CDCL.	FroCoS	2023	DBLP DOI BibTeX RDF
18	Stephan Gocht, Ruben Martins, Jakob Nordström, Andy Oertel	Certified CNF Translations for Pseudo-Boolean Solving (Extended Abstract).	IJCAI	2023	DBLP DOI BibTeX RDF
18	Samuel Manoharan Jayaseelan, Sakthivel Thirumalai Gopal, Sangeetha Muthu, Sivamani Selvaraju, Md Saad Patel	A Hybrid Fuzzy based Cross Neighbor Filtering (HF-CNF) for Image Enhancement of fine and coarse powder Scanned Electron Microscopy (SEM) images.	J. Intell. Fuzzy Syst.	2022	DBLP DOI BibTeX RDF
18	Vikraman Arvind, Venkatesan Guruswami	CNF Satisfiability in a Subspace and Related Problems.	Algorithmica	2022	DBLP DOI BibTeX RDF
18	Alexander A. Sherstov	The Approximate Degree of DNF and CNF Formulas.	Electron. Colloquium Comput. Complex.	2022	DBLP BibTeX RDF