Author name cluster

Allen Van Gelder

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

16 papers

2 author rows

AIJ Journal 2016 Journal Article

The QBF Gallery: Behind the scenes

Florian Lonsing
Martina Seidl
Allen Van Gelder

Over the last few years, much progress has been made in the theory and practice of solving quantified Boolean formulas (QBF). Novel solvers have been presented that either successfully enhance established techniques or implement novel solving paradigms. Powerful preprocessors have been realized that tune the encoding of a formula to make it easier to solve. Frameworks for certification and solution extraction emerged that allow for a detailed interpretation of a QBF solver's results, and new types of QBF encodings were presented for various application problems. To capture these developments the QBF Gallery was established in 2013. The QBF Gallery aims at providing a forum to assess QBF tools and to collect new, expressive benchmarks that allow for documenting the status quo and that indicate promising research directions. These benchmarks became the basis for the experiments conducted in the context of the QBF Gallery 2013 and follow-up evaluations. In this paper, we report on the setup of the QBF Gallery. To this end, we conducted numerous experiments which allowed us not only to assess the quality of the tools, but also the quality of the benchmarks.

Details DOI

SAT Conference 2013 Conference Paper

Efficient Clause Learning for Quantified Boolean Formulas via QBF Pseudo Unit Propagation

Florian Lonsing
Uwe Egly
Allen Van Gelder

Abstract Recent solvers for quantified boolean formulas (QBF) use a clause learning method based on a procedure proposed by Giunchiglia et al. (JAIR 2006), which avoids creating tautological clauses. Recently, an exponential worst case for this procedure has been shown by Van Gelder (CP 2012). That paper introduced QBF Pseudo Unit Propagation (QPUP) for non-tautological clause learning in a limited setting and showed that its worst case is theoretically polynomial, although it might be impractical in a high-performance QBF solver, due to excessive time and space consumption. No implementation was reported. We describe an enhanced version of QPUP learning that is practical to incorporate into high-performance QBF solvers, being compatible with pure-literal rules and dependency schemes. It can be used for proving in a concise format that a QBF formula is either unsatisfiable or satisfiable (working on both proofs in tandem). A lazy version of QPUP permits non-tautological clauses to be learned without actually carrying out resolutions, but this version is unable to produce proofs. Experimental results show that QPUP is somewhat faster than the previous non-tautological clause learning procedure on benchmarks from QBFEVAL-12-SR.

Details

SAT Conference 2012 Conference Paper

Extended Failed-Literal Preprocessing for Quantified Boolean Formulas

Allen Van Gelder
Samuel B. Wood
Florian Lonsing

Abstract ~Building on recent work that adapts failed-literal analysis (FL) to Quantified Boolean Formulas (QBF), this paper introduces extended failed-literal analysis (EFL). FL and EFL are both preprocessing methods that apply a fast, but incomplete reasoning procedure to abstractions of the underlying QBF. EFL extends FL by remembering certain binary clauses that are implied by the same reasoning procedure as FL when it assumes one literal and that implies a second literal. This extension is almost free because the second literals are implied anyway during FL, but compared to analogous techniques for propositional satisfiability, its correctness involves some subtleties. For the first time, application of the universal pure literal rule is considered without also applying the existential pure literal rule. It is shown that using both pure literal rules in EFL is unsound. A modified reasoning procedure for QBF, called Unit-clause Propagation with Universal Pure literals (UPUP) is described and correctness is proved for EFL based on UPUP. Empirical results on the 568-benchmark suite of QBFEVAL-10 are presented.

Details

IJCAI Conference 2011 Conference Paper

A Uniform Approach for Generating Proofs and Strategies for Both True and False QBF Formulas

Alexandra Goultiaeva
Allen Van Gelder
Fahiem Bacchus

Many important problems can be compactly represented as quantified boolean formulas (QBF) and solved by general QBF solvers. To date QBF solvers have mainly focused on determining whether or not the input QBF is true or false. However, additional important information about an application can be gathered from its QBF formulation. In this paper we demonstrate that a circuit-based QBF solver can be exploited to obtain a Q-Resolution proof of the truth or the falsity of a QBF. QBFs have a natural interpretation as a two person game and our main result is to show how, via a simple computation, the moves for the winning player can be computed directly from these proofs. This result shows that the proof is a representation of the winning strategy. In previous approaches the winning strategy has often been represented in a way that makes it hard to verify. In our approach the correctness of the strategy follows directly from the correctness of the proof, which is relatively easy to verify.

