BibSLEIGH
BibSLEIGH corpus
BibSLEIGH tags
BibSLEIGH bundles
BibSLEIGH people
EDIT!
CC-BY
Open Knowledge
XHTML 1.0 W3C Rec
CSS 2.1 W3C CanRec
email twitter
satisfiability
?fullname?SAT?
?longname?SAT (Satisfiability)?
Google satisfiability

Tag #satisfiability

717 papers:

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

Bibliography of Software Language Engineering in Generated Hypertext (BibSLEIGH) is created and maintained by Dr. Vadim Zaytsev.
Hosted as a part of SLEBOK on GitHub.