50 papers:
SAT-2015-IserMS #recognition- Recognition of Nested Gates in CNF Formulas (MI, NM, CS), pp. 255–271.
SAT-2015-PhilippS #constraints #encoding #library #named #pseudo- PBLib — A Library for Encoding Pseudo-Boolean Constraints into CNF (TP, PS), pp. 9–16.
SAT-2014-BiereBLM #constraints #detection- Detecting Cardinality Constraints in CNF (AB, DLB, EL, NM), pp. 285–301.
SAT-2014-SaetherTV #satisfiability- Solving MaxSAT and #SAT on Structured CNF Formulas (SHS, JAT, MV), pp. 16–31.
DATE-2013-GoultiaevaSB- Bridging the gap between dual propagation and CNF-based QBF solving (AG, MS, AB), pp. 811–814.
CAV-2013-VizelRN #generative #performance- Efficient Generation of Small Interpolants in CNF (YV, VR, AN), pp. 330–346.
SAT-2013-Stuckey #problem- There Are No CNF Problems (PJS), pp. 19–21.
LICS-2012-MullerT #random- Short Propositional Refutations for Dense Random 3CNF Formulas (SM, IT), pp. 501–510.
SAT-2012-AchlioptasM #algorithm #bound #exponential #random #satisfiability- Exponential Lower Bounds for DPLL Algorithms on Satisfiable Random 3-CNF Formulas (DA, RMM), pp. 327–340.
SAT-2012-Ben-HaimIMM #constraints #encoding- Perfect Hashing and CNF Encodings of Cardinality Constraints (YBH, AI, OM, AM), pp. 397–409.
SAT-2012-Manthey #flexibility- Coprocessor 2.0 — A Flexible CNF Simplifier — (Tool Presentation) (NM), pp. 436–441.
SAT-2011-Aavani #constraints #pseudo- Translating Pseudo-Boolean Constraints into CNF (AA), pp. 357–359.
SAT-2011-HeuleJB #graph #performance- Efficient CNF Simplification Based on Binary Implication Graphs (MH, MJ, AB), pp. 201–215.
SAT-2011-OrdyniakPS #satisfiability- Satisfiability of Acyclic and almost Acyclic CNF Formulas (II) (SO, DP, SS), pp. 47–60.
SAT-2010-BubeckB #quantifier- Rewriting (Dependency-)Quantified 2-CNF with Arbitrary Free Literals into Existential 2-HORN (UB, HKB), pp. 58–70.
SAT-2010-MakinoTY #algorithm #problem- An Exact Algorithm for the Boolean Connectivity Problem for k-CNF (KM, ST, MY), pp. 172–180.
DATE-2009-ChambersMV #generative #performance #satisfiability- Faster SAT solving with better CNF generation (BC, PM, DV), pp. 1590–1595.
SAT-2009-BailleuxBR #constraints #encoding #pseudo- New Encodings of Pseudo-Boolean Constraints into CNF (OB, YB, OR), pp. 181–194.
SAT-2009-GoultiaevaIB- Beyond CNF: A Circuit-Based QBF Solver (AG, VI, FB), pp. 412–426.
SAT-2009-JohannsenRW #satisfiability #strict- Solving SAT for CNF Formulas with a One-Sided Restriction on Variable Occurrences (DJ, IR, MW), pp. 80–85.
SAT-2008-PorschenS #linear- A CNF Class Generalizing Exact Linear Formulas (SP, ES), pp. 231–245.
DAC-2007-HanS #algorithm #named #performance #preprocessor- Alembic: An Efficient Algorithm for CNF Preprocessing (HH, FS), pp. 582–587.
TACAS-2007-CondratK #approach #preprocessor- A Gröbner Basis Approach to CNF-Formulae Preprocessing (CC, PK), pp. 618–631.
SAT-2007-AudemardS #encoding- Circuit Based Encoding of CNF Formula (GA, LS), pp. 16–21.
SAT-2007-Buresh-OppenheimM #polynomial- Minimum 2CNF Resolution Refutations in Polynomial Time (JBO, DGM), pp. 300–313.
SAT-2007-ManoliosV #performance- Efficient Circuit to CNF Conversion (PM, DV), pp. 4–9.
SAT-2006-PorschenSR #linear #on the- On Linear CNF Formulas (SP, ES, BR), pp. 212–225.
DATE-2005-FuYM #satisfiability- Considering Circuit Observability Don’t Cares in CNF Satisfiability (ZF, YY, SM), pp. 1108–1113.
STOC-2005-AgarwalCMM #algorithm #approximate #problem- O(sqrt(log n)) approximation algorithms for min UnCut, min 2CNF deletion, and directed cut problems (AA, MC, KM, YM), pp. 573–581.
SAT-J-2004-HeuleM05- Aligning CNF- and Equivalence-Reasoning (MH, HvM), pp. 145–156.
LICS-2005-Atserias05a #random- Definability on a Random 3-CNF Formula (AA), pp. 458–466.
SAT-2005-GershmanS #effectiveness #preprocessor- Cost-Effective Hyper-Resolution for Preprocessing CNF Formulas (RG, OS), pp. 423–429.
SAT-2005-Zhang #on the #on the fly- On Subsumption Removal and On-the-Fly CNF Simplification (LZ), pp. 482–489.
DAC-2004-DargaLSM #detection #symmetry- Exploiting structure in symmetry detection for CNF (PTD, MHL, KAS, ILM), pp. 530–534.
DATE-v1-2004-Velev #performance #verification- Exploiting Signal Unobservability for Efficient Translation to CNF in Formal Verification of Microprocessors (MNV), pp. 266–271.
ICALP-2004-FeigeO #random #scalability- Easily Refutable Subformulas of Large Random 3CNF Formulas (UF, EO), pp. 519–530.
SAT-2004-HeuleM- Aligning CNF- and Equivalence-reasoning (MH, HvM), pp. 174–180.
DATE-2003-GoldbergN #proving #satisfiability #verification- Verification of Proofs of Unsatisfiability for CNF Formulas (EIG, YN), pp. 10886–10891.
STOC-2003-Ben-SassonHR- Some 3CNF properties are hard to test (EBS, PH, SR), pp. 345–354.
SAT-2003-Williams #on the- On Computing k-CNF Formula Properties (RW), pp. 330–340.
DAC-2002-GanaiAGZM #algorithm #satisfiability- Combining strengths of circuit-based and CNF-based algorithms for a high-performance SAT solver (MKG, PA, AG, LZ, SM), pp. 747–750.
CADE-2002-Goldberg #satisfiability #testing- Testing Satisfiability of CNF Formulas by Computing a Stable Set of Points (EG), pp. 161–180.
SAT-2002-DavydovaD #optimisation- CNF application in discrete optimization (ID, GD), p. 44.
SAT-2002-Goldberg #satisfiability #testing- Testing satisfiability of CNF formulas by computing a stable set of points (EG), p. 12.
SAT-2002-ManyaABCL- Resolution methods for many-valued CNF formulas (FM, CA, RB, AC, CML), p. 42.
SAT-2002-MatsuuraI- Inclusion-exclusion for k-CNF formulas (AM, KI), p. 3.
SAT-2002-Szeider- Generalizations of matched CNF formulas (SS), p. 7.
STOC-1998-BeameKPS #complexity #on the #proving #random #satisfiability- On the Complexity of Unsatisfiability Proofs for Random k-CNF Formulas (PB, RMK, TP, MES), pp. 561–571.
SAC-1993-VaidyanathanL #analysis #bound #learning- Analysis of Upper Bound in Valiant’s Model for Learning Bounded CNF Expressions (SV, SL), pp. 754–761.
ML-1992-HirschbergP #analysis #concept #learning- Average Case Analysis of Learning κ-CNF Concepts (DSH, MJP), pp. 206–211.