PDF Details DOI

SAT Conference 2011 Conference Paper

Careful Ranking of Multiple Solvers with Timeouts and Ties

Allen Van Gelder

Abstract In several fields, Satisfiability being one, there are regular competitions to compare multiple solvers in a common setting. Due to the fact some benchmarks of interest are too difficult for all solvers to complete within available time, time-outs occur and must be considered. Through some strange evolution, time-outs became the only factor that was considered in evaluation. Previous work in SAT 2010 observed that this evaluation method is unreliable and lacks a way to attach statistical significance to its conclusions. However, the proposed alternative was quite complicated and is unlikely to see general use. This paper describes a simpler system, called careful ranking, that permits a measure of statistical significance, and still meets many of the practical requirements of an evaluation system. It incorporates one of the main ideas of the previous work: that outcomes had to be freed of assumptions about timing distributions, so that non-parametric methods were necessary. Unlike the previous work, it incorporates ties. The careful ranking system has several important non-mathematical properties that are desired in an evaluation system: (1) the relative ranking of two solvers cannot be influenced by a third solver; (2) after the competition results are published, a researcher can run a new solver on the same benchmarks and determine where the new solver would have ranked; (3) small timing differences can be ignored; (4) the computations should be easy to understand and reproduce. Voting systems proposed in the literature lack some or all of these properties. A property of careful ranking is that the pairwise ranking might contain cycles. Whether this is a bug or a feature is a matter of opinion. Whether it occurs among leaders in practice is a matter of experience. The system is implemented and has been applied to the SAT 2009 Competition. No cycles occurred among the leaders, but there was a cycle among some low-ranking solvers. To measure robustness, the new and current systems were computed with a range of simulated time-outs, to see how often the top rankings changed. That is, times above the simulated time-out are reclassified as time-outs and the rankings are computed with this data. Careful ranking exhibited many fewer changes.

Details

SAT Conference 2011 Conference Paper

Generalized Conflict-Clause Strengthening for Satisfiability Solvers

Allen Van Gelder

Abstract The dominant propositional satisfiability solvers of the past decade use a technique often called conflict-driven clause learning ( cdcl ), although nomenclature varies. The first half of the decade concentrated on deriving the best clause from the conflict graph that the technique constructs, also with much emphasis on speed. In the second half of the decade efforts have emerged to exploit other information that is derived by the technique as a by-product of generating the conflict graph and learning a conflict clause. The main thrust has been to strengthen the conflict clause by eliminating some of its literals, a process often called conflict-clause minimization, but more accurately described as conflict-clause width reduction, or strengthening. This paper first introduces implication sequences as a general framework to represent all the information derived by the CDCL technique, some of which is not represented in the conflict graph. Then the paper analyzes the structure of this information. The first main result is that any conflict clause that is a logical consequence of an implication sequence may be derived by a particularly simple form of resolution, known as linear input regular. A key observation needed for this result is that the set of clauses in any implication sequence is Horn-renamable. The second main result is that, given an implication sequence, and a clause C derived (learned) from it, it is NP -hard to find a minimum-cardinality subset of C that is also derivable. This is in sharp contrast to the known fact that such a minimum subset can be found quickly if the derivation is restricted to using only clauses in the conflict graph.

Details

SAT Conference 2010 Conference Paper

Zero-One Designs Produce Small Hard SAT Instances

Allen Van Gelder
Ivor T. A. Spence

Abstract Some basics of combinatorial block design are combined with certain constraint satisfaction problems of interest to the satisfiability community. The paper shows how such combinations lead to satisfiability problems, and shows empirically that these are some of the smallest very hard satisfiability problems ever constructed. Partially balanced (0, 1) designs (PB01Ds) are introduced as an extension of balanced incomplete block designs (BIBDs) and (0, 1) designs. Also, (0, 1) difference sets are introduced as an extension of certain cyclical difference sets. Constructions based on (0, 1) difference sets enable generation of PB01Ds over a much wider range of parameters than is possible for BIBDs. Building upon previous work of Spence, it is shown how PB01Ds lead to small, very hard, unsatisfiable formulas. A new three-dimensional form of combinatorial block design is introduced, and leads to small, very hard, satisfiable formulas. The methods are validated on solvers that performed well in the SAT 2009 and earlier competitions.

Details

SAT Conference 2009 Conference Paper

Improved Conflict-Clause Minimization Leads to Improved Propositional Proof Traces

