treewidth

[gsgs2]

is there a concept similar to "treewidth" for SAT-problems ?
That gave improvements in "parameterized programming"

We can just make the graph whose vertices are the variables
and there is an edge, iff 2 vertices appear in the same clause.

Then reorder the vertices with a treewidth program
and feed the reordered instance into kissat
(skipping kissat's initial reordering)

[arminbiere]

There is this early work on SAT which one might want to revisit:

Guiding SAT Diagnosis with Tree Decompositions

and related successful work in model counting by

Johannes K. Fichte DBLP papers

as well this hybrid version

SharpSAT-TD in Model Counting Competitions 2021-2023

[gsgs2]

thanks. I see, with so much work done on SAT such ideas can't be new.
I'm converting special randomized Hamiltonian Cycle problems to exact-cover and SAT
problems and my simple naive pathwidth-like reordering gives a factor 2
with my HCP-solver . Kissat seems to be fastest on these graphs for larger sizes.
I'd like a command-line switch to disable kissat's initial sorting of the variables
so to experiment with several reorderings , as I did with HCP.
current timings : http://magictour.free.fr/x9.l1l

[arminbiere]

Interesting problem indeed. Fixing the variable order only initially should not have a large impact on solving time but it is also clear that certain benchmarks (particularly pigeon holes) benefit from always using a fixed static variable order. Kissat is very precise in following the given order in the file (initially). So you could achieve this effect with giving the variable indices in the order you want your decisions to occur. Actually it would allocate internal variable indices based on first occurence of a variable (as the 'tumble' option enforces that and is turned on by default). So to achieve a static order you can use '--no-tumble', '--no-bump' and then give the indices in the desired order. If you only want it initially drop the '--no-bump'.
The solver switches from stable to focused mode once in a while. In focused mode it uses VMTF and the last activated variable comes last and thus first as decision. Similarly in stable mode the EVSIDS ordered binary heap is used and there the score is initialized with '1-1/idx', so also increasing with larger variable index. Therefore the last activated variable is also picked first as decision. Now the catch is that this initialization of the scores resp. VMTF queue position is done during activation of a variable and thus really as the variables occur in the file.

[DvonHolten]

does that mean, SAT-solvers use the variable-order in the CNF-file as the order to try an assignment? No nifty heuristics? like number of clauses using this variable? Average size of the clauses using this variable?
I always wondered, why the intro videos of the inner workings of SAT-solving say very little about how to pick the next variable to work on - it just happen to be there !
What about restarts? wouldn't it be beneficial to rearrange the variables (or the order of their processing) a little bit after each restart? So the 'probes' into different areas of the formula.

[arminbiere]

Yep, and it does make a difference.

BTW, MiniSAT packs the variables as they appear on the EVSIDS binary heap and then picks as first decision the one on the top of the heap (the first one unless score randomization is enabled which is off by default). Thus usually first decision is '-1'. Then when pulling off the next decision from the binary EVSIDS heap it will pop '1' from it by the usual replacement of the last variable in the heap (and popping that one from the heap). Therefore the next variable is the one with the highest index in the file. This continues until the first conflict and variables are bumped. So for 99 variables the first decisions will be -1,-99,-98,...,-3,-2. Now check out these benchmarks I generated for showing that the propagation in MiniSAT is quadratic and on these benchmarks all the time is spent in propagation without reaching a single conflict: Quadratic Propagation Benchmarks. The organizers of the SAT Competition 2017 did not use them though (neither the other MiniSAT adverserial benchmarks I submitted).

I also have looked into various ways to reorder the decision queue/heap, i.e., 'shuffle' in CaDiCaL, but without much success though.

[DvonHolten]

is there a way to find out the optimal order of variables (or decisions)? After the result is obtained - to get some insight, how this affects performance. Of course, this would not be transferrable to other problems or solvers - but it might bring some insight.
To me it seems, very little is known.

[DvonHolten]

"propagation in MiniSAT is quadratic and on these benchmarks all the time is spent in propagation without reaching a single conflict" - does that mean, conflict is preferred over propagation? of course CD means 'conflict driven' - but how do you get conflicts in an area of unassigned variables?

[arminbiere]

We know that a linear static order decision scheme is not good as it kind of gives you OBDD power, while FreeBDDs are exponentially more succinct. Already for OBDDs it is hard problem to find the best order and there are some papers (for FreeBDDs I do not remember any work). So finding a good "initial" order is another then more practical problem.

[DvonHolten]

'best order' may not be required - just knowing 'this rule' gives better results most of the time than 'that rule' could be a step forward.

when i think of it, i would go for the variable with most binary clauses - would lead to unit propagation and drive things forward.

[arminbiere]

Yes exactly, reviving all the old 1990ies work on branching heuristics is a good idea.

[DvonHolten]

why not ...
that research was based on solvers and encodings in the 90s - is it guaranteed that it's still valid today?

[arminbiere]

I do think it is a good in case might comment looked like irony.

[gsgs2]

From the treewidth/pathwidth consideration, I would try to sort the variables so to minimize the average interaction between the already used variables and the rest. ---------------------------------- first occurrence of a variable , tumble --no-tumble -- no bump . you can use '--no-tumble', '--no-bump' and then give the indices in the desired order. you mean, kissat doesn't sort the variables and already performs differently on equivalent , variable-permuted or clause-permuted instances ? I find 101 lines in the code with keyword "sort", 2 with sort variables LOG ("quick sorting %zu analyzed variables", size); I'm using kissat sc2020 , I found the Ubuntu executable somewhere online with keyword search. sudo apt install kissat would be nice I have not yet experimented with varible reordering and no-tumble maybe later today

…

------------------------------------------- VMTF = EVSIDS = VSIDS [31,2004] maps each variable to a score and bumping a variable consists in increasing the score of the variable We actually intended to go to EVSIDS this year’s competition (EVSIDS For the new version 3.1.0 (sc2023) of Kissat ... We also incorporated the ESA idea proposed in the compe- tition last year [4] and schedule bounded variable elimination attempts based on variables scores (EVSIDS and VMTF stamps [3]) and refined it further by taking the difference and not as previously the sum when falling back to the number of positive and negative occurrences of a variable. We also went over SAT sweeping again which improved it slightly. Am 18.12.2023 13:32 schrieb Armin Biere:

Interesting problem indeed. Fixing the variable order only initially should not have a large impact on solving time but it is also clear that certain benchmarks (particularly pigeon holes) benefit from always using a fixed static variable order. Kissat is very precise in following the given order in the file (initially). So you could achieve this effect with giving the variable indices in the order you want your decisions to occur. Actually it would allocate internal variable indices based on first occurence of a variable (as the 'tumble' option enforces that and is turned on by default). So to achieve a static order you can use '--no-tumble', '--no-bump' and then give the indices in the desired order. If you only want it initially drop the '--no-bump'. The solver switches from stable to focused mode once in a while. In focused mode it uses VMTF and the last activated variable comes last and thus first as decision. Similarly in stable mode the EVSIDS ordered binary heap is used and there the score is initialized with '1-1/idx', so also increasing with larger variable index. Therefore the last activated variable is also picked first as decision. Now the catch is that this initialization of the scores resp. VMTF queue position is done during activation of a variable and thus really as the variables occur in the file. -- Reply to this email directly, view it on GitHub [1], or unsubscribe [2]. You are receiving this because you authored the thread.Message ID: ***@***.***> Links: ------ [1] #48 (comment) [2] https://github.com/notifications/unsubscribe-auth/BCAREI4PLPWZOWMSZMU6FI3YKAZXXAVCNFSM6AAAAABAYT7HCGVHI2DSMVQWIX3LMV43SRDJONRXK43TNFXW4Q3PNVWWK3TUHM3TQOBVHE4DA

[gsgs2]

I. CADICAL VIVINST
variable instantiation [2]
this form of variable instantiation tries to remove literals that appear less often.

[2] G. Andersson, P. Bjesse, B. Cook, and Z. Hanna, “A proof engine
approach to solving combinational design automation problems,” in
Proceedings of the 39th Design Automation Conference, DAC 2002,
New Orleans, LA, USA, June 10-14, 2002.
ACM, 2002, pp. 725–730.
[Online]. Available: https://doi.org/10.1145/513918.514101

---

https://www.cambridge.org/core/journals/theory-and-practice-of-logic-programming/article/on-the-foundations-of-grounding-in-answer-set-programming/573D6EDC447B516CF2A5D90B1A262332
We provide a comprehensive elaboration of the theoretical foundations of variable
instantiation, or grounding, in Answer Set Programming (ASP)

systematically replacing all variables by
variable-free terms. This process is called grounding.
{I don't understand. is it removing a variable by considering two problems,
one for x=true and one for x-false ?)

the importance of grounding has somehow been eclipsed by
that of solving

---

now, in my "railway graphs" I may have "clause-grounding" ?
I can recursively replace one of the n exactly-one-clauses
by another railway-graph with that clause omitted
but typically with more variables (=edges in the graph)
And I speculate that selecting the suitable clause for that
recursion is the best strategy to solve the SAT-problem

"Suitability" is somehow estimated by the balace of the
vertex-degrees or the distribution of the counts of the
number of variables in the eo-clauses

[gsgs2]

sorry, that recursion in my railway-graphs doesn't work, it's more complicated.
still there is an "instantantiation" on each of the n clauses
rather than (only) on each of the n*5 variables.
If I understand instantantiation=grounding correctly.

[arminbiere]

This is instantiation as used in CaDiCaL (in two forms - stand alone and in combination with vivification) is just a preprocessing algorithm and allows to remove variables in clauses. So is (mostly) independent of encoding.

[gsgs2]

I downloaded kissat3.1.0 with the --no-bump feature from
https://github.com/arminbiere//kissat/releases/tag/rel-3.1.0/kissat-3.1.0-linux-amd64.zip
it's 20% faster than sc2020 on my graphs at a first test.
--no-tumble has no impact
--no-tumble --no-bump is 3 times slower
my initial reordering reduces this to 50% slower
while --no-tumble alone or the original commandline
was insensitive to reordering
This was a reordering of the original (randomized) graph,
the general reordering of the variables-clauses graph
had no impact.

I now recoded the clingo file with the exactly-one clauses
from the exact-cover encoding and it is faster than kissat
for sizes n<80 (n5=400 variables,3600 cnf-clauses
(n4=320 EO-clauses with 4-6 terms)
on my railway-graphs.

time in seconds for 100 instances of sizes 40,50,60,70,80:
clingo:3,13,41,214,1320,
kissat:6,26,76,290,1195,