Subsumption Algorithms for Three-Valued Geometric Resolution
Hans de Nivelle
TL;DR
This paper introduces efficient subsumption algorithms for three-valued geometric resolution, translating matching into constraint satisfaction problems and applying filtering techniques to improve performance.
Contribution
It presents novel algorithms and translation methods for subsumption testing in geometric resolution, including SAT-based approaches and local consistency filtering.
Findings
Filtering techniques can refute many constraint problems before solving
SAT-based algorithms improve matching efficiency
Algorithms find minimal interpretation solutions
Abstract
In our implementation of geometric resolution, the most costly operation is subsumption testing (or matching): One has to decide for a three-valued, geometric formula, if this formula is false in a given interpretation. The formula contains only atoms with variables, equality, and existential quantifiers. The interpretation contains only atoms with constants. Because the atoms have no term structure, matching for geometric resolution is hard. We translate the matching problem into a generalized constraint satisfaction problem, and discuss several approaches for solving it efficiently, one direct algorithm and two translations to propositional SAT. After that, we study filtering techniques based on local consistency checking. Such filtering techniques can a priori refute a large percentage of generalized constraint satisfaction problems. Finally, we adapt the matching algorithms in such…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsConstraint Satisfaction and Optimization · Data Management and Algorithms · Logic, Reasoning, and Knowledge
\lmcsheading
1–LABEL:LastPageMar. 09, 2017Dec. 11, 2018
Subsumption Algorithms for Three-Valued Geometric Resolution
Hans de Nivelle
School of Science and Technology, Nazarbayev University, 53 Qabanbay Batyr, Astana 010000, Kazakhstan
Abstract.
In our implementation of geometric resolution, the most costly operation is subsumption testing (or matching): One has to decide for a three-valued, geometric formula, if this formula is false in a given interpretation. The formula contains only atoms with variables, equality, and existential quantifiers. The interpretation contains only atoms with constants. Because the atoms have no term structure, matching for geometric resolution is hard. We translate the matching problem into a generalized constraint satisfaction problem, and discuss several approaches for solving it efficiently, one direct algorithm and two translations to propositional SAT. After that, we study filtering techniques based on local consistency checking. Such filtering techniques can a priori refute a large percentage of generalized constraint satisfaction problems. Finally, we adapt the matching algorithms in such a way that they find solutions that use a minimal subset of the interpretation. The adaptation can be combined with every matching algorithm. The techniques presented in this paper may have applications in constraint solving independent of geometric resolution.
1. Introduction
Main topic of this paper is the generalized matching problem, for example how to match into without matching This problem arose in the implemention of geometric resolution. Geometric logic as a theorem proving strategy was introduced in [2]. (The authors use the name coherent logic.) Bezem and Coquand were motivated mostly by the desire to obtain a theorem proving strategy with a simple normal form transformation, which makes that many natural problems need no transformation at all, others have a much simpler transformation, and which makes that in all cases Skolemization can be avoided. This results in more readable proofs, and proofs that can be backtranslated more easily.
Our motivation for using geometric resolution is different, more engineering-oriented: We hope that three-valued, geometric resolution can be made sufficiently efficient, so that it can be used as a generic reasoning core, into which different kinds of two- or three-valued decision problems (e.g. problems representing type correctness, two-valued decision problems, or simply typed classical problems) can be translated. Because we want the geometric reasoning core to be generic, we are willing to accept transformations that do not preserve much of the structure of the original formula. Subformulas are freely renamed, and functional expressions are flattened and replaced by relations. For details of the calculus, its motivation, and related work, we refer to [6].
In the current paper we give only a short introduction, which is aimed at explaining how matching is used in geometric resolution, and how matching instances in geometric resolution are translated into generalized constraint satisfaction problems. If one is interested only in the methods for constraint satisfaction, one can ignore the technical part of this section and continue reading at the overview at the end of this section.
We continue this section by giving a definition of three-valued, geometric formulas. The definition that we give here is slightly too general, but easier to understand than the correct definition in [6], which contains some additional, technical restrictions which are not relevant for matching.
{defi}
A geometric literal has one of the following four forms:
- (1)
A simple atom of form where are variables (with repetitions allowed) and (denoting false, error and true.) 2. (2)
An equality atom of form with distinct variables. 3. (3)
A domain atom with a variable. 4. (4)
An existential atom of form with and such that occurs at least once in the atom, not necessarily on the last place.
A geometric formula has form where the are simple or domain atoms, and the are atoms of arbitrary type.
We require that geometric formulas are range restricted, which means that every variable that occurs free in a must occur in an as well.
The intuitive meaning of is where are all the free variables. The vertical bar has no logical meaning. Its only purpose is to separate the two types of atoms.
A geometric formula that is not range restricted, can always be made range restricted by inserting suitable atoms into the left hand side. This is the only purpose of the -predicate. Interpretations contain predicates of form for every domain element Atoms in geometric formulas are variable-only, and are labeled with truth-values, as in [16]. It is shown in [4] and [6] that formulas in classical logic with partial functions ([3]) can be translated into sets of geometric formulas.
{defi}
We define an interpretation as a finite set of atoms of forms with a constant, or form where are constants (repetitions allowed). Interpretations must be range restricted as well. This means that every constant occurring in the interpretation must occur in an atom of form
Matching searches for false formulas. These are formulas whose premises clash with while none of the is true in
{defi}
Let be an interpretation. Let be a geometric literal. Let be a substitution that assigns constants to variables, and that is defined on the variables in We say that conflicts(or is in conflict with) if (1) has form and there is an atom of form with (2) has form and or (3) has form and
We say that is true in if
(1) has form and (2) has form and (3) has form and or (4) has form and there exists a constant s.t.
In the definitions of truth and conflict, is treated as a usual predicate.
{defi}
Let be an interpretation. Let be a geometric atom. Let be a substitution that instantiates all free variables of and for which is not true in We define the extension set as follows:
- •
If has form or then
- •
If has form then
- •
If has form then
[TABLE]
By we mean: is a constant occurring in an atom of We assume that is a fresh constant for which
Intuitively, if for a geometric formula and a substitution the are in conflict with while none of the is true in then is false in If there exist a and an atom that is not in conflict with then can be made true by adding If no such exists, a conflict was found. If more than one exists, the search algorithm has to backtrack through all possibilities. The search algorithm tries to extend an initial interpretation into an interpretation that makes all formulas true. At each stage of the search, it looks for a formula and a substitution that make the formula false. If no formula and substitution can be found, the current interpretation is a model. Otherwise, search continues either by extending or by backtracking. Details of the procedure are described in [8] for the two-valued case, and in [6] for the three-valued case. Experiments with the current three-valued version (available from [18]), and the previous two-valued version ([9]) show that the search for false formulas consumes nearly all of the resources of the prover.
{defi}
An instance of the matching problem consists of an interpretation and a geometric formula
Determine if there exists a substitution that brings all in conflict with and makes none of the true in If yes, then return such substitution.
{exas}
Consider an interpretation consisting of atoms
[TABLE]
The formula can be matched in five ways:
[TABLE]
The substitution would make the conclusion true. Next consider the formula
The substitution is the only matching of into Finally, the formula can be matched with and in no other way.
The first formula in example 1 has five matchings. In case there exists more than one matching, it matters for the geometric prover which matching is returned. This is because the prover analyses which ground atoms in the interpretation contributed to the matching, and will consider only those in backtracking. In general, the set of conflicting atoms in should be as small as possible, and should depend on as few as possible decisions. (Decisions in the sense of propositional reasoning, see [15].) The simplest solution for finding the best matching would be to enumerate all matchings, and use some preference relation to keep the best one. Unfortunately, this approach is not practical because the number of matchings can be extremely high. We will address this problem in Section 9.
Even if one is interested in the decision problem only, matching is still intractable because the decision problem is already NP-complete. (See problem LO18 in [12].) In this paper, we introduce several algorithms for efficiently solving the matching problem. The algorithms evolved out of predecessors that have been implemented before in the two-valued version of Geo ([9]), and in the three-valued version of Geo that took part in CASC J8 (see [18]). The matching algorithm of the three-valued version is discussed in detail in [5]. Unfortunately, after comparison with other methods, in particular the algorithms in the current paper, and translation to SAT, the approach of [5] turned out not competitive, and we have abandoned it. The algorithm in this paper, and translation to SAT are on average 500-1000 times faster than the algorithm of [5].
The paper is organized as follows: In Section 2, we translate the matching problem into a structure called generalized constraint satisfaction problem (GCSP). The generalization consists of the fact that it contains additional constraints, that a solution must not make true. These constraints correspond to the conclusions of the geometric formula that one is trying to match.
After that, we present in Section 3 a backtracking algorithm for solving GCSP, which is based on backtracking combined with a form of propagation. It relies on a data structure that we call refinement stack. Refinements stacks were introduced in [5]. The matching algorithm of [5] turned out non-competitive, but its data structure is still useful. In Section 4 we add conflict learning to our matching algorithm. In Section 5, we briefly discuss the algorithm of [5]. In Section 6, we give two translations from GCSP to SAT. The translations are straightforward, and efficiently solved by MiniSat ([11]). In order to make it possible to run our matching algorithm independent of geometric logic, possibly opening the way for other applications, we define an input format for matching problems in Section 7. The format is derived from the DIMACS format for SAT. We released the sources in [7]. Section 8 contains experimental results. The main conclusions are that the algorithm of [5] is not competitive, and that our own algorithm is comparable to translation to SAT combined with MiniSat. In Section 9, we explain how every algorithm that is able to find some solution, can be transformed into an algorithm that finds an optimal solution. This transformation is essential for the application in geometric resolution. In Section 10, we present a priori filtering techniques, that are able to reject a large percentage of matching instances a priori.
2. Translation into Generalized Constraint Satisfaction Problem
We introduce the generalized constraint satisfaction problem, and show how instances of the matching problem can be translated. It is ‘generalized’ because there are additional, negative constraints (called blockings), which a solution is not allowed to satisfy. The blockings originate from translations of the
{defi}
A substlet is a (small) substitution. We usually write in the form where is a sequence of variables without repetitions, and is a sequence of constants of same length as
We say that two substlets and are in conflict if there exist s.t. and
If is a sequence of substlets not containing a conflicting pair, then one can merge them into a substitution as follows:
If is a substitution and is a substlet, we say that makes true if every is present in
We say that and are in conflict if there is a with s.t. is defined and distinct from
A clause is a finite set of substlets with the same domain. We say that a substitution makes true (notation ) if makes a substlet true. We say that makes false (notation ) if every substlet is in conflict with In the remaining case, we call undecided by
{defi}
A generalized constraint satisfaction problem (GCSP) is a pair of form in which is a finite set of clauses, and is a finite set of substlets.
A substitution is a solution of if every clause in is true in and there is no s.t. makes true.
{defi}
Let a GCSP. We call range restricted if for every variable that occurs in a substlet there exists a clause s.t. every substlet has in its domain.
We now explain how a matching instance is translated into a generalized constraint satisfaction problem.
{defi}
Assume that and together form an instance of the matching problem. The translation of into GCSP is obtained as follows:
- •
For every let denote the variables of Then contains the clause
[TABLE]
- •
For every let denote the variables of For every that makes true in contains the substlet
Theorem 1**.**
A matching instance has a matching iff its corresponding GCSP has a solution.
In theory, the set of blockings can be removed, because a blocking can always be replaced by a clause as follows: Let be a blocking, let be its variables. Define and let be the blockings whose domain is also One can replace by the clause
We prefer to keep because in the worst case, the resulting clause has size where is the size of the domain. For example, if result from an equality then has form The resulting clause has size
Clauses resulting from a matching problem have the following trivial, but essential property:
Lemma 2**.**
Let be obtained by the translation in Definition 2. Let Then either or and are in conflict with each other.
Lemma 2 holds because and have the same domain.
{exas}
In example 1, the matching problem can be translated into the GCSP below. The clauses are above the horizontal line, and the blockings are below it. Because substlets in the same clause always have the same variables, we write the variables of a clause only once.
[TABLE]
Translating results in:
[TABLE]
Translation of results in:
[TABLE]
Before one runs any algorithms on a GCSP, it is useful to do some simplifications. If the GCSP contains a propositional clause (a clause whose domain contains no variables), this clause either has form (\ )\ /\ (no assignments), or (one assignment). In the first case, the problem is trivially unsolvable. In the second case, the clause can be removed.
Similarly, if contains a propositional blocking, then is trivially unsolvable. Such blockings originate from a that is purely propositional, or that has form
A third important preprocessing step is removal of unit blockings. Let be a blocking whose domain is included in the domain of some clause In that case, one can remove every substlet from that has If this results in being empty, then trivially has no solution. If no in any clause implies then can be removed from because of Lemma 2.
Applying removal of unit blockings to the translation of above results in
[TABLE]
It is worth noting that removal of propositional blockings can be viewed as a special case of removal of unit blockings.
A GCSP can be solved by backtracking, similar to SAT solving. A backtracking algorithm for GCSP can be either variable or clause based. A variable based algorithm maintains a substitution which it tries to extend into a solution. It backtracks by picking a variable and trying to assign it in all possible ways. It backtracks when makes a clause false, or a blocking true.
A clause based algorithm maintains a consistent set of substlets (whose union defines a substitution). It backtracks by picking an undecided clause and consecutively inserting all substlets that are consistent with into It backtracks when there is a clause all of whose atoms are in conflict with or when makes a blocking true.
Our experiments suggest that there is no significant difference in performance, nor in programming effort, between the two variants. We will stick with clause based algorithms, because it seems that they can be more easily combined with local consistency checking.
3. Matching Using Refinement Stacks
We first present the algorithm without learning, and add learning in the next section. The algorithm that we present here is a simplification of the algorithm in [5], which unfortunately could not be made competitive. The previous algorithm was based on a combination of local consistency checking and lemma learning from conflicts. Local consistency checking will be discussed in detail in Section 10, because there is still a probability that it can be used as priori check.
Local consistency checking means that one generates all subsets of clauses up to some size and checks which substlets can occur in solutions. Substlets that do not occur in any solution of some subset, certainly do not occur in a solution of the complete GCSP. In most instances, filtering with a small e.g. or results in an empty clause. The algorithm of [5] was based on a combination of local consistency checking and decision. It is discussed in more detail in Section 5.
The algorithm that we discuss in this section evolved from [5]. The main differences are: Clauses are not checked against each other anymore. Instead, clauses are checked only against the substitution in combination with blockings. Secondly, learnt lemmas are flat, i.e. finite disjunctions of single assignments to variables. In [5], lemmas were finite disjunctions of substlets. It turns out that this simplification improves performance by a factor between 100 and 1000.
In order to implement matching algorithms and local consistency checking, one needs to be able to remove substlets from clauses, and reintroduce them during backtracking. We call the process of removing substlets from a clause refinement. Whenever a clause has been refined, it may trigger other refinements. In the earlier algorithm, refinement of a clause could directly trigger more refinements of other clauses. In the current algorithm, refinement of a clause can only trigger possible extension of the substitution, but extension of the substitution may still trigger other clause refinements. As a consequence, one needs to maintain a queue of recent refinements and use this queue to check which more clauses can be refined. We introduce a data structure, called refinement stack which supports refinement of clauses, restoring during backtracking, and keeping track of unchecked refinements.
{defi}
A refinement has form where both and are clauses, and is a subclause of
A refinement stack is a finite sequence of refinements If there exists a with and then must be a strict subclause of
For a clause if is the last refinement with occurring in we call the current refinement of
We define a predicate that is true if is the current refinement of in This means that there is no with
A refinement stack supports gradual refinement of clauses. If is true, then clause can be refined into by appending to
In the new refinement stack we have is false, and is true.
The size of a refinement stack is defined as the total number of refinements that occur in it, independent of the values of
The refinement stack is initialized with the refinements for each initial clause Refinement stacks can be efficiently implemented without need to copy clauses by maintaining a stack of intervals of active substlets in the initial clauses. A substlet can be disabled by swapping it with the last active substlet in the interval, and decreasing the size of the interval by one. When the substlet is made active again, it is sufficient to restore the interval, because the order of active substlets in a clause does not matter. Refinement stacks support change driven inspection as well as backtracking.
Change driven inspection of clauses can be implemented by starting at position As long as one first checks If it is false, then is not the current version of and one can increase If is current, one can check if triggers refinement of other clauses. If yes, the results are inserted at the end, so that they will be inspected at later time. When one reaches one has reached a stable state.
When some change involving a variable takes place, one needs to check which clauses may be affected by the change, so that they can be refined. These are obviously the clauses that contain but also the clauses that contain a variable occuring in a blocking that contains since the algorithm takes blockings into account, when refining. This gives rise to the following definition:
{defi}
Let be two variables. We call and connected if and occur together in a blocking
We define the search algorithm. We assume that propositional clauses and unit blockings have been removed from We assume that the substitution is an ordered sequence (stack) of assignments
{algo}
We want to find a solution for Initially, set and After that, for each do the following:
**PREPROC: **
Let be the -th clause in Append to For every variable occurring in for which all substlets in agree on the value of let be the agreed value.
- **•: **
If is defined, and then return
- **•: **
If is undefined and there is a blocking containing s.t. then return Otherwise, append to
After that, we call the main search algorithm with It either returns or it extends into a solution of is defined as follows:
**FORW: **
As long as let be the -th assignment of
- **(1): **
For every which has true, and which either contains itself, or a variable that is connected to let
[TABLE]
If then return Otherwise, let
[TABLE]
If then return Otherwise, if then
- **(a): **
append to 2. **(b): **
For every variable occurring in that is unassigned in for which all substlets in agree on the assigned value, let be the agreed value. Append to 2. **(2): **
Set
**PICK: **
Find an with true and If no such exists, then is a solution.
Otherwise, for every substlet in do the following:
- **(1): **
Append to and extend with the unassigned variables in 2. **(2): **
Recursively call If was extended into a solution, then return 3. **(3): **
Otherwise, restore and to the sizes that they had before (1).
At this point, each of the recursive calls has returned Return
At FORW, the algorithm attempts deterministic reasoning. For every new assignment in it is checked if it conflicts with some substlets in some clause. Two types of conflicts are considered, either the substlet contains an assignment that directly conflicts with or it contains an assignment that, together with implies a blocking. As long as conflicts are found, the corresponding clauses are refined. Refinement of a clause may result in being extended (FORW b), if the remaining substlets agree on an assignment. Extension of may result in further refinements of clauses.
If FORW failed to solve the problem, then at PICK a non-unit clause is picked, and non-deterministically refined into a unit clause. This step requires backtracking. It is important (for performance) to pick a clause of minimal length.
Main purpose of PREPROC is to initialize the refinement stack with After that, is initialized by looking for assignments that are common to all substlets in some clause. If this results in a conflict (either directly, or with a blocking), the problem is rejected.
Algorithm 3 is similar to DPLL in that it tries to postpone backtracking as long as possible by giving preference to deterministic extension. At FORW, blockings are taken into account. It is possible to implement FORW without considering blockings. In that case, it has to be checked, whenever the substitution is extended (at PICK 2 and at FORW 1b) that the extended substitution does not imply a blocking. The given version performs better in experiments.
In order to show that Algorithm 3 is correct, i.e. does not report false solutions, we have to show that all necessary checks are made.
Lemma 3**.**
- (1)
At points FORW and PICK of Algorithm 3, there is no s.t. 2. (2)
At point PICK, no refined clause contains a substlet that is in conflict with
Initially, the preprocessor ensures that there is no s.t. When is extended in FORW 1b, it has been checked before that does not imply a blocking, for each of the substlets in At point PICK, findmatch passed through FORW which refined away all substlets that conflict with
In the next section, we will extend Algorithm 3 with learning. This will prove completeness, because whenever Algorithm 3 does not find a solution, it will construct a lemma that proves that no lemma exists.
4. Conflict Learning
It is known from propositional SAT solving that conflict learning dramatically improves the performance of SAT solvers ([15]). The matching algorithm in the two-valued version of Geo ([9]) was already equipped with a primitive form of conflict learning. Before releasing Geo, we had experimented with naive matching, the algorithm in [13], and many ad hoc methods. Matching with conflict learning is the only approach that results in acceptable performance. Despite this, matching was still a critical operation in the last two-valued version of Geo. In the two-valued version of Geo, lemmas had form i.e. they had form for a single substlet.
In [5] we proposed to replace the lemmas of Geo 2007 by arbitrary sets of substlets. It is quite easy to see, that in general such a lemma can be in conflict with more substitutions than a lemma of the previous form. For example, if we assume that the domain is and the range then rejects a single substitution, while rejects 25 substitutions. Since in case of a conflict, one can always obtain a lemma of the second form, it seemed that lemmas of the second form should be preferred over lemmas of the first form.
The latest version of Geo see ([18]) used the algorithm of [5] with lemmas of the unrestricted form above. Although this matching algorithm performs better than matching in Geo 2007, recent experiments have shown that it performs significantly worse than some other approaches, in particular translation to SAT and Algorithm 3 in combination with flat lemmas. Flat lemmas are lemmas of form Surprisingly, Algorithm 3 with unrestricted lemmas performs several orders worse than Algorithm 3 with flat lemmas. This is surprising, because every general lemma can be flattened into a lemma of the second form by picking a single assignment from each substlet. The resulting lemma is obviously less general than its original, non-flattened version. This loss of generality also applies to the reasoning rules that we use on lemmas. If two substlets in two general lemmas are in conflict, then their flattenings are not necessarily in conflict. Conversely, whenever two flattened substlets are in conflict, their original counterparts are. This means that by using flattened lemmas, one looses conflicts with substitutions, and also resolution derivations involving lemma resolution. Despite this clever reasoning, the first columns of Figure 1 of Section 8 show that Algorithm 3 with flat lemmas performs approximately 200-400 times worse than Algorithm 3 with unrestricted lemmas. One could assume that this is caused by the fact that handling of unrestricted lemmas is more costly, and that their theoretical advantage is compensated by the increased cost of their maintenance. This assumption is rejected by Figure 1, because Algorithm 3 with flattened lemmas is not only faster, but it also uses less lemmas, typically by a factor 2-3. The only point where Algorithm 3 with and without flattening can diverge, is when a conflict lemma rejects a substitution and there exists more than one conflict lemma. Since both versions will prefer the shortest lemma, it must be due to the fact that flattening changes the relative sizes of the lemmas.
The outcomes of the experiments make it probable that the best approach to matching will be either Algorithm 3 with flat lemmas, or translation to SAT in combination with a SAT-solver, which we will describe in Section 6.
From the practical point of view, the fact that the refining algorithm in [5] turned out not competitive, is not a serious loss. Despite being elegant on paper, it was hard to implement. Implementation of Algorithm 3 was much easier, and in the long term, it is better that the easier algorithm has the better performance. Moreover, it is clear from Figure 1 that matching in future versions of Geo can be approximately times faster than it was at Geo 2016c ([18]).
We will now introduce the flat lemmas, and prove that Algorithm 3 can always generate a flat conflict lemma.
{defi}
A lemma is an object of form with The are variables, and the are finite sets of constants.
It is convenient to treat lemmas as total functions from variables to sets of constants. For a variable and is defined as
Let be a substitution. We say that makes true if there exists a variable in the domain of for which
We say that makes false if all variables for which is nonempty, are in the domain of and In that case, we write
{defi}
Let be a GCSP. Let be a lemma. We say that is valid in if every solution of makes true.
For a given substitution we call a conflict lemma if is valid and makes false.
If is a substitution, and there exists a valid lemma that is false in then it is not possible to extend into a solution of
In order to derive the conflict lemma, the following rules will be used:
{defi}
Given a GCSP we define the following derivation rules:
**RESOLUTION: **
Let be a sequence of lemmas. Let be a variable. Let be the set of variables for which one of the has We define the -resolvent of as
[TABLE]
**PROJECTION: **
Let be a clause, let be a lemma. We call a projection of if every substlet contains an assignment s.t.
**-RESOLUTION: **
Let be a blocking. Write Let be clauses, chosen in such a way that every variable occurs in For every let
[TABLE]
Then the lemma
[TABLE]
is called a -resolvent of
The lemmas and can resolve into Given clauses and and a blocking one can obtain the -resolvent The lemma is a projection of is also a projection of It is easy to see that the reasoning rules are valid, which implies that every lemma that has been obtained by repeated application from the original clauses in and blockings in is valid.
Lemma 4**.**
Let be a GCSP. Let be an interpretation. Let be a blocking for which Let be a -resolvent of Then makes false.
Proof 4.1**.**
Write Let be the clauses that were used in the construction of Because we know that for every we have From the construction of the it follows that Because the variables are pairwise distinct, we have It follows that For all other variables that do not occur in we have We can conclude that if is non-empty, then equals one of the and we have
The following lemma states that substlets that are switched off, were switched off because they conflict possibly with help of a blocking.
Lemma 5**.**
At every moment during Algorithm 3, for every refinement the following holds: If then either is in conflict with or for a
Proof 4.2**.**
There are two points at which refinement can take place, PICK 1 and FORW 1a. At PICK 1, clause is refined into after which is extended with If some substlet occurs in then either or In the first case, the desired property is inherited from the previous state, because it is an invariant. In the second case, because is extended by at the same time, we can apply Lemma 2.
At FORW 1a, if then either or In the first case, the desired property is inherited from the previous state. In the second case, it follows from the construction of that was in conflict with In the third case, it follows from the construction of that there is a for which
The following property is the essential property, for proving that Algorithm 3 can always return a conflict lemma.
Lemma 6**.**
Let be a GCSP. Let be a clause. Let be a substitution. Let be a set of lemmas. Assume that there is no s.t. and no s.t. makes false. Assume that for every substlet either
- (1)
* is in conflict with * 2. (2)
* for a or* 3. (3)
* makes a false.*
Then it is possible to derive a conflict lemma for from and by applying the rules in Definition 4.
Proof 4.3**.**
We first remove (2) by means of -resolution. We will add the resulting -resolvents to For every for which do not apply, must apply. Write Since is range restricted, we can find clauses s.t. each occurs in We now can construct the -resolvent. Write for the resulting lemma. It follows from Lemma 4 that is false in We can add to At this point, we have for every either or The rest of the proof is Lemma 7.
Lemma 7**.**
Let be a GCSP. Let be a clause. Let be a substitution. Let be a set of lemmas. Assume that there is no s.t. makes false. Assume that for every substlet either
- (1)
* is in conflict with or* 2. (2)
* makes a false.*
Then it is possible, using the rules in Definition 4, to obtain a conflict lemma for from and
Proof 4.4**.**
We prove the lemma by induction on the number of unassigned variables in Let be the part of to which (1) applies, and let
Since each is in conflict with one can obtain a projection of by picking from each an assignment for which is defined and By construction, will be false in
If there are no unassigned variables in then must be empty. This means that is a projection of and false in so we are done.
Otherwise, select a in that is unassigned by Let be set of values that are assigned to by the substlets in Define Clearly, is a projection of and is a projection of For each value define If there is no that is false in then still satisfy the conditions of Lemma 7. Moreover, since contains an assignment to the number of unassigned variables in has decreased by one. This means that we can assume, by induction, that we can derive a lemma that is false in If is also a conflict lemma of we have completed the proof. Otherwise, we can assume that is added to
At this point, contains a conflict lemma for every with Let be the -resolvent of the projection constructed above, and the i.e.
[TABLE]
In order to show that is false in we have to show that for every variable for which is defined, and
- •
For we just show that We have because It follows from the fact that is undefined in and is false in For each we know that is false in which implies that This implies that is not in the intersection of all which in turn implies and have no elements in common.
- •
If and then either for an or In the first case, it follows from the fact that is false in and that is defined. In the second case, we know that only assigns to so that Since we know that is false in we know is defined.
At this point, we are certain that is defined, so that we can start showing that If then, because only assigns to we have This is impossible because is false in
We can also not have for any because this would imply that which contradicts the fact that is false in
At this point, it is straightforward to prove that Algorithm 3 can always derive a conflict lemma. There are two points in Algorithm 3 where the substitution is extended. We show for both points that it is possible to obtain a conflict lemma when the substitution is restored.
**FORW 1b: **
The substitution is extended by the common assignments in Since the extension of had a conflict lemma, we know that for each has a conflict lemma. It follows from Lemma 5 that for every substlet in either is in conflict with or implies for a blocking From Lemma 3, we know that there is no s.t. It follows that we can apply Lemma 6 with to obtain a conflict lemma for
**PICK: **
Let be the refinement that was selected by PICK. Let be the set of conflict lemmas that were returned by the recursive calls of findmatch. If there is a that is false in we can return Otherwise, we know that no is false in From Lemma 3, we know that there is no s.t.
By Lemma 5, every substlet is either in conflict with or there exists a s.t. This implies that we can apply Lemma 6 to obtain a conflict lemma of
In an implementation of Algorithm 3, there is no need to follow the rules of Definition 4 carefully, because the conflict lemma can be constructed immediately from the premisses of Lemma 6.
In order to make Algorithm 3 reuse conflict lemmas, one has to add before FORW 1: If there is a containing variable s.t. makes false, then return
Integrating lemmas into the refining step of FORW 1 seems difficult, because the notion of connection (Definition 3) must be extended to include ‘ and occur together in a lemma ’ Currently we don’t know how to efficiently enumerate variables that are connected through a lemma.
5. Matching Based on Local Consistency Checking
We will discuss the matching algorithm of [5]. Its performance turned out not competitive, so we will omit most of the details, in particular the completeness proofs for learning. The algorithm is based on the fact that local consistency checking rejects a large percentage of GCSPs without backtracking.
Local consistency checking is the following procedure: For every clause check, for all sets of clauses with size if has a solution. If not, then remove from Keep on doing this, until no further changes are possible or a clause has become empty. The procedure is described in detail in Section 10. Local consistency checking with small rejects a large percentage of instances without backtracking. It therefore seemed reasonable to combine local consistency checking with backtracking in the following way:
**FILTER: **
Apply local consistency checking. If this results in an empty clause, then backtrack to the last decision. If there are no decisions left, then report failure.
**DECIDE: **
If every clause has become unit, then report a solution. Otherwise, pick a non-unit clause, and replace it by a singleton consisting of one of its substlets. Continue at FILTER. If this results in an empty clause, then backtrack through the remaining substlets of the clause.
The assumption was that local consistency checking could play the same role as unit propagation in DPLL, and that local consistency checking would be equally effective on the subproblems obtained during backtracking, as on the initial problem. This assumption turned out false. In [5], the algorithm is described for but we have implemented it for arbitrary Note that a size of means that so that has size Performance results are presented in Figure 2 in Section 8. It can be seen that does not perform better than It rarely creates less lemmas, and it usually costs more time.
The main observation to be made is that the algorithm is not close to being competitive against Algorithm 3 with flat lemmas, or translation to SAT. In addition to that, it turned out rather unpleasant to implement, much harder than Algorithm 3. Especially is difficult to handle, because the resolution rules for obtaining lemmas become rather complicated. This does not only apply to the implementation, but also to the theoretical description.
We define the lemmas that were used by the matching algorithm, and the reasoning rules that it uses. A clause can be viewed as a special form of lemma in which the substlets have the same domain.
{defi}
A lemma is a finite set of substlets, possibly with different domains.
If is a lemma, and a substitution, then makes true if there is a substlet s.t. makes true. makes false if every substlet is in conflict with We say that is valid relative to if is true in every solution of We call a conflict lemma if is false in the current and valid
Learning was based on the following resolution rules:
{defi}
Let and be lemmas. Let and let Assume that every is in conflict with every Then is a resolvent of and
One can resolve with based on and The resolvent is
{defi}
Let be a blocking. Let be a sequence of clauses containing all variables of For each let Then is a -resolvent of
Using given above, and blocking one can obtain the -resolvent
It is easy to see that both conflict resolution and -resolution are valid reasoning rules, which implies that every lemma that was derived by repeated application of resolution from the original clauses in is valid.
In [5], it was shown that a matching algorithm using can always obtain a conflict lemma using resolution and -resolution. For an additional rule, called product resolution, is required. Results are listed in Figure 2.
After observing that Algorithm 3 improves by a factor when lemmas are flattened, we tried the same with the refining algorithm. Whenever a new lemma is derived, the assignments that do not contribute to conflicts are removed from the substlets. Different from Algorithm 3, this does not necessarily lead to a lemma consisting only of single-assignment substlets, but in most cases it does. Surprisingly, this has a strong, negative impact on the performance.
6. Translation to SAT
Translating an instance of the matching problem to SAT is easy, and modern SAT solvers have become very effective. As a consequence, translation to SAT should be attempted. In this section, we give two methods of translating GCSP into SAT. The translations are not complicated, and MiniSat [11] performs rather well on the results of the translations. Results are listed in the last two columns of Figure 1 and in Figure 3 in Section 8. The results suggest that translation to SAT has a performance that is comparable with Algorithm 3.
In our first translation only substlets are translated. We assign propositional variables to the substlets, specify that at least one substlet from each clause has to be selected, and list the conflicts between the substlets.
{defi}
We assume a general mapping that transforms mathematical objects into distinct propositional variables.
{defi}
Let be GCSP. The translation into propositional logic has form where is a set of atoms, and is a set of clauses over Assume that the GCSP has form assume that contains clauses, and write for the -th clause of
The set of atoms is defined as The clause set is defined as follows:
- (1)
For every the propositional clause set contains the propositional clause and for every the clause 2. (2)
For every pair of distinct clauses that share a variable, for every substlet contains the clause
[TABLE] 3. (3)
For every blocking we assume that there is a way of selecting a most suitable subset of that contains all variables of Then contains the clause
[TABLE]
The first part specifies that exactly one substlet must be selected from each The second part specifies that if one selects a substlet from one has to select a substlet from that is not in conflict with The third part of Definition 6 can be viewed as an application of -RESOLUTION (Definition 5).
The second translation differs from the first translation in the fact that it does not only translate substlets, but also variable assignments. In addition to the substlets, it assigns propositional variables to variable assignments It specifies the dependencies between substlets and variable assignments. Instead of relying on -RESOLUTION, blockings can be specified directly in terms of the forbidden variable assignments.
{defi}
Let be a GCSP. Write Write each in the form The translation to propositional logic has form where is the set of atoms used in the translation, and is the set of clauses. The set of atoms is defined as
[TABLE]
The set of propositional clauses is obtained as follows:
- (1)
For every clause clause set contains the clause 2. (2)
For every substlet with for every assignment that occurs in clause set contains the clause 3. (3)
For every variable that occurs in for every two distinct values s.t. and occur somewhere in substlets in clause set contains the clause 4. (4)
For every blocking if every occurs somewhere in a clause in then clause set contains the clause If some does not occur in then is impossible, and there is no need to generate a clause for it.
We show correctness of Definition 6. If has a solution one can define a satisfying interpretation for as follows:
- •
For set iff
- •
For every assignment occurring in a substlet occurring in a clause set iff
It is easily checked that makes all clauses in Definition 6 true.
For the other direction, assume that has a satisfying interpretation Define By part 4, does not contain conflicting assignments. By part 1 and part 2, contains an assignment for every variable occurring in Because of part 3, does not imply a blocking By part 1 and part 2, every contains one substlet that agrees with
We end the section with an example of both translations:
{exa}
We will translate the following GCSP. As usual, and are separated by a horizontal bar.
[TABLE]
alone has three solutions:
[TABLE]
The first solution is blocked by the third solution is blocked by so that only is a solution of the complete GCSP. Assume that
[TABLE]
Definition 6 constructs the following translation:
[TABLE]
The only satisfying interpretation is which corresponds to In order to apply the second translation, assume that
[TABLE]
The second translation constructs
[TABLE]
Its only satisfying interpretation is which again corresponds to
7. An Input Format for GCSP
Since we are claiming that GCSPs are fundamental enough to study on their own, and may have applications outside of geometric resolution, we made our implementation publicly available ([7]). In this section, we define the input format for GCSP, which is used by our implementation. The format is similar to the DIMACS format for satisfiability ([1]). Similar to the DIMACS format, variables and constants are represented by integers. Since GCSP has no polarity (there is no negation), all integers are non-negative.
{defi}
We define a representation for GCSP. Input is represented in plain ASCII. The format never distinguishes between upper and lower case.
- •
Input starts with whitespace, possibly mixed with comment lines. A comment line is a line whose first non-whitespace character is a ‘c’ or a ‘C’. The initial comment lines are ignored.
- •
After that comes a line of form
p gcsp nrvars nrconsts nrclauses nrblockings
nrvars is the number of variables in the problem, nrconsts is the number of constants in the problem. Both need not be exact, but must be upperbounds. More precisely, both variables and constants are represented by non-negative integers, and nrvars,nrconsts must be bigger than any variable or constant that appears in the problem.
nrclauses must be the exact number of clauses, and nrblockings must be the exact number of blockings.
- •
A clause has form V var1 ... varV S subst1 ... substS. Here V is the exact number of variables in the clause, and var1 ... varV are the variables, represented by non-negative integers. Each variable must be less than nrvars.
S is the exact number of substlets in the clause. Each substlet is represented by a sequence of non-negative integers of length V, that specifies the values assigned to the variables, in the same order as the variables. Each value must be less than nrconsts. There must be exactly nrclauses clauses.
- •
Blockings are represented in the same way as clauses. Although in Definition 2, blockings are single substlets, it is convenient to merge blockings with identical domain into clauses, so that they can be represented more compactly.
There must be exactly nrblockings (merged) blockings. Note that it is not obligatory to merge blockings with same domain.
- •
Everything after the blockings is ignored, so there is room for more comments.
- •
Solutions are presented in the format
A V1 C1 ... VA CA
Here A is the number of assignments in the substitution, and each Vi Ci is an assignment. The assigments can be listed in arbitrary order.
{exa}
We represent the GCSP of Example 6. There are three variables which we will represent by This means that is an upperbound. There are two constants so that is an upperbound. This is a representation:
c we did not merge the blockings
p gcsp 3 2 2 2
2 0 1 2 0 1 1 0 2 1 2 3 0 0 0 1 1 0
2 0 2 1 0 0 2 0 2 1 1 1
Since the two blockings in Example 6 have the same domain, the GCSP can be alternatively represented as follows:
c this time we merged the two blockings c there is no difference in meaning
P GCSP 3 2 2 1
2 0 1 2 0 1 1 0 2 1 2 3 0 0 0 1 1 0
2 0 2 2 0 0 1 1
The solution can be output as 3 0 1 1 0 2 0. Since the order is arbitrary, it can also be output as 3 1 0 2 0 0 1.
8. Experiments
We present measurements on two benchmark sets. Both sets were obtained by running Geo on a few input problems, and collecting hard matching instances. The first set consists of problems that took more than an hour to solve with a naive matching algorithm. This set was used in Figures 1 and 2.
Entries in Figure 1 have form where is the time used in seconds, and the number of lemmas generated. For the 3d and 4th column, the times are the CPU-times reported by MiniSat (Version 2.0 beta) ([11]). Since MiniSat is not integrated into Geo, it is difficult to measure the total time (conversion+solving). For hard problems, the conversion times are probably negligible, but for trivial problems, they may be significant (in the same order of magnitude as the solving times) because translation is quadratic. Due to the way the benchmarks were collected, they contain no trivial problems. It can be seen from Figure 1 that translation to propositional SAT is comparable to Algorithm 3 with flat lemmas. We will dicuss this more in the context of Figure 3. We were not sure how to determine the number of lemmas generated during a run of MiniSat, due to the fact that it performs restarts. Currently, we simply added the numbers reported by the different restarts. Since MiniSat probably reuses lemmas between different restarts, this means that the indicated numbers are likely too high. It can be seen that nearly always, Definition 6 performs better than Definition 6.
Figure 2 shows results for the refining algorithm of [5], discussed in Section 5. It can be seen that using is hardly worth the effort, and that the refining algorithm performs somewhat worse than Algorithm 3 with learning of unrestricted lemmas. Since flattening of lemmas improves the performance of Algorithm 3 dramatically, we tried the same with the refining algorithm. Unfortunately, the last column of Figure 2 shows that flattening has a big, negative impact on the refining algorithm. That means that the refining algorithm can be ruled out as a candidate for being optimal.
Figure 3 presents another benchmark test that was obtained by running Geo on several input problems using Algorithm 3 with flat lemmas. We started by setting a short initial time Whenever a matching took more than seconds to solve, we added it to the benchmark set, and doubled From several runs, we kept the last three instances generated in this way. Figure 3 shows that most of the problems obtained in this way, are also hard for MiniSat. We believe Figure 3 shows the potential of direct matching algorithms, but there are several caveats: Runs of geo do not generate really hard matching instances, all instances are solved within seconds, most much faster. The way of collecting problems that are hard for Algorithm 3 puts it at a disadvantage. For example, there may be problems that are hard for MiniSat, which will not enter the benchmark set. On the other hand, MiniSat is not state of the art anymore, and modern SAT solvers probably will perform better. We carefully conclude that there is a chance that in the long term, at least for some applications, our approach of directly implementing matching, may be the optimal approach.
9. Finding Optimal Matchings
In this section we address the problem of finding optimal matchings. For the effectiveness of geometric resolution, it is important that a minimal matching is returned, in case more than one exists. A minimal matching is a matching that uses the smallest possible set of assumptions. In terminology of DPLL, assumptions represent decision levels. The assumptions contributing to a conflict represent choice options, which will be replaced by other options during backtracking. In addition to being as few as possible, assumptions at a lower decision level should always be preferred over assumptions at a higher decision level. The reason for this is the fact that in other branches of the search tree, there is a risk that more assumptions will be used, and when assumptions are at a lower level, there is less room for this.
{defi}
Let be an interpretation. A weight function is a function that assigns finite subsets of natural numbers to the atoms of
Let be a geometric literal. Let be a substitution such that is in conflict with Referring to definition 1, we define and
{defi}
Let and together form an instance of the matching problem (Definition 1). Assume that is a solution. The weight of for which we write is defined as
[TABLE]
Solving optimal matching means: First establish if has a solution. If it has, then find a solution for which is multiset minimal.
One could try to impose further selection criteria that are harder to explain and whose advantage is less evident.
Solving the minimal matching problem is non-trivial, because the number of possible solutions can be very large. The straightforward solution is to use some efficient algorithm (e.g. the one in this paper) that enumerates all solutions, and keeps the best solution. Unfortunately, this approach is completely impractical because some instances have a very high number of solutions. One frequently encounters instances with solutions.
In order to find a minimal solution without enumerating all solutions, one can use any algorithm that stops on the first solution in the following way: The first call is used to find out whether a solution exists. If not, then we are done. Otherwise, the algorithm is called again with its input restricted in such a way that it has to find a better solution than the previous. One can continue doing this, until all possibilities to improve the solution have been exhausted. It can be shown that the number of calls needed to obtain an optimal solution is linear in the size of the assumption set of solution. In this way, it can be avoided that all solutions have to be enumerated.
{defi}
Let be an interpretation that is equipped with a weight function Let be a geometric formula. Let be a fixed set of natural numbers. We define the -restricted translation of as follows:
- •
For every let be the variables of Then contains the clause
[TABLE]
- •
For each let denote the variables of For every that makes true in contains the substlet In addition, if there exists a that is in conflict with and for which then contains the substlet
The -restricted translation ensures that only conflicts involving atoms with are considered, and (independently of ), that no is made true. The translation of Definition 2 can be viewed as a special case of -restricted translation with
Theorem 8**.**
Let be obtained by -restricted translation of For every substitution is a solution of iff is a solution of and it has
Using -restricted translation, we can define the optimal matching algorithm:
{algo}
Let be a function that returns some solution of if it has a solution, and otherwise.
We define the algorithm that returns an optimal solution of if one exists and otherwise.
- (1)
Let be the GCSP obtained by the translation of Definition 2. If contains an empty clause, then return If contains a propositional blocking, then return Otherwise, remove unit blockings from If this results in containing an empty clause, then return 2. (2)
Let If then return 3. (3)
Let and let 4. (4)
As long as do the following:
- •
Set If then do
- –
Let
- –
Let be the -restricted translation of
- –
If contains an empty clause or contains a propositional blocking, then skip the rest of the loop. Otherwise, remove the unit blockings from If this results in containing the empty clause, then skip the rest of the loop.
- –
Let If then set and 5. (5)
Now is an optimal solution, so we can return
Algorithm first solves without restriction. If this results in a solution it checks for each if can be removed. The invariant of the main loop is: There exists no that occurs in and no that is a solution of with In addition, the invariant is maintained.
{exa}
Assume that in example 1, the atoms have weights as follows:
[TABLE]
We have and If is the first solution generated, will construct the -restricted translation of which equals
[TABLE]
If the next solution found is then will construct the -restricted translation
[TABLE]
whose only solution is
10. Filtering by Local Consistency Checking
Filtering is any procedure that simplifies or possibly rejects a GCSP before the main algorithm is called. In Geo, we have used filtering based on local consistency checking. In earlier versions, this was effective because very often, filtering rejects a GCSP without calling the main algorithm. Since the algorithms that we present in this paper, are much more efficient, this is not certain anymore. We still present the local consistency checking procedure, because it is easy to implement using refinement stacks, and it may be still an effective tool for filtering out easy instances.
Local consistency checking (see [10, 14, 17]) is a pre-check that comes in many variations. Local consistency checking is the following procedure: For every clause check, for all sets of clauses with size if has a solution. If not, then remove from Keep on doing this, until no further changes are possible or a clause has become empty. Local consistency checking rejects a large percentage of GCSP instances a priori, and usually decreases the size of the clauses involved by a factor two or three.
In [10] (Chapter 3), local consistency checking is defined using subsets of variables (instead of clauses). Using subsets of two variables is called arc consistency checking, while considering subsets of three variables is called path consistency checking. In general, using bigger subsets is a more effective precheck, but also more costly because it gets closer to the original problem.
As discussed in Section 5, we had assumed in [5] that filtering is so effective, that one can base the complete search algorithm on it. Although this is possible in theory, the resulting algorithm turned out not competitive.
Since the local consistency checks the substlets in a single clause against sets of clauses we define the size of a local consistency check as When performing a local consistency check up to size one has to generate subsets up to size and generate their solutions. If the total number of such subsets equals \left(\begin{array}[]{l}n\\ S+1\\ \end{array}\right), which grows very quickly for realistic The problem can be decreased by not generating all subsets, but only generate subsets whose clauses share variables, or have variables that co-occur in a blocking. {defi}
Let be clauses. We write if either and share a variable, or there exist connected (Definition 3) variables and s.t. occurs in and occurs in
It is sufficient to generate subsets that are connected, because consideration of subsets that are not connected will not lead to the removal of more substlets. We always assume that solutions are non-redundant, i.e. do not contain irrelevant assignments.
Lemma 9**.**
Let be a GCSP. Let If can be written as s.t. there exist no and no with then for every two substitutions s.t. is a solution of and is a solution of is a solution of
Lemma 9 guarantees that it is not needed to attempt to remove substlets from clauses in after and have been checked. If some substlet in occur some solution of and has a solution, then will occur in the combined solution.
We will now show that instead of ignoring disconnected subsets, one can also ignore subsets that are connected only through a single clause:
Lemma 10**.**
Let be a GCSP. Assume that and Assume that for every pair of variables occurring in a clause of and occurring in a clause of if either or and are connected, then occur in
Then the following holds: If is a solution of and is a solution of s.t. agree on the variables occurring in then is a solution of
Proof 10.1**.**
Assume that fulfil the conditions of the lemma. By non-redundancy, does not contain assignments to variables not occurring in or Similarly, does not contain assignments to variables not occurring in or If share a variable then this variable must occur in which implies that As a consequence, and can be merged into a single substitution which has
If there would be a blocking s.t. then we still have and This implies that there are variables in and occurring in which occur together in But this contradicts the fact that and cannot be connected.
As above, if some substlet is used in a solution of and has a solution, then the solutions can be combined into a single solution that uses If some substlet of occurs in a solution of and in a solution of then the solutions can be combined into a single solution that still uses
This implies that, if one uses a local consistency checker that gives preference to small subsets, one can ignore subsets that do not contain ’cycles’. If there exist s.t. are not connected, and every path from to has to pass through then can be ignored. This gives rise to the following definition:
{defi}
Let with be a sequence of clauses. We call a circle if for every we have and in addition we have
If is a refinement stack, we call a sequence of indices a circle if each is true, and is a circle.
The local consistency checker checks only circles. Generation of circles in is easier to implement than generation of all connected subsets, especially if one wants to avoid generating the same subset in different ways. In addition, it is more efficient because there are less circles than connected subsets. The discussion above suggests that generating circles is sufficient to obtain a complete check. We have believed for some time that this is true in general, but we will show below that it is false.
{algo}
Let be a natural number. Let be a substitution. Let be a refinement stack.
A call to constructs a refinement of by removing the substlets that do not occur in any solution of the subset of of size
It returns if it establishes that cannot be extended into a solution of Initially
**SUBST: **
As long as let be the -th assignment in
- **(1): **
For every blocking involving check if If yes, then return 2. **(2): **
For every which has true and which contains let be the set of substlets in that are consistent with If then return Otherwise, if append to
**CLAUSES1: **
As long as do the following:
- **(1): **
If is true, and the -refinement contains a variable s.t. all substlets agree on the assignment to then let be the agreed value. Append to 2. **(2): **
Set
If then restart at SUBST. (This means that was extended in the previous step.)
**CLAUSESN: **
As long as there is an with s.t. pick the smallest such If holds, then
- **(1): **
Enumerate all circles of size starting at For each such circle let
Call If the result is then return If after the call, we have then restart at CLAUSES1.
Let be a refinement stack. Let Let be a subset of s.t. for every holds. Algorithm is defined as follows:
- (1)
Initialize a map with domain by setting for each Eventually, will map each to the set of substlets in that can occur in a solution of extending 2. (2)
Enumerate all maps with domain that map each to a substlet in and that have the following properties: No conflicts no are in conflict with each other. does not imply a blocking
For each of the generated mappings for each set 3. (3)
For every for which add the refinement to
The local consistency checker gives priority to checking against the substitution. After checking for conflicts against the substitution, Algorithm 10 generates circles of size up to and checks for each of the substlets occurring in the clauses of such a circle, whether it can occur in a solution. Substlets that do not occur in a solution are refined away. Preference is given to small circles. This means that circles of size will be checked only after all circles up to size have been checked.
We will discuss (and disprove) the conjecture mentioned above, that it is sufficient to check circles, when preference is given to smaller subsets. More precisely: If for a given subset all its subcircles have been checked, then needs to be checked only if it is a circle by itself. We formally define what ’has been checked’ means:
{defi}
Let be a GCSP. Let be a substitution. Let be a subset of clauses of We write for the following property: For every clause for every substlet there is a solution of s.t.
Algorithm 10 tries to establish for every subset of size up to It assumes that when holds for circles with size smaller than and is not a circle, then automatically holds. We have believed for some time that this assumption is true, because Lemma 9 and Lemma 10 provide evidence for it, and it simplifies Algorithm 10. Unfortunately, the property fails at when circles have size
Conjecture 11**.**
Let be a GCSP. Assume that every strict subset that can be arranged into a circle has property Then if cannot be arranged into a circle, has the property
We prove Conjecture 11 for and provide a counter example for
Proof 10.2**.**
- •
* follows from Lemma 9.*
- •
In order to prove assume that are clauses that do not form a circle. Without loss of generality, we may assume that If we also have then can be partitioned into so that Lemma 9 can be applied. If we have we can apply Lemma 10 with
- •
We prove We use the fact that Conjecture 11 holds for Let If can be partitioned into two disjoints sets, we can apply Lemma 9, and we are done. Otherwise, if cannot be partitioned into disconnected sets, there are two possibilities:
- –
The clauses form a line If then is a circle, so that Conjecture 11 holds trivially.
Otherwise, we can still have or If we have both, then is a circle, so that Conjecture 11 again holds trivially.
If we can apply Lemma 10 with and
Similarly, if we can apply Lemma 10 with and
- –
The clauses form a kind of star with in the center:
For if nor we can apply Lemma 10 with
If we have both of and then is a circle.
In the remaining case, we may assume without loss of generality that but also
This means that we have If then is a circle. If then we can apply Lemma 10 with
We give a counter example for {exa}
Consider the following GCSP, which has no blockings, and the following clauses:
[TABLE]
We have and There are no other connections. The example can be understood as follows: Clause requires that Similarly, requires that and requires that Clause requires that is even, while requires that is odd. Since the sums must be equal, and cannot be odd and even at the same time, has no solution.
Ignoring direction and starting point, there are three circles of size
[TABLE]
Since the circles are symmetric, we show that every substlet occurring in can occur in a solution. One can pick the instance of and in such a way that they agree on and They will disagree on but because is not considered, this is no problem. After that, the instances to and are fixed. It is easily checked that cannot be arranged into a circle.
Example 10.2 contains a GCSP that would not be refined by Algorithm 10 with despite the fact that it has no solution. We will refrain from trying to make Algorithm 10 complete, because we believe that it is not worth the effort. Experiments suggest that using Algorithm 10 becomes too costly already at Implementing a more elaborate check at would make Algorithm 10 even more costly, and harder to implement, without much hope for improvement.
It is important to observe that even when Algorithm 10 is used as a precheck, it still needs to be restorable, because it may be called by Algorithm 9, which will turn on and off different substlets, based on Only the first call need not be restorable.
11. Conclusions
The problem of matching a geometric formula into an interpretation used to be the bottleneck of our implementation of geometric resolution. In order to improve this situation, we gave a translation of the matching problem into GCSP, and provided efficient approaches for solving GCSP. One approach is to solve the GCSP directly by a combination of refinement, backtracking and learning. The other approach is to translate the problem into SAT. Our experiments suggest that both approaches have comparable performance. Both approaches still have room for improvement. For translation to SAT, one could develop a dedicated SAT solver. For the direct approach using GCSP, one could add heuristics that control when learnt lemmas are forgotten, and probably it will be possible to add deep backtracking.
Independent of the relative performance of the two approaches, one can conclude that the speed of Geo can be improved by a very large factor, and that matching is no longer the bottleneck that hinders further development of the geometric resolution calculus.
Since GCSP may have applications outside of geometric logic, we defined an input format for GCSP, similar to DIMACS format for SAT, that can be used for independent applications. We also made the sources of our matching algorithm available.
The fact that the clause refining algorithm based on local consistency checking turned out not competitive, shows that search algorithms that appear good in theory, are not necessarily good in practice. In general, it is difficult to predict what will be the effect of a modification of a search algorithm. A seemingly small change may have a large impact on performance.
As for geometric resolution, one might argue that a calculus that uses an NP-complete problem as its basic operation is not viable, but there is room for interpretation: The complexity of the matching problem is caused by the fact that as result of flattening terms, geometric formulas and interpretations have DAG-structure instead of tree-structure. This increased expressiveness means that a geometric formula possibly represents exponentially many formulas with tree-structure. This may very well result in shorter proofs. Only experiments can determine which of the two effects will be stronger.
12. Acknowledgements
We gratefully acknowledge that this work was supported by the Polish National Science Center (Narodowe Centrum Nauki) under grant number DEC-2015/17/B/ST6/01898 (Application of Logic with Partial Functions). A large part of this work was carried out while the author was employed at Wrocław University, Poland.
The reference list from the paper itself. Each links out to its DOI / PubMed record.
- 1[1] Unknown Author. Satisfiability suggested format. http://www.cs.ubc.ca/~hoos/SATLIB/Benchmarks/SAT/satformat.ps .
- 2[2] Marc Bezem and Thierry Coquand. Automating coherent logic. In Geoff Sutcliffe and Andrei Voronkov, editors, LPAR , volume 3835 of LNCS , pages 246–260. Springer Verlag, 2005.
- 3[3] Hans de Nivelle. Classical logic with partial functions. Journal of Automated Reasoning , 47(4):399–425, 2011.
- 4[4] Hans de Nivelle. Theorem proving for logic with partial functions by reduction to Kleene logic. In Christoph Benzmüller and Jens Otten, editors, Automated Reasoning in Quantified Non-Classical Logics (ARQNL) 2014 , pages 71–85. VSL Workshop Proceedings, 2014.
- 5[5] Hans de Nivelle. Subsumption algorithms for three-valued geometric resolution. In Nicola Olivetti and Ashish Tiwari, editors, International Joint Conference on Automated Reasoning (IJCAR) 2016 , volume 9706 of LNCS , pages 257–272. Springer, 2016.
- 6[6] Hans de Nivelle. Theorem proving for classical logic with partial functions by reduction to Kleene logic. Journal of Logic and Computation , 27(2):509–548, 2017. (Accepted April 2014).
- 7[7] Hans de Nivelle. solver for GCSP. can be obtained from https://cs-sst.github.io/faculty/nivelle under ‘Implementation’, 2018.
- 8[8] Hans de Nivelle and Jia Meng. Geometric resolution: A proof procedure based on finite model search. In John Harrison, Ulrich Furbach, and Natarajan Shankar, editors, International Joint Conference on Automated Reasoning 2006 , volume 4130 of Lecture Notes in Artificial Intelligence , pages 303–317, Seattle, USA, August 2006. Springer Verlag.