BibSLEIGH — satisfiability tag

satisfiability

?fullname?SAT?
?longname?SAT (Satisfiability)?
Google

satisfiability

Tag #satisfiability

717 papers:

CSL-2020-Mascle0 #decidability #modelling: The Keys to Decidable HyperLTL Satisfiability: Small Models or Very Simple Formulas (CM, MZ0), p. 16.
IFM-2019-LutebergetCJ #automation #optimisation #using: Automated Drawing of Railway Schematics Using Numerical Optimization in SAT (BL, KC, CJ), pp. 341–359.
IFM-2019-OsamaW #gpu #named: SIGmA: GPU Accelerated Simplification of SAT Formulas (MO, AW), pp. 514–522.
SEFM-2019-AvellanedaP #approach #automaton #learning: Learning Minimal DFA: Taking Inspiration from RPNI to Improve SAT Approach (FA, AP), pp. 243–256.
SEFM-2019-BittnerTS #case study #configuration management #constraints #encoding: SAT Encodings of the At-Most-k Constraint - A Case Study on Configuring University Courses (PMB, TT, IS), pp. 127–144.
ICML-2019-WangDWK #learning #logic #named #reasoning #using: SATNet: Bridging deep learning and logical reasoning using a differentiable satisfiability solver (PWW, PLD, BW, JZK), pp. 6545–6554.
ECOOP-2019-MisonizhnikM #on the #type system: On Satisfiability of Nominal Subtyping with Variance (AM, DM), p. 20.
CAV-2019-LiVR #ltl: Satisfiability Checking for Mission-Time LTL (JL, MYV, KYR), pp. 3–22.
ICST-2019-PlazarAPDC #configuration management #question: Uniform Sampling of SAT Solutions for Configurable Systems: Are We There Yet? (QP, MA, GP, XD, MC), pp. 240–251.
AIIDE-2018-Horswill #embedded #named #runtime: CatSAT: A Practical, Embedded, SAT Language for Runtime PCG (IDH), pp. 38–44.
LOPSTR-2018-Lucas #first-order #proving: Proving Program Properties as First-Order Satisfiability (SL), pp. 3–21.
PADL-2018-KringsLKHH #smt: Three Is a Crowd: SAT, SMT and CLP on a Chessboard (SK, ML, PK, SH, MH), pp. 63–79.
ICSE-2018-DutraLBS #performance #testing: Efficient sampling of SAT solutions for testing (RD, KL, JB, KS), pp. 549–559.
IJCAR-2018-FazekasBB #algorithm #modulo theories #set: Implicit Hitting Set Algorithms for Maximum Satisfiability Modulo Theories (KF, FB, AB), pp. 134–151.
IJCAR-2018-FingerP #logic #probability: Probably Half True: Probabilistic Satisfiability over Łukasiewicz Infinitely-Valued Logic (MF, SP), pp. 194–210.
IJCAR-2018-HuangMGZZ #scalability #testing: Investigating the Existence of Large Sets of Idempotent Quasigroups via Satisfiability Testing (PH0, FM, CG, JZ0, HZ), pp. 354–369.
IJCAR-2018-IgnatievPNM #approach #set: A SAT-Based Approach to Learn Explainable Decision Sets (AI, FP, NN, JMS0), pp. 627–645.
IJCAR-2018-LagniezBLM #approach #problem: An Assumption-Based Approach for Solving the Minimal S5-Satisfiability Problem (JML, DLB, TdL, VM), pp. 1–18.
MoDELS-2017-MaozPRS #component #question #specification #why: Why is My Component and Connector Views Specification Unsatisfiable? (SM, NP, JOR, RS), pp. 134–144.
LOPSTR-2017-GutierrezM #algebra #decidability: Variant-Based Decidable Satisfiability in Initial Algebras with Predicates (RG, JM), pp. 306–322.
FASE-2017-UvaPRAF #automation #java #specification: Automated Workarounds from Java Program Specifications Based on SAT Solving (MU, PP, GR, NA, MFF), pp. 356–373.
CADE-2017-BonacinaGS #modulo theories: Satisfiability Modulo Theories and Assignments (MPB, SGL, NS), pp. 42–59.
CADE-2017-CimattiGIRS #incremental: Satisfiability Modulo Transcendental Functions via Incremental Linearization (AC, AG, AI, MR, RS), pp. 95–113.
CADE-2017-Cruanes #bound: Satisfiability Modulo Bounded Checking (SC), pp. 114–129.
CADE-2017-Lammich #performance: Efficient Verified (UN)SAT Certificate Checking (PL), pp. 237–254.
CADE-2017-XuCW #composition #constraints #logic: Satisfiability of Compositional Separation Logic with Tree Predicates and Data Constraints (ZX, TC, ZW), pp. 509–527.
CAV-2017-SiZGN #analysis: Maximum Satisfiability in Software Analysis: Applications and Techniques (XS, XZ, RG, MN), pp. 68–94.
CAV-2017-FinkbeinerHS #equivalence #named: EAHyper: Satisfiability, Implication, and Equivalence Checking of Hyperproperties (BF, CH, MS), pp. 564–570.
ICTSS-2017-WangTJK #quantifier #sequence: Homing Sequence Derivation with Quantified Boolean Satisfiability (HEW, KHT, JHRJ, NK), pp. 230–242.
IFM-2016-AntoninoGR #analysis #performance #using: Efficient Deadlock-Freedom Checking Using Local Analysis and SAT Solving (PA, TGR, AWR), pp. 345–360.
SEFM-2016-AbrahamK #theory and practice: Satisfiability Checking: Theory and Applications (EÁ, GK), pp. 9–23.
BX-2016-SemerathDHV #co-evolution #logic #modelling #synthesis #using: Change Propagation of View Models by Logic Synthesis using SAT solvers (OS, CD, ÁH0, DV), pp. 40–44.
MoDELS-2016-DaniaC #constraints #first-order #logic #named #ocl: OCL2MSFOL: a mapping to many-sorted first-order logic for efficiently checking the satisfiability of OCL constraints (CD, MC), pp. 65–75.
POPL-2016-ZhangMNN: Query-guided maximum satisfiability (XZ, RM, AVN, MN), pp. 109–122.
QAPL-2016-KlebanovWW #probability: Sound Probabilistic #SAT with Projection (VK, AW, JW), pp. 15–29.
ASE-2016-DegiovanniRACA #detection: Goal-conflict detection based on temporal satisfiability checking (RD, NR, DA, PFC, NA), pp. 507–518.
ASE-2016-YamadaBAKC #combinator #generative #testing #using: Greedy combinatorial test case generation using unsatisfiable cores (AY, AB, CA, TK, EHC), pp. 614–624.
CAV-2016-LeSC #source code: Satisfiability Modulo Heap-Based Programs (QLL, JS0, WNC), pp. 382–404.
CAV-2016-NiemetzPB #modulo theories #precise: Precise and Complete Propagation Based Local Search for Satisfiability Modulo Theories (AN, MP, AB), pp. 199–217.
CAV-2016-FuS #float #named #performance: XSat: A Fast Floating-Point Satisfiability Solver (ZF, ZS), pp. 187–209.
CAV-2016-LeggNR #bound #synthesis: A SAT-Based Counterexample Guided Method for Unbounded Synthesis (AL, NN, LR), pp. 364–382.
CSL-2016-KotekVZ #bound #finite #higher-order #monad: Monadic Second Order Finite Satisfiability and Unbounded Tree-Width (TK, HV, FZ), p. 20.
IJCAR-2016-BlanchetteFW #framework: A Verified SAT Solver Framework with Learn, Forget, Restart, and Incrementality (JCB, MF, CW), pp. 25–44.
IJCAR-2016-ZoharZ #automation #calculus #named: Gen2sat: An Automated Tool for Deciding Derivability in Analytic Pure Sequent Calculi (YZ, AZ), pp. 487–495.
VMCAI-2016-BrainHKM #automation #encoding #generative: Automatic Generation of Propagation Complete SAT Encodings (MB, LH, DK, RM), pp. 536–556.
SPLC-2015-LiangGCR #analysis #feature model #modelling #scalability: SAT-based analysis of large real-world feature models is easy (JH(L, VG, KC, VR), pp. 91–100.
ICSE-v1-2015-Ben-DavidSAB #model checking #product line #requirements #using: Symbolic Model Checking of Product-Line Requirements Using SAT-Based Methods (SBD, BS, JMA, SB), pp. 189–199.
SAC-2015-TodaT #performance: BDD construction for all solutions SAT and efficient caching mechanism (TT, KT), pp. 1880–1886.
PDP-2015-YounessIMO #gpu #implementation #optimisation #performance #problem: An Efficient Implementation of Ant Colony Optimization on GPU for the Satisfiability Problem (HAY, AI, MM, MO), pp. 230–235.
STOC-2015-DingSS #proving #scalability: Proof of the Satisfiability Conjecture for Large k (JD, AS, NS), pp. 59–68.
STOC-2015-FeldmanPV #complexity #on the #problem #random: On the Complexity of Random Satisfiability Problems with Planted Solutions (VF, WP, SV), pp. 77–86.
TACAS-2015-ChakrabortyFMSV #generative #on the #parallel #scalability: On Parallel Scalable Uniform SAT Witness Generation (SC, DJF, KSM, SAS, MYV), pp. 304–319.
CADE-2015-David: Deciding ATL* Satisfiability by Tableaux (AD), pp. 214–228.
CADE-2015-ZulkoskiGC #algebra #named: MathCheck: A Math Assistant via a Combination of Computer Algebra Systems and SAT Solvers (EZ, VG, KC), pp. 607–622.
CAV-2015-BacchusK #set #using: Using Minimal Correction Sets to More Efficiently Compute Minimal Unsatisfiable Sets (FB, GK), pp. 70–86.
ICLP-J-2015-AlvianoP #fuzzy #modulo theories #set: Fuzzy answer set computation via satisfiability modulo theories (MA, RP), pp. 588–603.
ICST-2015-YamadaKACOB #combinator #incremental #optimisation #testing: Optimization of Combinatorial Testing by Incremental SAT Solving (AY, TK, CA, EHC, YO, AB), pp. 1–10.
SAT-2015-BalyoSS #named #parallel: HordeSat: A Massively Parallel Portfolio SAT Solver (TB, PS, CS), pp. 156–172.
SAT-2015-BurchardSB #parallel: Laissez-Faire Caching for Parallel #SAT Solving (JB, TS, BB), pp. 46–61.
SAT-2015-CaiLS #named: CCAnr: A Configuration Checking Based Local Search Solver for Non-random Satisfiability (SC, CL, KS), pp. 1–8.
SAT-2015-ChenS #algorithm: Improved Algorithms for Sparse MAX-SAT and MAX-k-CSP (RC, RS), pp. 33–45.
SAT-2015-DouglassKR #quantum: Constructing SAT Filters with a Quantum Annealer (AD, ADK, JR), pp. 104–120.
SAT-2015-FalknerLH #analysis #automation #named #performance: SpySMAC: Automated Configuration and Performance Analysis of SAT Solvers (SF, MTL, FH), pp. 215–222.
SAT-2015-GanianS #algorithm #community: Community Structure Inspired Algorithms for SAT and #SAT (RG, SS), pp. 223–237.
SAT-2015-IgnatievPM: SAT-Based Formula Simplification (AI, AP, JMS), pp. 287–298.
SAT-2015-IvriiRS #incremental #mining: Mining Backbone Literals in Incremental SAT — A New Kind of Incremental Data (AI, VR, OS), pp. 88–103.
SAT-2015-LonsingE #api #incremental: Incrementally Computing Minimal Unsatisfiable Cores of QBFs via a Clause Group Solver API (FL, UE), pp. 191–198.
SAT-2015-MangalZNN #framework #lazy evaluation #named #scalability: Volt: A Lazy Grounding Framework for Solving Very Large MaxSAT Instances (RM, XZ, AVN, MN), pp. 299–306.
SAT-2015-MenciaPM #bound: SAT-Based Horn Least Upper Bounds (CM, AP, JMS), pp. 423–433.
SAT-2015-NevesMJLM: Exploiting Resolution-Based Representations for MaxSAT Solving (MN, RM, MJ, IL, VMM), pp. 272–286.
SAT-2015-NewshamLGLFC #evolution #named #visualisation: SATGraf: Visualizing the Evolution of SAT Formula Structure in Solvers (ZN, WL, VG, JHL, SF, KC), pp. 62–70.
SAT-2015-Oh #difference: Between SAT and UNSAT: The Fundamental Difference in CDCL SAT (CO), pp. 307–323.
SAT-2015-TuHJ #learning #named #reasoning: QELL: QBF Reasoning with Extended Clause Learning and Levelized SAT Solving (KHT, TCH, JHRJ), pp. 343–359.
ICALP-v1-2014-Hertli: Breaking the PPSZ Barrier for Unique 3-SAT (TH), pp. 600–611.
ICALP-v1-2014-Tzameret #algorithm #problem #random: Sparser Random 3-SAT Refutation Algorithms and the Interpolation Problem — (IT), pp. 1015–1026.
LATA-2014-CarapelleFGQ #word: Satisfiability for MTL and TPTL over Non-monotonic Data Words (CC, SF, OFG, KQ), pp. 248–259.
LATA-2014-GwynneK #constraints #on the: On SAT Representations of XOR Constraints (MG, OK), pp. 409–420.
KR-2014-Belardinelli #logic: Satisfiability of Alternating-Time Temporal Epistemic Logic Through Tableaux (FB).
OOPSLA-2014-UhlerD: Smten with satisfiability-based search (RU, ND), pp. 157–176.
POPL-2014-DSilvaHK: Abstract satisfaction (VD, LH, DK), pp. 139–150.
ASE-2014-HagiharaESY #set #specification: Minimal strongly unsatisfiable subsets of reactive system specifications (SH, NE, MS, NY), pp. 629–634.
FSE-2014-LiYP0H #finite #infinity #ltl #named: Aalta: an LTL satisfiability checker over Infinite/Finite traces (JL, YY, GP, LZ, JH), pp. 731–734.
ICSE-2014-DegiovanniAAU #automation: Automated goal operationalisation based on interpolation and SAT solving (RD, DA, NA, SU), pp. 129–139.
SLE-2014-KaufmannKPSW #debugging #diagrams #sequence chart #state machine: A SAT-Based Debugging Tool for State Machines and Sequence Diagrams (PK, MK, AP, MS, MW), pp. 21–40.
DAC-2014-ChakrabortyMV #generative #scalability: Balancing Scalability and Uniformity in SAT Witness Generator (SC, KSM, MYV), p. 6.
DATE-2014-CabodiPQV #approximate #reachability: Tightening BDD-based approximate reachability with SAT-based clause generalization∗ (GC, PP, SQ, DV), pp. 1–6.
PDP-2014-AudemardHJP #approach #distributed #effectiveness #problem: An Effective Distributed D&C Approach for the Satisfiability Problem (GA, BH, SJ, CP), pp. 183–187.
STOC-2014-Coja-Oghlan: The asymptotic k-SAT threshold (ACO), pp. 804–813.
STOC-2014-DingSS #random: Satisfiability threshold for random regular NAE-SAT (JD, AS, NS), pp. 814–822.
TACAS-2014-ArmandoCC #model checking #named: SATMC: A SAT-Based Model Checker for Security-Critical Systems (AA, RC, LC), pp. 31–45.
TACAS-2014-HeizmannCDHLMSWP #contest: Ultimate Automizer with Unsatisfiable Cores — (Competition Contribution) (MH, JC, DD, JH, ML, BM, CS, SW, AP), pp. 418–420.
IJCAR-2014-AnsoteguiBGL: The Fractal Dimension of SAT Formulas (CA, MLB, JGC, JL), pp. 107–121.
IJCAR-2014-CerritoDG #atl #logic #testing: Optimal Tableaux-Based Decision Procedure for Testing Satisfiability in the Alternating-Time Temporal Logic ATL+ (SC, AD, VG), pp. 277–291.
IJCAR-2014-ChocronFR: A Gentle Non-disjoint Combination of Satisfiability Procedures (PC, PF, CR), pp. 122–136.
IJCAR-2014-EhlersL #approximate #finite #incremental #logic: A Tool That Incrementally Approximates Finite Satisfiability in Full Interval Temporal Logic (RE, ML), pp. 360–366.
IJCAR-2014-LahavZ #calculus: SAT-Based Decision Procedure for Analytic Pure Sequent Calculi (OL, YZ), pp. 76–90.
ISSTA-2014-LinK #automation #concurrent #multi #source code #thread #using: Automatic repair for multi-threaded programs with Deadlock/Livelock using maximum satisfiability (YL, SSK), pp. 237–247.
LICS-CSL-2014-BrotherstonFPG #induction #logic: A decision procedure for satisfiability in separation logic with inductive predicates (JB, CF, JANP, NG), p. 10.
LICS-CSL-2014-FredriksonJ #approach #privacy: Satisfiability modulo counting: a new approach for analyzing privacy properties (MF, SJ), p. 10.
SAT-2014-AudemardS #lazy evaluation #parallel #policy: Lazy Clause Exchange Policy for Parallel SAT Solvers (GA, LS), pp. 197–205.
SAT-2014-BacchusN #algorithm #analysis: Cores in Core Based MaxSat Algorithms: An Analysis (FB, NN), pp. 7–15.
SAT-2014-BalintBFS #heuristic #implementation: Improving Implementation of SLS Solvers for SAT and New Heuristics for k-SAT with Long Clauses (AB, AB, AF, US), pp. 302–316.
SAT-2014-Bulatov0 #approximate #random: Approximating Highly Satisfiable Random 2-SAT (AAB, CW), pp. 384–398.
SAT-2014-Gableske #framework: An Ising Model Inspired Extension of the Product-Based MP Framework for SAT (OG), pp. 367–383.
SAT-2014-HaanS #parametricity #reduction: Fixed-Parameter Tractable Reductions to SAT (RdH, SS), pp. 85–102.
SAT-2014-IgnatievMM #independence #on the #set: On Reducing Maximum Independent Set to Minimum Satisfiability (AI, AM, JMS), pp. 103–120.
SAT-2014-KonevL: A SAT Attack on the Erdős Discrepancy Conjecture (BK, AL), pp. 219–226.
SAT-2014-MartinsML #composition #named: Open-WBO: A Modular MaxSAT Solver, (RM, VMM, IL), pp. 438–445.
SAT-2014-NadelRS #incremental: Ultimately Incremental SAT (AN, VR, OS), pp. 206–218.
SAT-2014-NewshamGFAS #community #performance: Impact of Community Structure on SAT Solver Performance (ZN, VG, SF, GA, LS), pp. 252–268.
SAT-2014-Nordstrom #complexity #overview #proving: A (Biased) Proof Complexity Survey for SAT Practitioners (JN), pp. 1–6.
SAT-2014-SaetherTV: Solving MaxSAT and #SAT on Structured CNF Formulas (SHS, JAT, MV), pp. 16–31.
SAT-2014-SakaiST #reduction #strict: Solving Sparse Instances of Max SAT via Width Reduction and Greedy Restriction (TS, KS, ST), pp. 32–47.
SAT-2014-SonobeKI #branch #community #parallel: Community Branching for Parallel Portfolio SAT Solvers (TS, SK, MI), pp. 188–196.
VMCAI-2014-BloemKS #safety #specification #synthesis: SAT-Based Synthesis Methods for Safety Specs (RB, RK, MS), pp. 1–20.
CIKM-2013-JabbourSS #mining #sequence: Boolean satisfiability for sequence mining (SJ, LS, YS), pp. 649–658.
HILT-2013-Bjorner #development #modulo theories: Satisfiability modulo theories for high integrity development (NB), pp. 5–6.
QAPL-2013-Schuppan #ltl: Enhancing Unsatisfiable Cores for LTL with Information on Temporal Relevance (VS), pp. 49–65.
SAC-2013-ChocklerIMRS #using: Using cross-entropy for satisfiability (HC, AI, AM, SFR, NS), pp. 1196–1203.
SAC-2013-LaroucheMGH #equation #word: Solving equations on words through boolean satisfiability (ML, ABM, SG, SH), pp. 104–106.
DAC-2013-WuWLH #algorithm #generative #model checking: A counterexample-guided interpolant generation algorithm for SAT-based model checking (CYW, CAW, CYL, CY(H), p. 6.
DATE-2013-Belov0MM #abstraction: Core minimization in SAT-based abstraction (AB, HC, AM, JMS), pp. 1411–1416.
DATE-2013-KumarCT #approach #distributed #realtime: A satisfiability approach to speed assignment for distributed real-time systems (PK, DBC, LT), pp. 749–754.
DATE-2013-MillerB #parametricity #verification: Formal verification of analog circuit parameters across variation utilizing SAT (MM, FB), pp. 1442–1447.
DATE-2013-SauerRSPB #performance: Efficient SAT-based dynamic compaction and relaxation for longest sensitizable paths (MS, SR, TS, IP, BB), pp. 448–453.
STOC-2013-Coja-OghlanP: Going after the k-SAT threshold (ACO, KP), pp. 705–714.
STOC-2013-Huang #approximate: Approximation resistance on satisfiable instances for predicates with few accepting inputs (SH), pp. 457–466.
TACAS-2013-WieringaH #incremental #manycore: Asynchronous Multi-core Incremental SAT Solving (SW, KH), pp. 139–153.
CADE-2013-KaminskiT #incremental #named #reasoning #reduction: InKreSAT: Modal Reasoning via Incremental Reduction to SAT (MK, TT), pp. 436–442.
CADE-2013-WilliamsK #problem #proving #reduction: Propositional Temporal Proving with Reductions to a SAT Problem (RW, BK), pp. 421–435.
CAV-2013-ChakrabortyMV #generative #scalability: A Scalable and Nearly Uniform Generator of SAT Witnesses (SC, KSM, MYV), pp. 608–623.
ICLP-J-2013-ArbelaezTC #parallel #predict #runtime #using: Using sequential runtime distributions for the parallel speedup prediction of SAT local search (AA, CT, PC), pp. 625–639.
ICST-2013-AbadABCFGMMRV #bound #contract #generative #incremental #testing: Improving Test Generation under Rich Contracts by Tight Bounds and Incremental SAT Solving (PA, NA, VSB, DC, MFF, JPG, TSEM, MMM, NR, IV), pp. 21–30.
SAT-2013-AudemardLS #incremental: Improving Glucose for Incremental SAT Solving with Assumptions: Application to MUS Extraction (GA, JML, LS), pp. 309–317.
SAT-2013-Ben-Ari #education #named: LearnSAT: A SAT Solver for Education (MBA), pp. 403–407.
SAT-2013-CimattiGSS #approach #composition #modulo theories: A Modular Approach to MaxSAT Modulo Theories (AC, AG, BJS, RS), pp. 150–165.
SAT-2013-DaviesB #power of: Exploiting the Power of mip Solvers in maxsat (JD, FB), pp. 166–181.
SAT-2013-FingerLGS #constraints #probability #using: Solutions for Hard and Soft Constraints Using Optimized Probabilistic Satisfiability (MF, RL, CPG, BS), pp. 233–249.
SAT-2013-FujitaKH #constraints #named: SCSat: A Soft Constraint Guided SAT Solver (HF, MK, RH), pp. 415–421.
SAT-2013-Gableske #heuristic #message passing #on the: On the Interpolation between Product-Based Message Passing Heuristics for SAT (OG), pp. 293–308.
SAT-2013-HeuleS #approach #clique: A SAT Approach to Clique-Width (MH, SS), pp. 318–334.
SAT-2013-IgnatievJM #approach #quantifier: Quantified Maximum Satisfiability: — A Core-Guided Approach (AI, MJ, JMS), pp. 250–266.
SAT-2013-IserST #modelling: Minimizing Models for Tseitin-Encoded SAT Instances (MI, CS, MT), pp. 224–232.
SAT-2013-MantheyPW: Soundness of Inprocessing in Clause Sharing SAT Solvers (NM, TP, CW), pp. 22–39.
SAT-2013-MartinsML #clustering: Community-Based Partitioning for MaxSAT Solving (RM, VMM, IL), pp. 182–191.
SAT-2013-SohTB #agile #constraints #named #programming #prototype: Scarab: A Rapid Prototyping Tool for SAT-Based Constraint Programming Systems (TS, NT, MB), pp. 429–436.
VMCAI-2013-MouraJ #calculus: A Model-Constructing Satisfiability Calculus (LMdM, DJ), pp. 1–12.
ICALP-v1-2012-AchlioptasM #bound #random: Unsatisfiability Bounds for Random CSPs from an Energetic Interpolation Method (DA, RMM), pp. 1–12.
ICALP-v1-2012-GaspersS: Backdoors to Acyclic SAT (SG, SS), pp. 363–374.
ECMFA-2012-KuhlmannG #modelling #ocl #representation #uml #validation: Strengthening SAT-Based Validation of UML/OCL Models by Representing Collections as Relations (MK, MG), pp. 32–48.
SAS-2012-DSilvaHK: Satisfiability Solvers Are Static Analysers (VD, LH, DK), pp. 317–333.
DAC-2012-KengV #abstraction #debugging #design #refinement: Path directed abstraction and refinement in SAT-based design debugging (BK, AGV), pp. 947–954.
DAC-2012-LinMK #logic #using: Boolean satisfiability using noise based logic (PCKL, AM, SPK), pp. 1260–1261.
DAC-2012-RyzhenkoB #standard: Standard cell routing via boolean satisfiability (NR, SB), pp. 603–612.
DATE-2012-LeMKV #debugging #using: Non-solution implications using reverse domination in a modern SAT-based debugging environment (BL, HM, BK, AGV), pp. 629–634.
DATE-2012-SekaninaV #optimisation #polymorphism: A SAT-based fitness function for evolutionary optimization of polymorphic circuits (LS, ZV), pp. 715–720.
FASE-2012-AlrajehKRU #learning #specification: Learning from Vacuously Satisfiable Scenario-Based Specifications (DA, JK, AR, SU), pp. 377–393.
STOC-2012-BartoK #constraints #problem #robust: Robust satisfiability of constraint satisfaction problems (LB, MK), pp. 931–940.
STOC-2012-Coja-OghlanP: Catching the k-NAESAT threshold (ACO, KP), pp. 899–908.
TACAS-2012-ZaeemGKM #data type #using: History-Aware Data Structure Repair Using SAT (RNZ, DG, SK, KSM), pp. 2–17.
CAV-2012-HanJ: When Boolean Satisfiability Meets Gaussian Elimination in a Simplex Way (CSH, JHRJ), pp. 410–426.
CSL-2012-BertrandFS #bound: Bounded Satisfiability for PCTL (NB, JF, SS), pp. 92–106.
CSL-2012-Lynce #named: Satisfiability: where Theory meets Practice (IL), pp. 12–13.
ICLP-2012-AndresKMS #optimisation: Unsatisfiability-based optimization in clasp (BA, BK, OM, TS), pp. 211–221.
ICLP-J-2012-Duck #constraints #named: SMCHR: Satisfiability modulo constraint handling rules (GJD), pp. 601–618.
ICLP-J-2012-MetodiC #compilation #constraints #finite: Compiling finite domain constraints to SAT with BEE (AM, MC), pp. 465–483.
IJCAR-2012-BaaderBM #encoding #ontology #strict #unification: SAT Encoding of Unification in ℰℒℋ_R⁺ w.r.t. Cycle-Restricted Ontologies (FB, SB, BM), pp. 30–44.
IJCAR-2012-Bjorner: Taking Satisfiability to the Next Level with Z3 — (NB), pp. 1–8.
IJCAR-2012-GaoAC: δ-Complete Decision Procedures for Satisfiability over the Reals (SG, JA, EMC), pp. 286–300.
IJCAR-2012-Nieuwenhuis #challenge #smt: SAT and SMT Are Still Resolution: Questions and Challenges (RN), pp. 10–13.
SAT-2012-AchlioptasM #algorithm #bound #exponential #random: Exponential Lower Bounds for DPLL Algorithms on Satisfiable Random 3-CNF Formulas (DA, RMM), pp. 327–340.
SAT-2012-AnsoteguiGL #community: The Community Structure of SAT Formulas (CA, JGC, JL), pp. 410–423.
SAT-2012-AudemardHJLP #parallel: Revisiting Clause Exchange in Parallel SAT Solving (GA, BH, SJ, JML, CP), pp. 200–213.
SAT-2012-BloomGHSSS #framework #game studies #named #parallel #scalability: SatX10: A Scalable Plug&Play Parallel SAT Framework — (BB, DG, BH, AS, HS, VAS), pp. 463–468.
SAT-2012-CreignouV #complexity #problem: Parameterized Complexity of Weighted Satisfiability Problems (NC, HV), pp. 341–354.
SAT-2012-GaneshOSDRS #named #problem: Lynx: A Programmatic SAT Solver for the RNA-Folding Problem (VG, CWO, MS, SD, MCR, ASL), pp. 143–156.
SAT-2012-GaspersS: Strong Backdoors to Nested Satisfiability (SG, SS), pp. 72–85.
SAT-2012-Hugel #named #random: SATLab: X-Raying Random k-SAT — (TH), pp. 424–429.
SAT-2012-HyvarinenM #design #parallel #scalability: Designing Scalable Parallel SAT Solvers (AEJH, NM), pp. 214–227.
SAT-2012-Knuth #programming: Satisfiability and The Art of Computer Programming (DEK), p. 15.
SAT-2012-KottlerZSK #analysis #named: CoPAn: Exploring Recurring Patterns in Conflict Analysis of CDCL SAT Solvers — (SK, CZ, PS, MK), pp. 449–455.
SAT-2012-KullmannZ #on the #reduction: On Davis-Putnam Reductions for Minimally Unsatisfiable Clause-Sets (OK, XZ), pp. 270–283.
SAT-2012-MorgadoHM: Improvements to Core-Guided Binary Search for MaxSAT (AM, FH, JMS), pp. 284–297.
SAT-2012-NadelR #performance: Efficient SAT Solving under Assumptions (AN, VR), pp. 242–255.
SAT-2012-NadelRS #incremental #preprocessor: Preprocessing in Incremental SAT (AN, VR, OS), pp. 256–269.
SAT-2012-TanjoTB #csp #encoding #named #order #using: Azucar: A SAT-Based CSP Solver Using Compact Order Encoding — (TT, NT, MB), pp. 456–462.
SMT-2012-Biere #aspect-oriented: Practical Aspects of SAT Solving (AB), p. 1.
SMT-2012-BjornerMR #modulo theories #verification: Program Verification as Satisfiability Modulo Theories (NB, KLM, AR), pp. 3–11.
SMT-2012-PhanBM #quantifier: Anatomy of Alternating Quantifier Satisfiability (ADP, NB, DM), pp. 120–130.
TAP-2012-CreignouES #framework #random #specification: A Framework for the Specification of Random SAT and QSAT Formulas (NC, UE, MS), pp. 163–168.
VMCAI-2012-OeSOC #named: versat: A Verified Modern SAT Solver (DO, AS, CO, KC), pp. 363–378.
CIAA-2011-CastanoC #approach: Variable and Clause Ordering in an FSA Approach to Propositional Satisfiability (JMC, RC), pp. 76–87.
ICALP-v1-2011-Coja-OghlanP #process #random: The Decimation Process in Random k-SAT (ACO, AYPP), pp. 305–316.
ICALP-v1-2011-NordstromR #on the #trade-off: On Minimal Unsatisfiability and Time-Space Trade-offs for k-DNF Resolution (JN, AAR), pp. 642–653.
FM-2011-RozierV #approach #encoding #ltl #multi: A Multi-encoding Approach for LTL Symbolic Satisfiability Checking (KYR, MYV), pp. 417–431.
SEFM-2011-EggersRNF #analysis #hybrid: Improving SAT Modulo ODE for Hybrid Systems Analysis by Combining Different Enclosure Methods (AE, NR, NSN, MF), pp. 172–187.
SEFM-2011-ParrinoGGF #analysis #bound #data flow #verification: A Dataflow Analysis to Improve SAT-Based Bounded Program Verification (BCP, JPG, DG, MFF), pp. 138–154.
KDD-2011-GilpinD #algorithm #approach #clustering #flexibility #performance: Incorporating SAT solvers into hierarchical clustering algorithms: an efficient and flexible approach (SG, IND), pp. 1136–1144.
TOOLS-EUROPE-2011-KuhlmannHG #modelling #ocl #validation: Extensive Validation of OCL Models by Integrating SAT Solving into USE (MK, LH, MG), pp. 290–306.
PLDI-2011-JoseM #fault #locality #using: Cause clue clauses: error localization using maximum satisfiability (MJ, RM), pp. 437–446.
SAS-2011-SuterKK #recursion #source code: Satisfiability Modulo Recursive Programs (PS, ASK, VK), pp. 298–315.
ASE-2011-ArcainiGR #automation #generative #optimisation #smt #testing: Optimizing the automatic test generation by SAT and SMT solving for Boolean expressions (PA, AG, ER), pp. 388–391.
SAC-2011-RosaGO #problem #quality: Optimal stopping methods for finding high quality solutions to satisfiability problems with preferences (EDR, EG, BO), pp. 901–906.
DAC-2011-LinH #using: Using SAT-based Craig interpolation to enlarge clock gating functions (THL, CY(H), pp. 621–626.
DATE-2011-KochteW #evaluation #fault: SAT-based fault coverage evaluation in the presence of unknown values (MAK, HJW), pp. 1303–1308.
DATE-2011-SafarESS #configuration management #pipes and filters: A reconfigurable, pipelined, conflict directed jumping search SAT solver (MS, MWEK, MS, AS), pp. 1243–1248.
STOC-2011-MoserS #algorithm: A full derandomization of schöning’s k-SAT algorithm (RAM, DS), pp. 245–252.
TACAS-2011-GopinathMK #program repair #using: Specification-Based Program Repair Using SAT (DG, MZM, SK), pp. 173–188.
TACAS-2011-GriggioLS #generative #integer #linear #performance: Efficient Interpolant Generation in Satisfiability Modulo Linear Integer Arithmetic (AG, TTHL, RS), pp. 143–157.
TACAS-2011-TeigeF #probability #problem: Generalized Craig Interpolation for Stochastic Boolean Satisfiability Problems (TT, MF), pp. 158–172.
CADE-2011-Brown #higher-order #problem #proving #sequence #theorem proving: Reducing Higher-Order Theorem Proving to a Sequence of SAT Problems (CEB), pp. 147–161.
CADE-2011-KlinovP #hybrid #probability: A Hybrid Method for Probabilistic Satisfiability (PK, BP), pp. 354–368.
CAV-2011-BrauerKK #incremental #quantifier: Existential Quantification as Incremental SAT (JB, AK, JK), pp. 191–207.
ICLP-J-2011-CodishGBFG #analysis #constraints #integer #termination #using: SAT-based termination analysis using monotonicity constraints over the integers (MC, IG, AMBA, CF, JG), pp. 503–520.
LICS-2011-HerrmannZ #complexity #quantum: Computational Complexity of Quantum Satisfiability (CH, MZ), pp. 175–184.
SAT-2011-ArgelichLMP #evaluation: Analyzing the Instances of the MaxSAT Evaluation (JA, CML, FM, JP), pp. 360–361.
SAT-2011-BelovS: Minimally Unsatisfiable Boolean Circuits (AB, JPMS), pp. 145–158.
SAT-2011-DantsinH: Satisfiability Certificates Verifiable in Subexponential Time (ED, EAH), pp. 19–32.
SAT-2011-GableskeH #named #random #using: EagleUP: Solving Random 3-SAT Using SLS with Unit Propagation (OG, MH), pp. 367–368.
SAT-2011-Gelder11a: Generalized Conflict-Clause Strengthening for Satisfiability Solvers (AVG), pp. 329–342.
SAT-2011-KatebiSS #empirical: Empirical Study of the Anatomy of Modern Sat Solvers (HK, KAS, JPMS), pp. 343–356.
SAT-2011-MalitskySSS #algorithm: Non-Model-Based Algorithm Portfolios for SAT (YM, AS, HS, MS), pp. 369–370.
SAT-2011-Nadel #generative: Generating Diverse Solutions in SAT (AN), pp. 287–301.
SAT-2011-OrdyniakPS: Satisfiability of Acyclic and almost Acyclic CNF Formulas (II) (SO, DP, SS), pp. 47–60.
SAT-2011-PetkeJ #csp #encoding #order: The Order Encoding: From Tractable CSP to Tractable SAT (JP, PJ), pp. 371–372.
SAT-2011-PrevitiRSS: Applying UCT to Boolean Satisfiability (AP, RR, MS, BS), pp. 373–374.
SAT-2011-RyvchinS #performance: Faster Extraction of High-Level Minimal Unsatisfiable Cores (VR, OS), pp. 174–187.
SAT-2011-SilverthornM #learning: Learning Polarity from Structure in SAT (BS, RM), pp. 377–378.
SAT-2011-SpeckenmeyerWP #approach #graph: A Satisfiability-Based Approach for Embedding Generalized Tanglegrams on Level Graphs (ES, AW, SP), pp. 134–144.
SAT-2011-TompkinsBH #heuristic: Captain Jack: New Variable Selection Heuristics in Local Search for SAT (DADT, AB, HHH), pp. 302–316.
SAT-2011-Williams #algorithm #bound #complexity: Connecting SAT Algorithms and Complexity Lower Bounds (RW), pp. 1–2.
TAP-2011-SoekenWD #data type #encoding #modelling #ocl #uml #verification: Encoding OCL Data Types for SAT-Based Verification of UML/OCL Models (MS, RW, RD), pp. 152–170.
VMCAI-2011-Bradley #model checking: SAT-Based Model Checking without Unrolling (ARB), pp. 70–87.
VMCAI-2011-SuterSK #constraints #modulo theories #set: Sets with Cardinality Constraints in Satisfiability Modulo Theories (PS, RS, VK), pp. 403–418.
ICALP-v1-2010-DietzfelbingerGMMPR: Tight Thresholds for Cuckoo Hashing via XORSAT (MD, AG, MM, AM, RP, MR), pp. 213–225.
ICALP-v1-2010-Welzl #constraints: When Conflicting Constraints Can Be Resolved — The Lovász Local Lemma and Satisfiability (EW), p. 18.
ICALP-v2-2010-AchilleosLM: Parameterized Modal Satisfiability (AA, ML, VM), pp. 369–380.
LATA-2010-AravantinosCP #complexity #problem: Complexity of the Satisfiability Problem for a Class of Propositional Schemata (VA, RC, NP), pp. 58–69.
LATA-2010-Cruz-SantosM #on the #quantum #reduction: On the Hamiltonian Operators for Adiabatic Quantum Reduction of SAT (WCS, GML), pp. 239–248.
FLOPS-2010-HoweK #prolog: A Pearl on SAT Solving in Prolog (JMH, AK), pp. 165–174.
FLOPS-2010-TamuraTB #constraints #problem: Solving Constraint Satisfaction Problems with SAT Technology (NT, TT, MB), pp. 19–23.
ICGT-2010-KreowskiKW #graph transformation: Graph Transformation Units Guided by a SAT Solver (HJK, SK, RW), pp. 27–42.
KR-2010-XiaoLMQ #consistency #metric #multi #nondeterminism #semantics: Computing Inconsistency Measurements under Multi-Valued Semantics by Partial Max-SAT Solvers (GX, ZL, YM, GQ).
POPL-2010-HarrisSIG #program analysis #source code: Program analysis via satisfiability modulo path programs (WRH, SS, FI, AG), pp. 71–82.
PPDP-2010-BofillBV #approach #declarative #robust: A declarative approach to robust weighted Max-SAT (MB, DB, MV), pp. 67–76.
SAC-2010-JiaLLZ: Local lemma: a new strategy of pruning in SAT solvers (XJ, RL, SL, JZ), pp. 2071–2072.
DAC-2010-PigorschS #preprocessor #using: An AIG-Based QBF-solver using SAT for preprocessing (FP, CS), pp. 170–175.
DAC-2010-ThalmaierNWSBK #induction #invariant: Analyzing k-step induction to compute invariants for SAT-based property checking (MT, MDN, MW, DS, JB, WK), pp. 176–181.
DATE-2010-ChenQM #generative #performance #testing: Efficient decision ordering techniques for SAT-based test generation (MC, XQ, PM), pp. 490–495.
DATE-2010-SoekenWKGD #modelling #ocl #uml #using #verification: Verifying UML/OCL models using Boolean satisfiability (MS, RW, MK, MG, RD), pp. 1341–1344.
DATE-2010-YangCZH #multi: SAT based multi-net rip-up-and-reroute for manufacturing hotspot removal (FY, YC, QZ, JH), pp. 1369–1372.
STOC-2010-DellM #polynomial: Satisfiability allows no nontrivial sparsification unless the polynomial-time hierarchy collapses (HD, DvM), pp. 251–260.
STOC-2010-PaturiP #complexity #on the: On the complexity of circuit satisfiability (RP, PP), pp. 241–250.
TACAS-2010-BardinHP: An Alternative to SAT-Based Approaches for Bit-Vectors (SB, PH, FP), pp. 84–98.
TACAS-2010-CimattiFGSS #formal method: Satisfiability Modulo the Theory of Costs: Foundations and Applications (AC, AF, AG, RS, CS), pp. 99–113.
TACAS-2010-MalinowskiN #automaton #bound #model checking #partial order #semantics: SAT Based Bounded Model Checking with Partial Order Semantics for Timed Automata (JM, PN), pp. 405–419.
IJCAR-2010-AravantinosCP10a #named: RegSTAB: A SAT Solver for Propositional Schemata (VA, RC, NP), pp. 309–315.
SAT-2010-BalintF #probability: Improving Stochastic Local Search for SAT with a New Probability Distribution (AB, AF), pp. 10–15.
SAT-2010-BelovS: Improved Local Search for Circuit Satisfiability (AB, ZS), pp. 293–299.
SAT-2010-BoufkhadH #bound: Non Uniform Selection of Solutions for Upper Bounding the 3-SAT Threshold (YB, TH), pp. 99–112.
SAT-2010-BrummayerLB #automation #debugging #testing: Automated Testing and Debugging of SAT and QBF Solvers (RB, FL, AB), pp. 44–57.
SAT-2010-DantsinW #exponential #on the: On Moderately Exponential Time for SAT (ED, AW), pp. 313–325.
SAT-2010-Ehlers #automaton #using: Minimising Deterministic Büchi Automata Precisely Using SAT Solving (RE), pp. 326–332.
SAT-2010-FuhsS #linear #source code #using: Synthesizing Shortest Linear Straight-Line Programs over GF(2) Using SAT (CF, PSK), pp. 71–84.
SAT-2010-GelderS #design: Zero-One Designs Produce Small Hard SAT Instances (AVG, IS), pp. 388–397.
SAT-2010-KatebiSM #symmetry: Symmetry and Satisfiability: An Update (HK, KAS, ILM), pp. 113–127.
SAT-2010-Kottler: SAT Solving with Reference Points (SK), pp. 143–157.
SAT-2010-Kullmann: Green-Tao Numbers and SAT (OK), pp. 352–362.
SAT-2010-LiMQZ: Exact MinSAT Solving (CML, FM, ZQ, ZZ), pp. 363–368.
SAT-2010-ManquinhoML #algorithm #optimisation: Improving Unsatisfiability-Based Algorithms for Boolean Optimization (VMM, RM, IL), pp. 181–193.
SAT-2010-MatthewsP: Uniquely Satisfiable k-SAT Instances with Almost Minimal Occurrences of Each Variable (WM, RP), pp. 369–374.
SAT-2010-Nikolic #comparison #statistics: Statistical Methodology for Comparison of SAT Solvers (MN), pp. 209–222.
SAT-2010-PankratovB #on the #problem: On the Relative Merits of Simple Local Search Methods for the MAX-SAT Problem (DP, AB), pp. 223–236.
SAT-2010-RathiARS #bound #random: Bounds on Threshold of Regular Random k-SAT (VR, EA, LKR, MS), pp. 264–277.
SAT-2010-TompkinsH: Dynamic Scoring Functions with Variable Expressions: New SLS Methods for Solving SAT (DADT, HHH), pp. 278–292.
PODS-2009-AbiteboulBM #documentation #query: Satisfiability and relevance for queries over active documents (SA, PB, BM), pp. 87–96.
PODS-2009-Figueira #similarity #testing #xpath: Satisfiability of downward XPath with data equality tests (DF), pp. 197–206.
DLT-2009-Saarela #complexity #equation #on the #theorem: On the Complexity of Hmelevskii’s Theorem and Satisfiability of Three Unknown Equations (AS), pp. 443–453.
ICALP-v1-2009-Coja-Oghlan #algorithm #random: A Better Algorithm for Random k-SAT (ACO), pp. 292–303.
SPLC-2009-MendoncaWC #analysis #feature model #modelling: SAT-based analysis of feature models is easy (MM, AW, KC), pp. 231–240.
PPDP-2009-CodishGS #declarative #encoding: A declarative encoding of telecommunications feature subscription in SAT (MC, SG, PJS), pp. 255–266.
SAC-2009-GroppeNL #java #named #query #rdf #semantics #type safety #web: SWOBE — embedding the semantic web languages RDF, SPARQL and SPARUL into java for guaranteeing type safety, for checking the satisfiability of queries and for the determination of query result types (SG, JN, VL), pp. 1239–1246.
SAC-2009-KrocSS #heuristic #message passing: Message-passing and local heuristics as decimation strategies for satisfiability (LK, AS, BS), pp. 1408–1414.
DAC-2009-JainC #graph #performance #using: Efficient SAT solving for non-clausal formulas using DPLL, graphs, and watched cuts (HJ, EMC), pp. 563–568.
DAC-2009-WangCL #network #scalability #simulation: Simulation and SAT-based Boolean matching for large Boolean networks (KHW, CMC, JCL), pp. 396–401.
DATE-2009-ChambersMV #generative #performance: Faster SAT solving with better CNF generation (BC, PM, DV), pp. 1590–1595.
DATE-2009-SulflowFBKD #debugging: Increasing the accuracy of SAT-based debugging (AS, GF, CB, UK, RD), pp. 1326–1331.
DATE-2009-ZhengH #array #logic #programmable: Defect-aware logic mapping for nanowire-based programmable logic arrays via satisfiability (YZ, CH), pp. 1279–1283.
STOC-2009-ODonnellW: Conditional hardness for satisfiable 3-CSPs (RO, YW), pp. 493–502.
TACAS-2009-NicoliniRR #integer: Satisfiability Procedures for Combination of Theories Sharing Integer Offsets (EN, CR, MR), pp. 428–442.
CADE-2009-BonacinaLM #on the #proving #theorem proving: On Deciding Satisfiability by DPLL(G+T) and Unsound Theorem Proving (MPB, CL, LMdM), pp. 35–50.
CADE-2009-BorrallerasLNRR #linear #polynomial: Solving Non-linear Polynomial Arithmetic via SAT Modulo Linear Arithmetic (CB, SL, RNM, ERC, AR), pp. 294–305.
CADE-2009-ClaessenL #automation #finite: Automated Inference of Finite Unsatisfiability (KC, AL), pp. 388–403.
CADE-2009-GoreW #on the fly: An Optimal On-the-Fly Tableau-Based Decision Procedure for PDL-Satisfiability (RG, FW), pp. 437–452.
CAV-2009-GeM #modulo theories #quantifier: Complete Instantiation for Quantified Formulas in Satisfiabiliby Modulo Theories (YG, LMdM), pp. 306–320.
ICLP-2009-Truszczynski #logic programming #semantics #source code: Reducts of Propositional Theories, Satisfiability Relations, and Generalizations of Semantics of Logic Programs (MT), pp. 175–189.
LICS-2009-KazakovP #complexity #logic #problem: A Note on the Complexity of the Satisfiability Problem for Graded Modal Logics (YK, IPH), pp. 407–416.
LICS-2009-KieronskiT #equivalence #finite #first-order #logic #on the: On Finite Satisfiability of Two-Variable First-Order Logic with Equivalence Relations (EK, LT), pp. 123–132.
SAT-2009-AnsoteguiBL #testing: Solving (Weighted) Partial MaxSAT through Satisfiability Testing (CA, MLB, JL), pp. 427–440.
SAT-2009-ArgelichCLM #encoding: Sequential Encodings from Max-CSP into Partial Max-SAT (JA, AC, IL, FM), pp. 161–166.
SAT-2009-BalintHG #approach #novel #problem: A Novel Approach to Combine a SLS- and a DPLL-Solver for the Satisfiability Problem (AB, MH, OG), pp. 284–297.
SAT-2009-BelovS #probability #process: Improving Variable Selection Process in Stochastic Local Search for Propositional Satisfiability (AB, ZS), pp. 258–264.
SAT-2009-BonetJ #metric #using: Efficiently Calculating Evolutionary Tree Measures Using SAT (MLB, KSJ), pp. 4–17.
SAT-2009-Chen #hybrid #reasoning: Building a Hybrid SAT Solver via Conflict-Driven, Look-Ahead and XOR Reasoning Techniques (JC), pp. 298–311.
SAT-2009-JohannsenRW #strict: Solving SAT for CNF Formulas with a One-Sided Restriction on Variable Occurrences (DJ, IR, MW), pp. 80–85.
SAT-2009-KimSJ #modulo theories #performance: Efficient Term-ITE Conversion for Satisfiability Modulo Theories (HK, FS, HJ), pp. 195–208.
SAT-2009-KrocSS: Relaxed DPLL Search for MaxSAT (LK, AS, BS), pp. 447–452.
SAT-2009-LiffitonS: Generalizing Core-Guided Max-SAT (MHL, KAS), pp. 481–494.
SAT-2009-LiMMP: Exploiting Cycle Structures in Max-SAT (CML, FM, NOM, JP), pp. 467–480.
SAT-2009-Nieuwenhuis #algorithm #modulo theories: SAT Modulo Theories: Enhancing SAT with Special-Purpose Algorithms (RN), p. 1.
SAT-2009-NikolicMJ #policy: Instance-Based Selection of Policies for SAT Solvers (MN, FM, PJ), pp. 326–340.
SAT-2009-OhmuraU #clustering #named #parallel: c-sat: A Parallel SAT Solver for Clusters (KO, KU), pp. 524–537.
SAT-2009-PipatsrisawatD #policy: Width-Based Restart Policies for Clause-Learning Satisfiability Solvers (KP, AD), pp. 341–355.
SAT-2009-SamerV #encoding: Encoding Treewidth into SAT (MS, HV), pp. 45–50.
SAT-2009-SoosNC #encryption #problem: Extending SAT Solvers to Cryptographic Problems (MS, KN, CC), pp. 244–257.
SAT-2009-Szeider #complexity: The Parameterized Complexity of k-Flip Local Search for SAT and MAX SAT (SS), pp. 276–283.
SAT-2009-Vardi: Symbolic Techniques in Propositional Satisfiability Solving (MYV), pp. 2–3.
TAP-2009-CalvagnaG #combinator #heuristic #interactive #testing: Combining Satisfiability Solving and Heuristics to Constrained Combinatorial Interaction Testing (AC, AG), pp. 27–42.
AFL-2008-BreveglieriCNR #equation #problem: NP-completeness of the alphabetical satisfiability problem for trace equations (LB, AC, CDN, ER), pp. 111–121.
ICALP-A-2008-EldarR #quantum: Quantum SAT for a Qutrit-Cinquit Pair Is QMA1-Complete (LE, OR), pp. 881–892.
ICALP-A-2008-RazgonO #parametricity: Almost 2-SAT Is Fixed-Parameter Tractable (IR, BO), pp. 551–562.
ICALP-B-2008-AxelssonHL #context-free grammar #incremental #using: Analyzing Context-Free Grammars Using an Incremental SAT Solver (RA, KH, ML), pp. 410–422.
ICALP-B-2008-Schewe: ATL* Satisfiability Is 2EXPTIME-Complete (SS), pp. 373–385.
FM-2008-TorlakCJ #declarative #specification: Finding Minimal Unsatisfiable Cores of Declarative Specifications (ET, FSHC, DJ), pp. 326–341.
GT-VC-2007-Pennemann08 #algorithm #approximate #problem: An Algorithm for Approximating the Satisfiability Problem of High-level Conditions (KHP), pp. 75–94.
ICEIS-DISI-2008-GroppeL #query #xpath: Discovering Veiled Unsatisfiable Xpath Queries (JG, VL), pp. 149–158.
SEKE-2008-ParkK08a #problem: Japanese Puzzle as a SAT Problem (SP, GK), pp. 543–548.
ASE-2008-KimKK #memory management #model checking #testing: Unit Testing of Flash Memory Device Driver through a SAT-Based Model Checker (MK, YK, HK), pp. 198–207.
ASE-2008-PradellaMP #bound #realtime #specification: Refining Real-Time System Specifications through Bounded Model- and Satisfiability-Checking (MP, AM, PSP), pp. 119–127.
DAC-2008-DavisTYZ #configuration management #hardware: A practical reconfigurable hardware accelerator for Boolean satisfiability solvers (JDD, ZT, FY, LZ), pp. 780–785.
DAC-2008-LeeJH #scalability: Bi-decomposing large Boolean functions via interpolation and satisfiability solving (RRL, JHRJ, WLH), pp. 636–641.
DATE-2008-FangH #algorithm #approximate #performance: A Fast Approximation Algorithm for MIN-ONE SAT (LF, MSH), pp. 1087–1090.
DATE-2008-Marques-SilvaP #algorithm #using: Algorithms for Maximum Satisfiability using Unsatisfiable Cores (JMS, JP), pp. 408–413.
DATE-2008-VelevG #comparison #encoding #problem: Comparison of Boolean Satisfiability Encodings on FPGA Detailed Routing Problems (MNV, PG), pp. 1268–1273.
TACAS-2008-Ben-AmramC #approach #ranking #termination: A SAT-Based Approach to Size Change Termination with Global Ranking Functions (AMBA, MC), pp. 218–232.
TACAS-2008-CimattiGS #generative #modulo theories #performance: Efficient Interpolant Generation in Satisfiability Modulo Theories (AC, AG, RS), pp. 397–412.
TACAS-2008-WulfDMR #algorithm #anti #ltl #model checking #named: Antichains: Alternative Algorithms for LTL Satisfiability and Model-Checking (MDW, LD, NM, JFR), pp. 63–77.
CAV-2008-KingS #congruence #equation #using: Inferring Congruence Equations Using SAT (AK, HS), pp. 281–293.
LICS-2008-BrazdilFKK #probability #problem: The Satisfiability Problem for Probabilistic CTL (TB, VF, JK, AK), pp. 391–402.
SAT-2008-ArgelichCLM #modelling: Modelling Max-CSP as Partial Max-SAT (JA, AC, IL, FM), pp. 1–14.
SAT-2008-ArgelichLM #preprocessor: A Preprocessor for Max-SAT Solvers (JA, CML, FM), pp. 15–20.
SAT-2008-Biere #adaptation: Adaptive Restart Strategies for Conflict Driven SAT Solvers (AB), pp. 28–33.
SAT-2008-DavisTYZ #design #hardware #performance: Designing an Efficient Hardware Implication Accelerator for SAT Solving (JDD, ZT, FY, LZ), pp. 48–62.
SAT-2008-EibachPV #using: Attacking Bivium Using SAT Solvers (TE, EP, GV), pp. 63–76.
SAT-2008-FaureNOR #formal method #linear: SAT Modulo the Theory of Linear Arithmetic: Exact, Inexact and Commercial Solvers (GF, RN, AO, ERC), pp. 77–90.
SAT-2008-GeorgiouP #algorithm #complexity: Complexity and Algorithms for Well-Structured k-SAT Instances (KG, PAP), pp. 105–118.
SAT-2008-HaimW #estimation #online #runtime: Online Estimation of SAT Solving Runtime (SH, TW), pp. 133–138.
SAT-2008-HerasL #clique #preprocessor: A Max-SAT Inference-Based Pre-processing for Max-Clique (FH, JL), pp. 139–152.
SAT-2008-Iwama: SAT, UNSAT and Coloring (KI), p. 153.
SAT-2008-KottlerKS08a #bound #np-hard #subclass #using: A New Bound for an NP-Hard Subclass of 3-SAT Using Backdoors (SK, MK, CS), pp. 161–167.
SAT-2008-LetombeM #algorithm #hybrid #incremental: Improvements to Hybrid Incremental SAT Algorithms (FL, JMS), pp. 168–181.
SAT-2008-LiffitonS #set: Searching for Autarkies to Trim Unsatisfiable Clause Sets (MHL, KAS), pp. 182–195.
SAT-2008-MarienWDB #induction #logic: SAT(ID): Satisfiability of Propositional Logic Extended with Inductive Definitions (MM, JW, MD, MB), pp. 211–224.
SAT-2008-Marques-SilvaM #algorithm #effectiveness #towards: Towards More Effective Unsatisfiability-Based Maximum Satisfiability Algorithms (JMS, VMM), pp. 225–230.
SAT-2008-SchederZ #how #question: How Many Conflicts Does It Need to Be Unsatisfiable? (DS, PZ), pp. 246–256.
SAT-2008-StachniakB #learning: Speeding-Up Non-clausal Local Search for Propositional Satisfiability with Clause Learning (ZS, AB), pp. 257–270.
RTA-2007-NieuwenhuisORR #challenge #modulo theories: Challenges in Satisfiability Modulo Theories (RN, AO, ERC, AR), pp. 2–18.
ECMDA-FA-2007-MaraeeB #diagrams #finite #performance #reasoning #set #uml: Efficient Reasoning About Finite Satisfiability of UML Class Diagrams with Constrained Generalization Sets (AM, MB), pp. 17–31.
ESEC-FSE-2007-DolbyVT #debugging: Finding bugs efficiently with a SAT solver (JD, MV, FT), pp. 195–204.
DAC-2007-DengBWYZ #named #performance #using: EHSAT: An Efficient RTL Satisfiability Solver Using an Extended DPLL Procedure (SD, JB, WW, XY, YZ), pp. 588–593.
DATE-2007-FangH #hybrid #performance: A new hybrid solution to boost SAT solver performance (LF, MSH), pp. 1307–1313.
DATE-2007-MangassarianVSNA #estimation #process #pseudo #using: Maximum circuit activity estimation using pseudo-boolean satisfiability (HM, AGV, SS, FNN, MSA), pp. 1538–1543.
DATE-2007-SafarSES #configuration management #interactive: Interactive presentation: A shift register based clause evaluator for reconfigurable SAT solver (MS, MS, MWEK, AS), pp. 153–158.
DATE-2007-TadesseSLBG #analysis #modelling #using: Accurate timing analysis using SAT and pattern-dependent delay models (DT, DS, EL, RIB, JG), pp. 1018–1023.
DATE-2007-WuLLH #named #robust: QuteSAT: a robust circuit-based SAT solver for complex circuit structure (CAW, THL, CCL, CYH), pp. 1313–1318.
FoSSaCS-2007-BaulandSSSV #complexity #linear #logic: The Complexity of Generalized Satisfiability for Linear Temporal Logic (MB, TS, HS, IS, HV), pp. 48–62.
STOC-2007-Austrin: Balanced max 2-sat might not be the hardest (PA), pp. 189–197.
TACAS-2007-AmlaM #abstraction #model checking #refinement: Combining Abstraction Refinement and SAT-Based Model Checking (NA, KLM), pp. 405–419.
TACAS-2007-KrsticGGT #parametricity: Combined Satisfiability Modulo Parametric Theories (SK, AG, JG, CT), pp. 602–617.
CADE-2007-DeshaneHJLLM #encoding #first-order #proving: Encoding First Order Proofs in SAT (TD, WH, PJ, HL, CL, REM), pp. 476–491.
CADE-2007-GeBT #modulo theories #quantifier #using #verification: Solving Quantified Verification Conditions Using Satisfiability Modulo Theories (YG, CB, CT), pp. 167–182.
CADE-2007-GhilardiNRZ #infinity #model checking: Combination Methods for Satisfiability and Model-Checking of Infinite-State Systems (SG, EN, SR, DZ), pp. 362–378.
CADE-2007-KoprowskiM #dependence #predict #using: Predictive Labeling with Dependency Pairs Using SAT (AK, AM), pp. 410–425.
CADE-2007-KuncakR #algebra #performance #towards: Towards Efficient Satisfiability Checking for Boolean Algebra with Presburger Arithmetic (VK, MCR), pp. 215–230.
CAV-2007-BrummayerB #c #named: C32SAT: Checking C Expressions (RB, AB), pp. 294–297.
CAV-2007-CimattiRST #abstraction #logic: Boolean Abstraction for Temporal Logic Satisfiability (AC, MR, VS, ST), pp. 532–546.
CAV-2007-MouraDS #modulo theories #tutorial: A Tutorial on Satisfiability Modulo Theories (LMdM, BD, NS), pp. 20–36.
CAV-2007-SinhaC #composition #lazy evaluation #learning #using #verification: SAT-Based Compositional Verification Using Lazy Learning (NS, EMC), pp. 39–54.
CSL-2007-FiliotTT #logic: Satisfiability of a Spatial Logic with Tree Variables (EF, JMT, ST), pp. 130–145.
MBT-2007-OuimetL #automation #consistency #specification #state machine #using #verification: Automated Verification of Completeness and Consistency of Abstract State Machine Specifications using a SAT Solver (MO, KL), pp. 85–97.
SAT-2007-AloulK #approach #deployment: Sensor Deployment for Failure Diagnosis in Networked Aerial Robots: A Satisfiability-Based Approach (FAA, NK), pp. 369–376.
SAT-2007-AnsoteguiBLM #csp: Mapping CSP into Many-Valued SAT (CA, MLB, JL, FM), pp. 10–15.
SAT-2007-ArgelichM #learning: Partial Max-SAT Solvers with Clause Learning (JA, FM), pp. 28–40.
SAT-2007-CimattiGS #flexibility #modulo theories: A Simple and Flexible Way of Computing Small Unsatisfiable Cores in SAT Modulo Theories (AC, AG, RS), pp. 334–339.
SAT-2007-Davis #named #past present future: SAT: Past and Future (MD), pp. 1–2.
SAT-2007-DershowitzHN #comprehension #towards: Towards a Better Understanding of the Functionality of a Conflict-Driven SAT Solver (ND, ZH, AN), pp. 287–293.
SAT-2007-EenMS #logic #synthesis: Applying Logic Synthesis for Speeding Up SAT (NE, AM, NS), pp. 272–286.
SAT-2007-FuhsGMSTZ #analysis #polynomial #termination: SAT Solving for Termination Analysis with Polynomial Interpretations (CF, JG, AM, PSK, RT, HZ), pp. 340–354.
SAT-2007-Gelder #verification: Verifying Propositional Unsatisfiability: Pitfalls to Avoid (AVG), pp. 328–333.
SAT-2007-HerasLO #named: MiniMaxSat: A New Weighted Max-SAT Solver (FH, JL, AO), pp. 41–55.
SAT-2007-HertelHU #encoding #formal method: Formalizing Dangerous SAT Encodings (AH, PH, AU), pp. 159–172.
SAT-2007-Kullmann #invariant #matrix #polynomial: Polynomial Time SAT Decision for Complementation-Invariant Clause-Sets, and Sign-non-Singular Matrices (OK), pp. 314–327.
SAT-2007-LiWZ #adaptation: Combining Adaptive Noise and Look-Ahead in Local Search for SAT (CML, WW, HZ), pp. 121–133.
SAT-2007-LynceM #matrix #modelling #symmetry: Breaking Symmetries in SAT Matrix Models (IL, JPMS), pp. 22–27.
SAT-2007-PipatsrisawatD #component #lightweight: A Lightweight Component Caching Scheme for Satisfiability Solvers (KP, AD), pp. 294–299.
SAT-2007-PorschenS #algorithm #problem: Algorithms for Variable-Weighted 2-SAT and Dual Problems (SP, ES), pp. 173–186.
SAT-2007-SchederZ #exponential #product line: Satisfiability with Exponential Families (DS, PZ), pp. 148–158.
ICALP-v1-2006-BjorklundH #algorithm: Exact Algorithms for Exact Satisfiability and Number of Perfect Matchings (AB, TH), pp. 548–559.
ICALP-v1-2006-GopalanKMP: The Connectivity of Boolean Satisfiability: Computational and Structural Dichotomies (PG, PGK, ENM, CHP), pp. 346–357.
SFM-2006-CimattiS #performance: Building Efficient Decision Procedures on Top of SAT Solvers (AC, RS), pp. 144–175.
SFM-2006-GuptaGW #hardware #verification: SAT-Based Verification Methods and Applications in Hardware Verification (AG, MKG, CW), pp. 108–143.
ICGT-2006-HabelP: Satisfiability of High-Level Conditions (AH, KHP), pp. 430–444.
ICEIS-DISI-2006-GroppeG #query #xpath: Filtering Unsatisfiable XPATH Queries (JG, SG), pp. 157–162.
PADL-2006-HawkinsS #constraints #finite #hybrid #theorem proving: A Hybrid BDD and SAT Finite Domain Constraint Solver (PH, PJS), pp. 103–117.
SAC-2006-LallouetL #consistency #constraints: From satisfiability to consistency through certificates: application to partially defined constraints (AL, AL), pp. 415–416.
DAC-2006-AksoyCFM #constraints #integer #linear #optimisation #programming #synthesis #using: Optimization of area under a delay constraint in digital filter synthesis using SAT-based integer linear programming (LA, EACdC, PFF, JM), pp. 669–674.
DAC-2006-SafarpourVBY #performance: Efficient SAT-based Boolean matching for FPGA technology mapping (SS, AGV, GB, RY), pp. 466–471.
DAC-2006-VimjamH #identification #induction #performance: Fast illegal state identification for improving SAT-based induction (VCV, MSH), pp. 241–246.
DAC-2006-ZhangMBC #detection #representation #scalability #simulation #symmetry #using: Symmetry detection for large Boolean functions using circuit representation, simulation, and satisfiability (JSZ, AM, RKB, MCJ), pp. 510–515.
DAC-2006-ZhuKKS: SAT sweeping with local observability don’t-cares (QZ, NK, AK, ALSV), pp. 229–234.
DATE-2006-FeySVD #on the: On the relation between simulation-based and SAT-based diagnosis (GF, SS, AGV, RD), pp. 1139–1144.
DATE-2006-JinS #analysis: Strong conflict analysis for propositional satisfiability (HJ, FS), pp. 818–823.
DATE-DF-2006-PotlapallyRRJL #encryption #framework: Satisfiability-based framework for enabling side-channel attacks on cryptographic software (NRP, AR, SR, NKJ, RBL), pp. 18–23.
TACAS-2006-Chaki #certification: SAT-Based Software Certification (SC), pp. 151–166.
CAV-2006-GershmanKS: Deriving Small Unsatisfiable Cores with Dominators (RG, MK, OS), pp. 109–122.
CAV-2006-RoordaC #abstraction #evaluation #refinement: SAT-Based Assistance in Abstraction Refinement for Symbolic Trajectory Evaluation (JWR, KC), pp. 175–189.
CSL-2006-ScheweF #calculus #finite #μ-calculus: Satisfiability and Finite Model Property for the Alternating-Time μ-Calculus (SS, BF), pp. 591–605.
IJCAR-2006-Darwiche #compilation #evolution: Searching While Keeping a Trace: The Evolution from Satisfiability to Knowledge Compilation (AD), p. 3.
IJCAR-2006-ReeberH #subclass: A SAT-Based Decision Procedure for the Subclass of Unrollable List Formulas in ACL2 (SULFA) (ER, WAHJ), pp. 453–467.
ISSTA-2006-DennisCJ #composition #verification: Modular verification of code with SAT (GD, FSHC, DJ), pp. 109–120.
LICS-2006-FischerMR #approximate #equivalence: Approximate Satisfiability and Equivalence (EF, FM, MdR), pp. 421–430.
SAT-2006-Bacchus #named: CSPs: Adding Structure to SAT (FB), p. 10.
SAT-2006-BonetLM #calculus: A Complete Calculus for Max-SAT (MLB, JL, FM), pp. 240–251.
SAT-2006-Buresh-OppenheimM: Minimum Witnesses for Unsatisfiable 2CNFs (JBO, DGM), pp. 42–47.
SAT-2006-DantsinW #constant #performance: MAX-SAT for Formulas with Constant Clause Density Can Be Solved Faster Than in O(s2) Time (ED, AW), pp. 266–276.
SAT-2006-DershowitzHN #algorithm #scalability: A Scalable Algorithm for Minimal Unsatisfiable Core Extraction (ND, ZH, AN), pp. 36–41.
SAT-2006-FuM #on the #problem: On Solving the Partial MAX-SAT Problem (ZF, SM), pp. 252–265.
SAT-2006-HsuM: Characterizing Propagation Methods for Boolean Satisfiability (EIH, SAM), pp. 325–338.
SAT-2006-HyvarinenJN: A Distribution Method for Solving SAT in Grids (AEJH, TAJ, IN), pp. 430–435.
SAT-2006-JainBC #using: Satisfiability Checking of Non-clausal Formulas Using General Matings (HJ, CB, EMC), pp. 75–89.
SAT-2006-JussilaSB #proving #quantifier: Extended Resolution Proofs for Symbolic SAT Solving with Quantification (TJ, CS, AB), pp. 54–60.
SAT-2006-KullmannLM #agile #categorisation #kernel #normalisation: Categorisation of Clauses in Conjunctive Normal Forms: Minimally Unsatisfiable Sub-clause-sets and the Lean Kernel (OK, IL, JMS), pp. 22–35.
SAT-2006-LynceM #type inference: SAT in Bioinformatics: Making the Case with Haplotype Inference (IL, JMS), pp. 136–141.
SAT-2006-MironovZ: Applications of SAT Solvers to Cryptanalysis of Hash Functions (IM, LZ), pp. 102–115.
SAT-2006-NieuwenhuisO #modulo theories #on the #optimisation #problem: On SAT Modulo Theories and Optimization Problems (RN, AO), pp. 156–169.
SAT-2006-NishimuraRS #using: Solving #SAT Using Vertex Covers (NN, PR, SS), pp. 396–409.
SAT-2006-PrestwichL: Local Search for Unsatisfiability (SDP, IL), pp. 283–296.
SAT-2006-SebastianiV #case study #encoding #logic: Encoding the Satisfiability of Modal and Description Logics into SAT: The Case Study of K(m)/ALC (RS, MV), pp. 130–135.
SAT-2006-SheiniS #modulo theories: From Propositional Satisfiability to Satisfiability Modulo Theories (HMS, KAS), pp. 1–9.
SAT-2006-SheiniS06a #modulo theories: A Progressive Simplifier for Satisfiability Modulo Theories (HMS, KAS), pp. 184–197.
SAT-2006-WatanabeY #analysis #problem: Average-Case Analysis for the MAX-2SAT Problem (OW, MY), pp. 277–282.
PODS-2005-BenediktFG #xpath: XPath satisfiability in the presence of DTDs (MB, WF, FG), pp. 25–36.
PADL-2005-BaileyS #constraints #set #using: Discovery of Minimal Unsatisfiable Subsets of Constraints Using Hitting Set Dualization (JB, PJS), pp. 174–186.
POPL-2005-XieA #detection #fault #scalability #using: Scalable error detection using boolean satisfiability (YX, AA), pp. 351–363.
DAC-2005-BabicBH #performance: Efficient SAT solving: beyond supercubes (DB, JDB, AJH), pp. 744–749.
DAC-2005-GanaiGA #model checking #safety: Beyond safety: customized SAT-based model checking (MKG, AG, PA), pp. 738–743.
DAC-2005-ZhangPHS #abstraction #using: Dynamic abstraction using SAT-based BMC (LZ, MRP, MSH, TS), pp. 754–757.
DATE-2005-ChandrasekarH #fault #generative #incremental #integration #learning #performance #testing: Integration of Learning Techniques into Incremental Satisfiability for Efficient Path-Delay Fault Test Generation (KC, MSH), pp. 1002–1007.
DATE-2005-FuYM: Considering Circuit Observability Don’t Cares in CNF Satisfiability (ZF, YY, SM), pp. 1108–1113.
DATE-2005-LuIPWCC #performance: An Efficient Sequential SAT Solver With Improved Search Strategies (FL, MKI, GP, LCW, KTC, KCC), pp. 1102–1107.
DATE-2005-MishchenkoB #network #optimisation: SAT-Based Complete Don’t-Care Computation for Network Optimization (AM, RKB), pp. 412–417.
DATE-2005-SheiniS #named #pseudo: Pueblo: A Modern Pseudo-Boolean SAT Solver (HMS, KAS), pp. 684–685.
ESOP-2005-NiehrenPS #complexity #type system: Complexity of Subtype Satisfiability over Posets (JN, TP, ZS), pp. 357–373.
TACAS-2005-BozzanoBCJRSS #incremental #linear #logic: An Incremental and Layered Procedure for the Satisfiability of Linear Arithmetic Logic (MB, RB, AC, TAJ, PvR, SS, RS), pp. 317–333.
TACAS-2005-ClarkeKSY #abstraction #named: SATABS: SAT-Based Predicate Abstraction for ANSI-C (EMC, DK, NS, KY), pp. 570–574.
TACAS-2005-GanaiGA #framework #model checking #named #platform #scalability #verification: DiVer: SAT-Based Model Checking Platform for Verifying Large Scale Systems (MKG, AG, PA), pp. 575–580.
SAT-J-2004-ArmandoCGM05 #constraints #difference: A SAT-Based Decision Procedure for the Boolean Combination of Difference Constraints (AA, CC, EG, MM), pp. 16–29.
SAT-J-2004-BerreS05 #contest: Fifty-Five Solvers in Vancouver: The SAT 2004 Competition (DLB, LS), pp. 321–344.
SAT-J-2004-DantsinW05 #algorithm: Derandomization of Schuler’s Algorithm for SAT (ED, AW), pp. 80–88.
SAT-J-2004-GalesiK05 #polynomial #rank: Polynomial Time SAT Decision, Hypergraph Transversals and the Hermitian Rank (NG, OK), pp. 89–104.
SAT-J-2004-GummadiNV05 #algorithm #independence #set #using: Algorithms for Satisfiability Using Independent Sets of Variables (RG, NSN, VR), pp. 133–144.
SAT-J-2004-HeuleDZM05 #implementation #named #performance #reasoning: March_eq: Implementing Additional Reasoning into an Efficient Look-Ahead SAT Solver (MH, MD, JvZ, HvM), pp. 345–359.
SAT-J-2004-JiaMS05: From Spin Glasses to Hard Satisfiable Formulas (HJ, CM, BS), pp. 199–210.
SAT-J-2004-JinS05 #hybrid #named: CirCUs: A Hybrid Satisfiability Solver (HJ, FS), pp. 211–223.
SAT-J-2004-MahajanFM05 #named #performance: Zchaff2004: An Efficient SAT Solver (YSM, ZF, SM), pp. 360–375.
SAT-J-2004-PanV05: Search vs. Symbolic Techniques in Satisfiability Solving (GP, MYV), pp. 235–250.
SAT-J-2004-Sinopalnikov05 #random: Satisfiability Threshold of the Skewed Random k-SAT (DAS), pp. 263–275.
SAT-J-2004-SubbarayanP05 #named #preprocessor: NiVER: Non-increasing Variable Elimination Resolution for Preprocessing SAT Instances (SS, DKP), pp. 276–291.
SAT-J-2004-TangYRM05 #algorithm #analysis #problem #quantifier: Analysis of Search Based Algorithms for Satisfiability of Propositional and Quantified Boolean Formulas Arising from Circuit State Space Diameter Problems (DT, YY, DR, SM), pp. 292–305.
SAT-J-2004-TompkinsH05 #algorithm #implementation #named: UBCSAT: An Implementation and Experimentation Environment for SLS Algorithms for SAT and MAX-SAT (DADT, HHH), pp. 306–320.
CAV-2005-BarrettMS #contest #modulo theories #named: SMT-COMP: Satisfiability Modulo Theories Competition (CWB, LMdM, AS), pp. 20–23.
CAV-2005-BozzanoBCJRRS #modulo theories #performance: Efficient Satisfiability Modulo Theories via Delayed Theory Combination (MB, RB, AC, TAJ, SR, PvR, RS), pp. 335–349.
CAV-2005-TangMGI #model checking #reduction #symmetry: Symmetry Reduction in SAT-Based Model Checking (DT, SM, AG, CNI), pp. 125–138.
CAV-2005-XieA #debugging #detection #named: Saturn: A SAT-Based Tool for Bug Detection (YX, AA), pp. 139–143.
CSL-2005-Tiwari #algebra #approach #constraints: An Algebraic Approach for the Unsatisfiability of Nonlinear Constraints (AT), pp. 248–262.
ICLP-2005-GiunchigliaM #on the #set: On the Relation Between Answer Set and SAT Procedures (or, Between cmodels and smodels) (EG, MM), pp. 37–51.
ICLP-2005-PelovT #induction: Reducing Inductive Definitions to Propositional Satisfiability (NP, ET), pp. 221–234.
SAT-2005-AlsinetMP: Improved Exact Solvers for Weighted Max-SAT (TA, FM, JP), pp. 371–377.
SAT-2005-ArgelichM #problem: Solving Over-Constrained Problems with SAT Technology (JA, FM), pp. 1–15.
SAT-2005-BelovS #logic: Substitutional Definition of Satisfiability in Classical Propositional Logic (AB, ZS), pp. 31–45.
SAT-2005-DantsinW #bound: An Improved Upper Bound for SAT (ED, AW), pp. 400–407.
SAT-2005-DershowitzHN #heuristic: A Clause-Based Heuristic for SAT Solvers (ND, ZH, AN), pp. 46–60.
SAT-2005-DurairajK #constraints #dependence #performance: Variable Ordering for Efficient SAT Search by Analyzing Constraint-Variable Dependencies (VD, PK), pp. 415–422.
SAT-2005-EenB #effectiveness #preprocessor: Effective Preprocessing in SAT Through Variable and Clause Elimination (NE, AB), pp. 61–75.
SAT-2005-HeuleM #bound #linear #programming #random #using: Observed Lower Bounds for Random 3-SAT Phase Transition Density Using Linear Programming (MH, HvM), pp. 122–134.
SAT-2005-KourilF #performance: Resolution Tunnels for Improved SAT Solver Performance (MK, JVF), pp. 143–157.
SAT-2005-Kulikov #automation #generative: Automated Generation of Simplification Rules for SAT and MAXSAT (ASK), pp. 430–436.
SAT-2005-LewisSB: Speedup Techniques Utilized in Modern SAT Solvers (MDTL, TS, BB), pp. 437–443.
SAT-2005-LiffitonS #on the: On Finding All Minimally Unsatisfiable Subformulas (MHL, KAS), pp. 173–186.
SAT-2005-LiH: Diversification and Determinism in Local Search for Satisfiability (CML, WH), pp. 158–172.
SAT-2005-LingSB #logic #quantifier #synthesis #using: FPGA Logic Synthesis Using Quantified Boolean Satisfiability (ACL, DPS, SDB), pp. 444–450.
SAT-2005-MaarenN: Sums of Squares, Satisfiability and Maximum Satisfiability (HvM, LvN), pp. 294–308.
SAT-2005-MeierS #algebra #benchmark #metric #problem #set: A New Set of Algebraic Benchmark Problems for SAT Solvers (AM, VS), pp. 459–466.
SAT-2005-MneimnehLASS #algorithm #bound: A Branch-and-Bound Algorithm for Extracting Smallest Minimal Unsatisfiable Formulas (MNM, IL, ZSA, JPMS, KAS), pp. 467–474.
SAT-2005-Rolf: Derandomization of PPSZ for Unique- k-SAT (DR), pp. 216–225.
SAT-2005-SeitzAO #behaviour #random: Threshold Behaviour of WalkSAT and Focused Metropolis Search on Random 3-Satisfiability (SS, MA, PO), pp. 475–481.
SAT-2005-SheiniS #integer #linear #logic #scalability: A Scalable Method for Solving Satisfiability of Integer Linear Arithmetic Logic (HMS, KAS), pp. 241–256.
SAT-2005-SinzD #named #visualisation: DPvis — A Tool to Visualize the Structure of SAT Instances (CS, EMD), pp. 257–268.
SAT-2005-Wahlstrom #performance: Faster Exact Solving of SAT Formulae with a Low Number of Occurrences per Variable (MW), pp. 309–323.
SAT-2005-Zarpas #benchmark #bound #metric #model checking: Benchmarking SAT Solvers for Bounded Model Checking (EZ), pp. 340–354.
VMCAI-2005-ShenQL #incremental: Minimizing Counterexample with Unit Core Extraction and Incremental SAT (SS, YQ, SL), pp. 298–312.
PODS-2004-Calders #complexity: Computational Complexity of Itemset Frequency Satisfiability (TC), pp. 143–154.
VLDB-2004-LakshmananRWZ #on the #query #testing: On Testing Satisfiability of Tree Pattern Queries (LVSL, GR, WHW, Z(Z), pp. 120–131.
ICALP-2004-AlekhnovichHI #algorithm #bound #exponential: Exponential Lower Bounds for the Running Time of DPLL Algorithms on Satisfiable Formulas (MA, EAH, DI), pp. 84–96.
ICALP-2004-MelkebeekR #bound: A Time Lower Bound for Satisfiability (DvM, RR), pp. 971–982.
CAiSE-2004-SebastianiGM #low cost #modelling: Simple and Minimum-Cost Satisfiability for Goal Models (RS, PG, JM), pp. 20–35.
KR-2004-SerafiniR: Satisfiability for Propositional Contexts (LS, FR), pp. 369–376.
PPDP-2004-CamaraoFV #constraints: Constraint-set satisfiability for overloading (CC, LF, CV), pp. 67–77.
SAC-2004-BoughaciD #metaheuristic #optimisation #problem #using: Solving weighted Max-Sat optimization problems using a Taboo Scatter Search metaheuristic (DB, HD), pp. 35–36.
DAC-2004-ChauhanCK #algorithm #simulation: A SAT-based algorithm for reparameterization in symbolic simulation (PC, EMC, DK), pp. 524–529.
DAC-2004-OhMASM #named: AMUSE: a minimally-unsatisfiable subformula extractor (YO, MNM, ZSA, KAS, ILM), pp. 518–523.
DAC-2004-WangJHS #bound #model checking: Refining the SAT decision ordering for bounded model checking (CW, HJ, GDH, FS), pp. 535–538.
DATE-v1-2004-LiHS #novel #performance: A Novel SAT All-Solutions Solver for Efficient Preimage Computation (BL, MSH, SS), pp. 272–279.
DATE-v1-2004-SafarpourVDL: Managing Don’t Cares in Boolean Satisfiability (SS, AGV, RD, JL), pp. 260–265.
DATE-v1-2004-WedlerSK #reasoning: Arithmetic Reasoning in DPLL-Based SAT Solving (MW, DS, WK), pp. 30–35.
CAV-2004-JinAS #bound #model checking #named #towards: CirCUs: A Satisfiability Solver Geared towards Bounded Model Checking (HJ, MA, FS), pp. 519–522.
CAV-2004-KroeningOSS: Abstraction-Based Satisfiability Solving of Presburger Arithmetic (DK, JO, SAS, OS), pp. 308–320.
CSL-2004-Atserias #complexity #random: Notions of Average-Case Complexity for Random 3-SAT (AA), pp. 1–5.
SAT-2004-ArmandoCGM #constraints #difference: A SAT-based Decision Procedure for the Boolean Combination of Difference Constraints (AA, CC, EG, MM), pp. 166–173.
SAT-2004-DantsinW #algorithm: Derandomization of Schuler’s Algorithm for SAT (ED, AW), pp. 69–75.
SAT-2004-GalesiK #polynomial #rank: Polynomial Time SAT Decision, Hypergraph Transversals and the Hermitian Rank (NG, OK), pp. 76–85.
SAT-2004-GummadiNV #algorithm #independence #set #using: Algorithms for Satisfiability using Independent Sets of Variables (RG, NSN, VR), pp. 56–63.
SAT-2004-HooryS: Computing Unsatisfiable k-SAT Instances with Few Occurrences per Variable (SH, SS), pp. 86–95.
SAT-2004-JiaMS: From Spin Glasses to Hard Satisfiable Formulas (HJ, CM, BS), pp. 12–19.
SAT-2004-JinS #hybrid #named: CirCUs: A Hybrid Satisfiability Solver (HJ, FS), pp. 47–55.
SAT-2004-LewisSB #detection: Early Conflict Detection Based BCP for SAT Solving (MDTL, TS, BB), pp. 29–36.
SAT-2004-ManquinhoM #bound #optimisation #pseudo #using: Using Lower-Bound Estimates in SAT-Based Pseudo-Boolean Optimization (VMM, JPMS), pp. 120–126.
SAT-2004-PanV: Search vs. Symbolic Techniques in Satisfiability Solving (GP, MYV), pp. 137–146.
SAT-2004-TangYRM #algorithm #analysis #problem #quantifier: Analysis of Search Based Algorithms for Satisfiability of Quantified Boolean Formulas Arising from Circuit State Space Diameter Problems (DT, YY, DR, SM), pp. 214–223.
SAT-2004-TompkinsH #algorithm #implementation #named: UBCSAT: An Implementation and Experimentation Environment for SLS Algorithms for SAT & MAX-SAT (DADT, HHH), pp. 37–46.
SAT-2004-Velev #encoding #performance: Encoding Global Unobservability for Efficient Translation to SAT (MNV), pp. 197–204.
SAT-2004-ZhangLS: A SAT Based Scheduler for Tournament Schedules (HZ, DL, HS), pp. 191–196.
FME-2003-ArmandoCG #analysis #graph #model checking #protocol #security #using: SAT-Based Model-Checking of Security Protocols Using Planning Graph Analysis (AA, LC, PG), pp. 875–893.
PPDP-2003-BandaSW #set: Finding all minimal unsatisfiable subsets (MJGdlB, PJS, JW), pp. 32–43.
ASE-2003-ShlyakhterSJST #debugging #declarative #modelling #using: Debugging Overconstrained Declarative Models Using Unsatisfiable Cores (IS, RS, DJ, MS, MT), pp. 94–105.
DAC-2003-AloulMS #named #performance #symmetry: Shatter: efficient symmetry-breaking for boolean satisfiability (FAA, ILM, KAS), pp. 836–839.
DAC-2003-DamianoK: Checking satisfiability of a conjunction of BDDs (RFD, JHK), pp. 818–823.
DAC-2003-GuptaGWYA #bound #learning #model checking: Learning from BDDs in SAT-based bounded model checking (AG, MKG, CW, ZY, PA), pp. 824–829.
DAC-2003-KangP #bound #model checking: SAT-based unbounded symbolic model checking (HJK, ICP), pp. 840–843.
DAC-2003-SeshiaLB #hybrid #logic: A hybrid SAT-based decision procedure for separation logic with uninterpreted functions (SAS, SKL, REB), pp. 425–430.
DAC-2003-Tahoori #testing #using: Using satisfiability in application-dependent testing of FPGA interconnects (MBT), pp. 678–681.
DATE-2003-CabodiNQ #approximate #bound #model checking #traversal: Improving SAT-Based Bounded Model Checking by Means of BDD-Based Approximate Traversals (GC, SN, SQ), pp. 10898–10905.
DATE-2003-GoldbergN #proving #verification: Verification of Proofs of Unsatisfiability for CNF Formulas (EIG, YN), pp. 10886–10891.
DATE-2003-HaubeltTFM #synthesis: SAT-Based Techniques in System Synthesis (CH, JT, RF, BM), pp. 11168–11169.
DATE-2003-LuWCH #correlation #learning: A Circuit SAT Solver With Signal Correlation Guided Learning (FL, LCW, KTC, RCYH), pp. 10892–10897.
DATE-2003-ZhangM #implementation #independence #using #validation: Validating SAT Solvers Using an Independent Resolution-Based Checker: Practical Implementations and Other Applications (LZ, SM), pp. 10880–10885.
STOC-2003-AchlioptasP #random: The threshold for random k-SAT is 2k (ln 2 — O(k)) (DA, YP), pp. 223–231.
CADE-2003-Clarke #abstraction #model checking #refinement: SAT-Based Counterexample Guided Abstraction Refinement in Model Checking (EMC), p. 1.
CAV-2003-GuptaGWYA #abstraction: Abstraction and BDDs Complement SAT-Based BMC in DiVer (AG, MKG, CW, ZY, PA), pp. 206–209.
CAV-2003-McMillan #model checking: Interpolation and SAT-Based Model Checking (KLM), pp. 1–13.
LICS-2003-Drimmelen #logic: Satisfiability in Alternating-time Temporal Logic (GvD), pp. 208–217.
SAT-2003-ArmandoC #analysis #protocol #security: Abstraction-Driven SAT-based Analysis of Security Protocols (AA, LC), pp. 257–271.
SAT-2003-BaumerS #algorithm #independence #probability: Improving a Probabilistic 3-SAT Algorithm by Dynamic Search and Independent Clause Pairs (SB, RS), pp. 150–161.
SAT-2003-BerreS #contest: The Essentials of the SAT 2003 Competition (DLB, LS), pp. 452–467.
SAT-2003-BerreST #challenge #evaluation: Challenges in the QBF Arena: the SAT’03 Evaluation of QBF Solvers (DLB, LS, AT), pp. 468–485.
SAT-2003-BessiereHW #consistency: Local Consistencies in SAT (CB, EH, TW), pp. 299–314.
SAT-2003-BjesseKDSZ: Guiding SAT Diagnosis with Tree Decompositions (PB, JHK, RFD, TS, YZ), pp. 315–329.
SAT-2003-BraunsteinZ #overview #random: Survey and Belief Propagation on Random K-SAT (AB, RZ), pp. 519–528.
SAT-2003-BroeringL #algorithm: Width-Based Algorithms for SAT and CIRCUIT-SAT: (EB, SVL), pp. 162–171.
SAT-2003-Bruni #fault #scalability #set: Solving Error Correction for Large Data Sets by Means of a SAT Solver (RB), pp. 229–241.
SAT-2003-Chen #algorithm: An Algorithm for SAT Above the Threshold (HC), pp. 14–24.
SAT-2003-ClarkeTVW #abstraction #hardware #verification: SAT Based Predicate Abstraction for Hardware Verification (EMC, MT, HV, DW), pp. 78–92.
SAT-2003-DequenD #named #performance #random: kcnfs: An Efficient Solver for Random k-SAT Formulae (GD, OD), pp. 486–501.
SAT-2003-DransfieldMT: Satisfiability and Computing van der Waerden Numbers (MRD, VWM, MT), pp. 1–13.
SAT-2003-FrancoKSWWDV #named: SBSAT: a State-Based, BDD-Based Satisfiability Solver (JVF, MK, JSS, JW, SW, MD, WMV), pp. 398–410.
SAT-2003-LiSB #effectiveness #performance #using: A Local Search SAT Solver Using an Effective Switching Strategy and an Efficient Unit Propagation (XYL, MFMS, FB), pp. 53–68.
SAT-2003-Parisi #approach #on the #probability #problem #random: On the Probabilistic Approach to the Random Satisfiability Problem (GP), pp. 203–213.
SAT-2003-PorschenRS #algorithm #linear #problem: Linear Time Algorithms for Some Not-All-Equal Satisfiability Problems (SP, BR, ES), pp. 172–187.
SAT-2003-Pretolani #problem #reduction: Hypergraph Reductions and Satisfiability Problems (DP), pp. 383–397.
SAT-2003-SemerjianM #case study #physics #problem #random: A Study of Pure Random Walk on Random Satisfiability Problems with “Physical” Methods (GS, RM), pp. 120–134.
SAT-2003-Szeider #on the #parametricity: On Fixed-Parameter Tractable Parameterizations of SAT (SS), pp. 188–202.
SAT-2003-ZhangM #algorithm #case study #implementation #performance: Cache Performance of SAT Solvers: a Case Study for Efficient Implementation of Algorithms (LZ, SM), pp. 287–298.
DAC-2002-AloulRMS #symmetry: Solving difficult SAT instances in the presence of symmetry (FAA, AR, ILM, KAS), pp. 731–736.
DAC-2002-CabodiCQ #bound #model checking #question: Can BDDs compete with SAT solvers on bounded model checking? (GC, PC, SQ), pp. 117–122.
DAC-2002-GanaiAGZM #algorithm: Combining strengths of circuit-based and CNF-based algorithms for a high-performance SAT solver (MKG, PA, AG, LZ, SM), pp. 747–750.
DAC-2002-PilarskiH: SAT with partial clauses and back-leaps (SP, GH), pp. 743–746.
DATE-2002-AloulMS #search-based #using: Search-Based SAT Using Zero-Suppressed BDDs (FAA, MNM, KAS), p. 1082.
DATE-2002-GoldbergPB #algorithm #problem #symmetry #using: Using Problem Symmetry in Search Based Satisfiability Algorithms (EIG, MRP, RKB), pp. 134–141.
DATE-2002-PilarskiH: Speeding up SAT for EDA (SP, GH), p. 1081.
DATE-2002-SkliarovaF #configuration management #hardware #using: A SAT Solver Using Software and Reconfigurable Hardware (IS, AdBF), p. 1094.
CADE-2002-AudemardBCKS #approach #linear: A SAT Based Approach for Solving Formulas over Boolean and Linear Mathematical Propositions (GA, PB, AC, AK, RS), pp. 195–210.
CADE-2002-Goldberg #testing: Testing Satisfiability of CNF Formulas by Computing a Stable Set of Points (EG), pp. 161–180.
CADE-2002-ZhangM #performance: The Quest for Efficient Boolean Satisfiability Solvers (LZ, SM), pp. 295–313.
CAV-2002-BarrettDS #first-order #incremental: Checking Satisfiability of First-Order Formulas by Incremental Translation to SAT (CWB, DLD, AS), pp. 236–249.
CAV-2002-ClarkeGKS #abstraction #machine learning #using: SAT Based Abstraction-Refinement Using ILP and Machine Learning Techniques (EMC, AG, JHK, OS), pp. 265–279.
CAV-2002-McMillan #bound #model checking: Applying SAT Methods in Unbounded Symbolic Model Checking (KLM), pp. 250–264.
CAV-2002-StrichmanSB: Deciding Separation Formulas with SAT (OS, SAS, REB), pp. 209–222.
CAV-2002-ZhangM #performance: The Quest for Efficient Boolean Satisfiability Solvers (LZ, SM), pp. 17–36.
LICS-2002-Atserias #random: Unsatisfiable Random Formulas Are Hard to Certify (AA), pp. 325–334.
LICS-2002-Bars #logic: The 0-1 law fails for frame satisfiability of propositional modal logic (JMLB), pp. 225–234.
SAT-2002-AloulRMS #symmetry: Solving difficult SAT instances in the presence of symmetry (FAA, AR, IM, KS), p. 23.
SAT-2002-BrglezLS #algorithm #benchmark #metric #testing: The role of a skeptic agent in testing and benchmarking of SAT algorithms (FB, XYL, MFS), p. 13.
SAT-2002-Bruni: Exact selection of minimal unsatisfiable subformulae for special classes of propositional formulae (RB), p. 22.
SAT-2002-BueningX #complexity #morphism: The complexity of homomorphisms and renamings of minimal unsatisfiable formulas (HKB, DX), p. 9.
SAT-2002-Clarke #abstraction #logic #model checking #refinement: SAT based abstraction refinement in temporal logic model checking (EC), p. 26.
SAT-2002-CreignouD #problem #random: Random generalized satisfiability problems (NC, HD), p. 2.
SAT-2002-DrakeFW: Adding resolution to the DPLL procedure for satisfiability (LD, AF, TW), p. 46.
SAT-2002-DuboisD #random: Renormalization as a function of clause lengths for solving random k-SAT formulae (OD, GD), p. 15.
SAT-2002-FormanS #named #parallel #random: NAGSAT: A randomized, complete, parallel solver for 3-SAT (SF, AMS), p. 45.
SAT-2002-FriezeW #named: k-SAT: A tight threshold for moderately growing k (AF, NW), p. 6.
SAT-2002-Gelder #reasoning #towards: Toward leaner binary-clause reasoning in a satisfiability solver (AVG), p. 16.
SAT-2002-GentP #encoding #problem: SAT encodings of the stable marriage problem with ties and incomplete lists (IG, PP), p. 19.
SAT-2002-Goldberg #testing: Testing satisfiability of CNF formulas by computing a stable set of points (EG), p. 12.
SAT-2002-HirschK #named: UnitWalk: A new SAT solver that uses local search guided by unit clause elimination (EH, AK), p. 38.
SAT-2002-Hoos #algorithm #modelling: SLS algorithms for SAT: irregular instances, search stagnation, and mixture models (HH), p. 41.
SAT-2002-KaporisKL #algorithm #analysis #probability: The Probabilistic Analysis of a Greedy Satisfiability Algorithm (ACK, LMK, EGL), p. 5.
SAT-2002-Kullmann #adaptation #branch #database #encryption #normalisation #random #standard #towards #using: Towards an adaptive density based branching rule for SAT solvers, using a database for mixed random conjunctive normal forms built upon the Advanced Encryption Standard (AES) (OK), p. 8.
SAT-2002-Kusper #linear #problem: Solving the resolution-free SAT problem by hyper-unit propagation in linear time (GK), p. 32.
SAT-2002-LiB #empirical: An empirical measure for characterizing 3-SAT (CML, HB), p. 35.
SAT-2002-LynceM #backtracking #data type #performance: Efficient data structures for backtrack search SAT solvers (IL, JMS), p. 20.
SAT-2002-LynceM1 #algorithm #backtracking #strict: Complete unrestricted backtracking algorithms for satisfiability (IL, JMS), p. 29.
SAT-2002-MalerMNA #difference #logic: A satisfiability checker for difference logic (OM, MM, PN, EA), p. 27.
SAT-2002-Marques-Silva #reasoning: Hypothetical reasoning in propositional satisfiability (JMS), p. 14.
SAT-2002-MonassonC #algorithm #analysis #exponential #random #scalability: Restart method and exponential acceleration of random 3-SAT instances resolutions: A large deviation analysis of the Davis-Putnam-Loveland-Logemann algorithm (RM, SC), p. 11.
SAT-2002-MotterM #on the #performance #proving: On proof systems behind efficient SAT solvers (DM, IM), p. 31.
SAT-2002-PorschenRS #decidability: X3SAT is decidable in time O(2n/5) (SP, BR, ES), p. 10.
SAT-2002-PrestwichB #approach #optimisation #query: A SAT approach to query optimization in mediator systems (SP, SB), p. 33.
SAT-2002-Roli #parallel: Impact of structure on parallel local search for SAT (AR), p. 24.
SAT-2002-RuessM: Lemmas on demand for Satisfiability solvers (HR, LdM), p. 17.
SAT-2002-Schoening #bound: New worst case bounds on k-SAT (US), p. 1.
SAT-2002-TakenakaH #algorithm #problem: An analog algorithm for the satisfiability problem (YT, AH), p. 40.
SAT-2002-Zhang #generative: Generating college conference basketball schedules by a SAT solver (HZ), p. 39.
VMCAI-2002-CimattiPRS #encoding #ltl #model checking: Improving the Encoding of LTL Model Checking into SAT (AC, MP, MR, RS), pp. 196–207.
ICALP-2001-FriedmanG #random: Recognizing More Unsatisfiable Random 3-SAT Instances Efficiently (JF, AG), pp. 310–321.
SAC-2001-Zhang #automation #symmetry: Automatic symmetry breaking method combined with SAT (JZ0), pp. 17–21.
DAC-2001-GuptaGYA #detection #image: Dynamic Detection and Removal of Inactive Clauses in SAT with Application in Image Computation (AG, AG, ZY, PA), pp. 536–541.
DAC-2001-MajumdarW #combinator #using: Watermarking of SAT using Combinatorial Isolation Lemmas (RM, JLW), pp. 480–485.
DAC-2001-MoskewiczMZZM #named #performance: Chaff: Engineering an Efficient SAT Solver (MWM, CFM, YZ, LZ, SM), pp. 530–535.
DAC-2001-VelevB #effectiveness #using #verification: Effective Use of Boolean Satisfiability Procedures in the Formal Verification of Superscalar and VLIW Microprocessors (MNV, REB), pp. 226–231.
DAC-2001-WhittemoreKS #incremental #named: SATIRE: A New Incremental Satisfiability Engine (JW, JK, KAS), pp. 542–545.
DATE-2001-GoldbergPB #equivalence #using: Using SAT for combinational equivalence checking (EIG, MRP, RKB), pp. 114–121.
DATE-2001-NamSR #approach #incremental: A boolean satisfiability-based incremental rerouting approach with application to FPGAs (GJN, KAS, RAR), pp. 560–565.
DATE-2001-RedaS #diagrams #equivalence #using: Combinational equivalence checking using Boolean satisfiability and binary decision diagrams (SR, AS), pp. 122–126.
DATE-2001-ZengKC #approach #named: LPSAT: a unified approach to RTL satisfiability (ZZ, PK, MJC), pp. 398–402.
ESOP-2001-CadoliS #compilation #problem #specification: Compiling Problem Specifications into SAT (MC, AS), pp. 387–401.
TACAS-2001-WilliamsAH #diagrams #using: Satisfiability Checking Using Boolean Expression Diagrams (PFW, HRA, HH), pp. 39–51.
CAV-2001-BjesseLM #debugging #using: Finding Bugs in an α Microprocessor Using Satisfiability Solvers (PB, TL, AM), pp. 454–464.
IJCAR-2001-BaaderT #approach #automaton: The Inverse Method Implements the Automata Approach for Modal Satisfiability (FB, ST), pp. 92–106.
IJCAR-2001-GiunchigliaMTZ #heuristic #optimisation: Evaluating Search Heuristics and Optimization Techniques in Propositional Satisfiability (EG, MM, AT, DZ), pp. 347–363.
IJCAR-2001-GiunchigliaNT #named #quantifier: QUBE: A System for Deciding Quantified Boolean Formulas Satisfiability (EG, MN, AT), pp. 364–369.
LICS-2001-LangeS #game studies #logic: Focus Games for Satisfiability and Completeness of Temporal Logic (ML, CS), pp. 357–365.
SAT-2001-AmirM #composition #problem #using: Solving Satisfiability using Decomposition and the Most Constrained Subproblem (EA, SM), pp. 329–343.
SAT-2001-BejarCFMG #logic: Extending the Reach of SAT with Many-Valued Logics (RB, AC, CF, FM, CPG), pp. 392–407.
SAT-2001-BruniS #maintenance: Restoring Satisfiability or Maintaining Unsatisfiability by finding small Unsatisfiable Subformulae (RB, AS), pp. 162–173.
SAT-2001-BuningZ: Satisfiable Formulas Closed Under Replacement (HKB, XZ), pp. 48–58.
SAT-2001-CoccoM #analysis #backtracking #physics #random #statistics: Statistical physics analysis of the backtrack resolution of random 3-SAT instances (SC, RM), pp. 36–47.
SAT-2001-Gelder: Combining Preorder and Postorder Resolution in a Satisfiability Solver (AVG), pp. 115–128.
SAT-2001-GiunchigliaNTV #library #performance #towards: Towards an Efficient Library for SAT: a Manifesto (EG, MN, AT, MYV), pp. 290–310.
SAT-2001-Goldberg #proving: Proving unsatisfiability of CNFs locally (EG), pp. 96–114.
SAT-2001-KaporisKSVZ #revisited: The unsatisfiability threshold revisited (ACK, LMK, YCS, MV, MZ), pp. 81–95.
SAT-2001-KautzRAGSS #problem: Balance and Filtering in Structured Satisfiable Problems (HAK, YR, DA, CPG, BS, MES), pp. 2–18.
SAT-2001-Kullmann #on the #using: On the use of autarkies for satisfiability decision (OK), pp. 231–253.
SAT-2001-LagoudakisL #branch #learning: Learning to Select Branching Rules in the DPLL Procedure for Satisfiability (MGL, MLL), pp. 344–359.
SAT-2001-LynceBM #algorithm #probability: Stochastic Systematic Search Algorithms for Satisfiability (IL, LB, JMS), pp. 190–204.
SAT-2001-Morrisette #algorithm #effectiveness: The Unreasonable Effectiveness of Alternation-Based Satisfiability Algorithms (TM), pp. 254–268.
SAT-2001-NuallainRB #behaviour #predict: Ensemble-based prediction of SAT search behaviour (BÓN, MdR, JvB), pp. 278–289.
SAT-2001-RanderathSBHKMSC #graph #problem: A Satisfiability Formulation of Problems on Level Graphs (BR, ES, EB, PLH, AK, KM, BS, OC), pp. 269–277.
SAT-2001-SimonC #framework #named: SatEx: A Web-based Framework for SAT Experimentation (LS, PC), pp. 129–149.
SAT-2001-Subramani: A polyhedral projection procedure for Q2SAT (KS), pp. 369–375.
ICALP-2000-DantsinGHS #algorithm: Deterministic Algorithms for k-SAT Based on Covering Codes and Local Search (ED, AG, EAH, US), pp. 236–247.
KR-2000-GinsbergP #algorithm #finite #quantifier: Satisfiability Algorithms and Finite Quantification (MLG, AJP), pp. 690–701.
KR-2000-Giunchiglia #concurrent #constraints #nondeterminism: Planning as Satisfiability with Expressive Action Languages: Concurrency, Constraints and Nondeterminism (EG), pp. 657–666.
SAC-2000-RossiMK #adaptation #algorithm #problem: An Adaptive Evolutionary Algorithm for the Satisfiability Problem (CR, EM, JNK), pp. 463–469.
DAC-2000-SilvaS #automation #design: Boolean satisfiability in electronic design automation (JPMS, KAS), pp. 675–680.
DATE-2000-KallaZCH #framework #paradigm #recursion #using: A BDD-Based Satisfiability Infrastructure Using the Unate Recursive Paradigm (PK, ZZ, MJC, CH), pp. 232–236.
DATE-2000-KimWSS #fault #incremental #on the #testing: On Applying Incremental Satisfiability to Delay Fault Testing (JK, JW, KAS, JPMS), pp. 380–384.
DATE-2000-ManquinhoS #algorithm #on the #using: On Using Satisfiability-Based Pruning Techniques in Covering Algorithms (VMM, JPMS), pp. 356–363.
DATE-2000-SakallahAS #case study #heuristic: An Experimental Study of Satisfiability Search Heuristics (KAS, FAA, JPMS), p. 745.
STOC-2000-Achlioptas #bound #random: Setting 2 variables at a time yields a new lower bound for random 3-SAT (DA), pp. 28–37.
STOC-2000-CzumajS #algorithm #approach #problem #scheduling: A new algorithm approach to the general Lovász local lemma with applications to scheduling and satisfiability problems (AC, CS), pp. 38–47.
STOC-2000-Gutierrez #equation: Satisfiability of equations in free groups is in PSPACE (CG), pp. 21–27.
CAV-2000-BryantV #constraints #transitive: Boolean Satisfiability with Transitivity Constraints (REB, MNV), pp. 85–98.
CAV-2000-Marques-SilvaS #algorithm #automation #design #tutorial: Invited Tutorial: Boolean Satisfiability Algorithms and Applications in Electronic Design Automation (JPMS, KAS), p. 3.
CAV-2000-Shtrichman #bound #model checking: Tuning SAT Checkers for Bounded Model Checking (OS), pp. 480–494.
CAV-2000-WilliamsBCG #diagrams #model checking #performance: Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking (PFW, AB, EMC, AG), pp. 124–138.
CL-2000-AudemardBS #named: AVAL: An Enumerative Method for SAT (GA, BB, PS), pp. 373–383.
CL-2000-ErdemLW: Wire Routing and Satisfiability Planning (EE, VL, MDFW), pp. 822–836.
CL-2000-JunttilaN #performance #towards: Towards an Efficient Tableau Method for Boolean Circuit Satisfiability Checking (TAJ, IN), pp. 553–567.
CSL-2000-Hemaspaandra #linear: Modal Satisfiability Is in Deterministic Linear Space (EH), pp. 332–342.
LICS-2000-Selman #challenge #problem #testing: Satisfiability Testing: Recent Developments and Challenge Problems (BS), p. 178.
ICALP-1999-NiedermeierR #bound: New Upper Bounds for MaxSat (RN, PR), pp. 575–584.
RTA-1999-CaronSTT #quantifier: Deciding the Satisfiability of Quantifier free Formulae on One-Step Rewriting (ACC, FS, ST, MT), pp. 103–117.
DAC-1999-AbramoviciSS #configuration management #hardware #using: A Massively-Parallel Easily-Scalable Satisfiability Solver Using Reconfigurable Hardware (MA, JTdS, DGS), pp. 684–690.
DAC-1999-BiereCCFZ #model checking #using: Symbolic Model Checking Using SAT Procedures instead of BDDs (AB, AC, EMC, MF, YZ), pp. 317–320.
DATE-1999-Marques-SilvaG #equivalence #learning #recursion #using: Combinational Equivalence Checking Using Satisfiability and Recursive Learning (JPMS, TG), pp. 145–149.
DATE-1999-SilvaSM #algorithm: Algorithms for Solving Boolean Satisfiability in Combinational Circuits (LGeS, LMS, JPMS), pp. 526–530.
STOC-1999-Plandowski #equation #word: Satisfiability of Word Equations with Constants is in NEXPTIME (WP), pp. 721–725.
KR-1998-McCainT: Satisfiability planning with Causal Theories (NM, HT), pp. 212–223.
SAC-1998-Nemer-PreeceW #algorithm #parallel #problem #search-based: Parallel genetic algorithm to solve the satisfiability problem (NNP, RWW), pp. 23–28.
DAC-1998-FallahDK #functional #generative #linear #modelling #programming #using: Functional Vector Generation for HDL Models Using Linear Programming and 3-Satisfiability (FF, SD, KK), pp. 528–533.
DAC-1998-ZhongAMM #case study #configuration management #problem #using: Using Reconfigurable Computing Techniques to Accelerate Problems in the CAD Domain: A Case Study with Boolean Satisfiability (PZ, PA, SM, MM), pp. 194–199.
DATE-1998-RingeLB #using #verification: Path Verification Using Boolean Satisfiability (MR, TL, EB), pp. 965–966.
STOC-1998-BeameKPS #complexity #on the #proving #random: On the Complexity of Unsatisfiability Proofs for Random k-CNF Formulas (PB, RMK, TP, MES), pp. 561–571.
STOC-1998-Freedman: K-sat on Groups and Undecidability (MHF), pp. 572–576.
CADE-1998-MazureSG #framework #platform: System Description: CRIL Platform for SAT (BM, LS, ÉG), pp. 124–128.
CSL-1998-Sadowski #algorithm #on the: On an Optimal Deterministic Algorithm for SAT (ZS), pp. 179–187.
KR-1996-GiunchigliaS: A SAT-based Decision Procedure for ALC (FG, RS), pp. 304–314.
SAC-1996-Hartley #problem: Steiner systems and the Boolean satisfiability problem (SJH), pp. 277–281.
DAC-1996-ChenG #fault #generative: A Satisfiability-Based Test Generator for Path Delay Faults in Combinational Circuts (CAC, SKG), pp. 209–214.
STOC-1996-CleggEI #algorithm #proving #using: Using the Groebner Basis Algorithm to Find Proofs of Unsatisfiability (MC, JE, RI), pp. 174–183.
CADE-1996-ParkG #clustering #scalability #testing: Partitioning Methods for Satisfiability Testing on Large Formulas (TJP, AVG), pp. 748–762.
PDP-1995-AlbertiBCGP #problem: A neural circuit for the maximum 2-satisfiability problem (MAA, AB, PC, GG, RP), pp. 319–323.
ICLP-1995-FormicaMT #database #object-oriented #proving #theorem proving: A Theorem Prover for Checking Satisfiability of Object-Oriented Database Schemas (AF, MM, RT), p. 819.
PODS-1994-MumickS: Universal Finiteness and Satisfiability (ISM, OS), pp. 190–200.
STOC-1994-GoemansW #algorithm #approximate: .879-approximation algorithms for MAX CUT and MAX 2SAT (MXG, DPW), pp. 422–431.
PODS-1993-LevyMSS #datalog #equivalence: Equivalence, Query-Reachability, and Satisfiability in Datalog Extensions (AYL, ISM, YS, OS), pp. 109–122.
RTA-1993-Fernandez #problem: AC Complement Problems: Satisfiability and Negation Elimination (MF), pp. 358–373.
CSL-1992-Creignou #linear #problem #proving: The Class of Problems that are Linear Equivalent to Satisfiability or a Uniform Method for Proving NP-Completeness (NC), pp. 115–133.
CSL-1992-Schiermeyer: Solving 3-Satisfiability in Less Then 1, 579n Steps (IS), pp. 379–394.
ICALP-1991-JouannaudO #decidability: Satisfiability of Systems of Ordinal Notations with the Subterm Property is Decidable (JPJ, MO), pp. 455–468.
KR-1991-Baalen #automation #design: The Completeness of DRAT, A Technique for Automatic Design of Satisfiability Procedures (JVB), pp. 514–525.
VLDB-1987-LenzeriniN #constraints #dependence #on the: On The Satisfiability of Dependency Constraints in Entity-Relationship Schemata (ML, PN), pp. 147–154.
CSL-1987-BryM #database #deduction #finite #proving: Proving Finite Satisfiability of Deductive Databases (FB, RM), pp. 44–55.
CSL-1987-Speckenmeyer #backtracking #complexity #on the #problem: On the Average Case Complexity of Backtracking for the Exact-Satisfiability Problem (ES), pp. 281–288.
CADE-1986-BuningL #first-order: Classes of First Order Formulas Under Various Satisfiability Definitions (HKB, TL), pp. 553–563.
CADE-1984-Gelder #calculus: A Satisfiability Tester for Non-Clausal Propositional Calculus (AVG), pp. 101–112.
STOC-1978-Schaefer #complexity #problem: The Complexity of Satisfiability Problems (TJS), pp. 216–226.