Allen Van Gelder

Abstract Recent empirical results show that recursive, or expensive, conflict-clause minimization is quite beneficial on industrial-style propositional satisfiability problems. The details of this procedure appear to be unpublished to date, but may be found in the open-source code of MiniSat 2. 0, for example. Biere reports that proof traces are made more complicated when conflict-clause minimization is used because some clauses need to be resolved upon multiple times during the minimization procedure as found in MiniSat 2. 0. Biere proposes a proof-trace format in which the set of clause numbers needed for a certain derivation is given, but their order is not specified. This paper presents a new procedure for conflict-clause minimization that is slightly more efficient and, more importantly, discovers a correct order so that each clause used for the derivation is resolved upon only once. This permits the proof trace to specify the order in which to use the clauses, greatly reducing the burden on software that processes the proof trace. The method is validated on the unsatisfiable formulas used for industrial benchmarks in the verified-unsatisfiable track of the SAT 2007 competition.

Details

SAT Conference 2007 Conference Paper

Verifying Propositional Unsatisfiability: Pitfalls to Avoid

Allen Van Gelder

Abstract The importance of producing a certificate of unsatisfiability is increasingly recognized for high performance propositional satisfiability solvers. The leading solvers develop a conflict graph as the basis for deriving (or “learning”) new clauses. Extracting a resolution derivation from the conflict graph is theoretically straightforward, but it turns out to have some surprising practical pitfalls (as well as the unsurprising problem that resolution proofs can be extremely long). These pitfalls are exposed, solutions are presented, and analyzed for worse cases. Dramatic improvements on industrial benchmarks are demonstrated.

Details

SAT Conference 2006 Conference Paper

Preliminary Report on Input Cover Number as a Metric for Propositional Resolution Proofs

Allen Van Gelder

Abstract Input Cover Number (denoted by κ ) is introduced as a metric for difficulty of propositional resolution derivations. If \({\cal F} = \{C_i\}\) is the input CNF formula, then \(\kappa_{{\cal F}}(D)\) is defined as the minimum number of clauses C i needed to form a superset of (i. e. , cover) clause D. Input Cover Number provides a refinement of the clause-width metric in the sense that it applies to families of formulas whose clause width grows with formula size, such as pigeon-hole formulas PHP( m, n ) and GT( n ). Although these two families have much different general-resolution complexities, it is known that both require Θ( n ) clause width (after transforming to 3-CNF). It is shown here that κ is Θ( n ) for pigeon-hole formulas and is Θ(1) for GT( n ) formulas and variants of GT( n ).

Details

LPAR Conference 2005 Conference Paper

Independently Checkable Proofs from Decision Procedures: Issues and Progress

Allen Van Gelder

Abstract In many verification applications the desired outcome is that the formula is unsatisfiable: a satisfying assignment essentially exhibits a bug and unsatisfiability implies a lack of bugs, at least for the property being verified. Most current high-performance satisfiability solvers and special-theory decision procedures are unable to provide proof of unsatisfiability. Since bugs have been discovered in many such programs long after being put into service, an uncheckable decision poses a significant problem if important economic or safety decisions are to be based upon it. This talk develops the thesis is that decision procedures can and should be designed with the ability to output an independently checkable proof. While finding a proof is hard, checking a proof can be straightforward if the proof system is simple enough. (By a “proof” we mean a real proof, with no steps omitted.) In practice, most underlying theories can produce a resolution proof. We argue that outputting such a proof does not place an undue burden on the decision procedures. We report on practical progress in this area for satisfiability solvers. Experiments have been carried out with what might be the first implementations of solver and proof checker that were developed completely independently, having only the specifications of the proof-file format as common knowledge. There is a trend toward combining high-performance satisfiability solvers with other theorem-proving methods. As the total systems become more complex, the need for “independent audits” becomes greater. Design goals for checkable proofs are proposed.

Details

SAT Conference 2005 Conference Paper

Input Distance and Lower Bounds for Propositional Resolution Proof Length

Allen Van Gelder

