Stem cnf$ (all stems)

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.