exactly one clauses

[gsgs2]

is it possible -in theory- to handle exactly-one-clauses (non-cnf) more efficiently by SAT-solvers like kissat ?

they are tedious and lengthy to convert to cnf and are used by exact-cover problem conversions.

These are clauses where exactly one from a list of variables is true and all others in the list are false.

[DvonHolten]

• in theory - yes- AFAIK, there was/is some cardinality detection in lingeling-solver. the problem is, i think, how to detect such a construct in a 'sea-of-clauses' - there are a handful of different 1-of-n encodings. can be hairy to build some pattern/structure matching for all of them. one direction for the future might be to investigate, which encoding is most easily detected, implement that in the solver(s) and state 'this solver supports this kind of 1-of-n cardinality. if you use that - good. if you use another one - no gain'.

[gsgs2]

thanks. I'm new to SAT (and github) - I'll look up "lingeling" ...

My idea was to include the non-cnf-clauses in the instance-file and mark them as exactly-one and the solver would detect that.

[benjaminbartsch]

@gsgs2: I developed my own encoding (i guess its already well known). In my experience its quite efficient:

Input: List of Integers Algorithm:

if (list.isEmpty())
    return UNSAT 

WHILE list.size() >= 2
    a = list.removeFirst()
    b = list.removeFirst()
    addClauseNothBothTrue(a, b)
    c = createVariableLogicalOR(a, b)
    list.addLast(c)

// we constructed a binary tree. the list contains the root // up to this point we encoded "AT MOST ONE". The root has // the information if there is a TRUE element. if we force the root to // be TRUE, then we have encoded "EXACTLY ONE"

x = list.removeFirst()
addClause(x); 

If you need JAVA Code I can post it. The encoding has O(n) additional clauses and variables. All clauses have size <= 3.

[gsgs2]

yes, that's "pairwise" in this paper : https://iopscience.iop.org/article/10.1088/1742-6596/1288/1/012035/pdf I also tried "bitwise", but not the 3rd one (too complicated)

For my special type of problems pairwise and bitwise made no big difference for kissat , which btw. was 10 times faster than "dancing links" , old version.

I was thinking that it is maybe not so effective for kissat to handle all these many clauses for just one logical context.

[arminbiere]

The winner of this year's SAT competition uses (Structured) Bounded Variable Addition (BVA) as preprocessing and then CaDiCaL (using Kissat as backend was for still unknown reasons less efficient). During experiments of our original paper on BVA

Norbert Manthey, Marijn Heule, Armin Biere. Automated Reencoding of Boolean Formulas. In Proc. Haifa Verification Conference (HVC'12), Lecture Notes in Computer Science, vol. 7857, pages 102-117, Springer 2013.

we already realized that BVA reencodes pairwise (also called 'naive' or 'direct' encoding) of the at-most-one constraint into something better. Results were only empirical though and we did not analyze whether in principle BVA can turn the direct encoding into for instance the product or sequential counter encoding. The best encoding recursively starts with PE, then switches to something reported above and at the end (with say less than 6 variables) switches to the direct encoding. I think Knuth writes about this in his SAT book too. The paper on structural bounded variable addition (SBVA) has a better heuristic for tie breaking when introducing new variables and seems to give some additional benefit empirically

https://drops.dagstuhl.de/opus/frontdoor.php?source_opus=18473

There are also papers on using cardinality constraints natively, for instance this one

A Cardinality Solver: More Expressive Constraints for Free Mark H. Liffiton and Jordyn C. Maglalang SAT'12

There might be some groups working on revisiting this idea.

Finally as discussed above Lingeling extracts at-most-[12] constraints (if they are not hidden). There are more ways to do that:

Armin Biere, Daniel Le Berre, Emmanuel Lonca, Norbert Manthey. Detecting cardinality constraints in CNF. In Proc. 17th Intl. Conf. on Theory and Applications of Satisfiability Testing (SAT'14), Lecture Notes in Computer Science, vol. 8561, 285-301, Springer 2014.

[DvonHolten]

... and then comes the clever preprocessing technique BVE (bounded variable elimination) How is it assured, that they dont interfere? Are these artificial variables marked? Are they output in the final model (when there is a solution)? thanks for the dagstuhl-link

[arminbiere]

BVA strictly decreases the number of clauses, while in the (base) version of BVE you never add more clauses then you remove during variable elimination. After BVA the model projected onto the original variables is a model of the original formula, so you just have to filter out those.

However, combining BVA with inprocessing, i.e., interleaving BVA and BVE, is not trivial (you need to garbage collect variables I guess and further need some good heuristics as BVE in inprocessing does increase the number of clauses) and the main reason I did not port it to Kissat nor CaDiCaL sofar. More problematic is even how to apply BVA to incremental solving, particularly while generating proofs. That is also the reason the SBVA paper and their solver in the competition just used BVA for preprocessing (separate C++ preprocessing program then CaDiCaL orchestrated with a Python script).

[arminbiere]

I am closing this discussion as an issue. If you want to continue, I would suggest to start a proper discussion.