Abstract Input Distance (Δ) is introduced as a metric for propositional resolution derivations. If \(\mathcal{F} = C_i\) is a formula and D is a clause, then \(\Delta(\mathcal{D}, \mathcal{F})\) is defined as min i | D – C i |. The Δ for a derivation is the maximum Δ of any clause in the derivation. Input Distance provides a refinement of the clause-width metric analyzed by Ben-Sasson and Wigderson (JACM 2001) in that it applies to families whose clause width grows, such as pigeon-hole formulas. They showed two upper bounds on \((W - width(\mathcal{F}))\), where W is the maximum clause width of a narrowest refutation of \(\mathcal{F}\). It is shown here that (1) both bounds apply with \((W - width(\mathcal{F}))\) replaced by Δ; (2) for pigeon-hole formulas PHP( m, n ), the minimum Δ for any refutation is Ω( n ). A similar result is conjectured for the GT ( n ) family analyzed by Bonet and Galesi (FOCS 1999).

Details

LPAR Conference 2005 Conference Paper

Pool Resolution and Its Relation to Regular Resolution and DPLL with Clause Learning

Allen Van Gelder

Abstract Pool Resolution for propositional CNF formulas is introduced. Its relationship to state-of-the-art satisfiability solvers is explained. Every regular-resolution derivation is also a pool-resolution derivation. It is shown that a certain family of formulas, called NT ** ( n ) has polynomial sized pool-resolution refutations, whereas the shortest regular refutations have an exponential lower bound. This family is a variant of the GT( n ) family analyzed by Bonet and Galesi (FOCS 1999), and the GT’n family shown to require exponential-length regular-resolution refutations by Alekhnovitch, Johannsen, Pitassi and Urquhart (STOC 2002). Thus, Pool Resolution is exponentially stronger than Regular Resolution. Roughly speaking a general-resolution derivation is a pool-resolution derivation if its directed acyclic graph (DAG) has a depth-first search tree that satisfies the regularity restriction: on any path in this tree no resolution variable is repeated. In other words, once a clause is derived at a node and used by its tree parent, its derivation is forgotten, and subsequent uses of that clause treat it as though it were an input clause. This policy is closely related to DPLL search with recording of so-called conflict clauses. Variations of DPLL plus conflict analysis currently dominate the field of high-performance satisfiability solving. The power of Pool Resolution might provide some theoretical explanation for their success.

Details

I&C Journal 2000 Journal Article

Partitioning Methods for Satisfiability Testing on Large Formulas

Tai Joon Park
Allen Van Gelder

Methods for partitioning large propositional formulas are investigated, with the goal of producing a set of smaller formulas whose satisfiability can be determined within reasonable time frames by known algorithms. CNF formula partitioning can be viewed as hypergraph partitioning, which has been studied extensively in VLSI design. Although CNF formulas have been considered as hypergraphs before, we found that this viewpoint was not productive for partitioning, and we introduce a new viewpoint in the dual hypergraph. Hypergraph partitioning technology from VLSI design is adapted to this problem. The overall goal of satisfiability testing requires criteria different from those used in VLSI design. Several heuristics are described and investigated experimentally. Some formulas from circuit applications that were extremely difficult or impossible for existing algorithms have been solved. However, the method is not useful on formulas with little or no structure, such as randomly generated formulas.

Details DOI

I&C Journal 1988 Journal Article

A satisfiability tester for non-clausal propositional calculus

Allen Van Gelder

An algorithm for satisfiability testing in the propositional calculus with a worst case running time that grows at a rate less than 2(0. 25 + ε)L is described, where L can be either the length of the input expression or the number of occurrences of literals (i. e. , leaves) in it. This represents a new upper bound on the complexity of non-clausal satisfiability testing. The performance is achieved by using lemmas concerning assignments and pruning that preserve satisfiability, together with choosing a “good” variable upon which to recur. For expressions in conjunctive normal form, it is shown that an upper bound is 20. 128L.

Details DOI

FOCS Conference 1986 Conference Paper

Parallel Complexity of Logical Query Programs

Jeffrey D. Ullman
Allen Van Gelder

We consider the parallel time complexity of logic programs without function symbols, called logical query programs, or Datalog programs. We give a PRAM algorithm for computing the minimum model of a logical query program, and show that for programs with the "polynomial fringe property, " this algorithm runs in logarithmic time. As a result, the "linear" and "piecewise linear" classes of logic programs are in NC. Then we examine several nonlinear classes in which the program has a single recursive rule that is an "elementary chain" We show that certain nonlinear programs are related to GSM mappings of a balanced parentheses language, and that this relationship implies the "polynomial fringe property; " hence such programs are in NC. Finally, we describe an approach for demonstrating that certain logical query programs are log space complete for P, and apply it to both elementary single rule programs and nonelementary programs.

Details