kclause_to_dimacs.py does not create a correct CNF

[ekuiter]

Hi Paul,
working on my ASE paper from last year, I kind of found (but forgot to look into and report) the following problem in scripts/kclause_to_dimacs.py. Now, for a new project, I stumbled across it again, so here's a proper report. :)

The file uses the following code to transform its SMT input into CNF/DIMACS:

use_tseitin = True

if use_tseitin:
  g = z3.Goal()
  g.add(constraints)
  t = z3.Tactic('tseitin-cnf')
  solver.add(g)
else:
  solver.add(constraints)

print((solver.dimacs()))

But the tseitin-cnf tactic in the variable t is never used, so the solver.dimacs() is just called as-is.

As I just reported over at Z3Prover/z3#6577, this kind of usage is actually not allowed in Z3. Yes, it will return a DIMACS file, but this file is generally neither equisatisfiable nor model-count-preserving to the original formula (and Z3 fails to report this correctly). For a possible fix, see the linked issue (tseitin-cnf must be called explicitly, Z3 does not implement a non-Tseitin CNF conversion, apart from setting a higher distributivity_blowup).

All users of this file are affected, in the best case it's only me, as I understand that you only work with the internal SMT representation. Also, it does not affect my ASE paper, as I wrote my own scripts for that. But future users could run into this problem (I only ran into this again because I tried to run #SAT on large feature models and got suspicious results).

Best, Elias

[ekuiter]

another small issue: right now, setup.py does not restrain the z3 solver version, so the newest version (4.12.1) is used. but in this version (4.11.2 behaves differently), the call to tseitin has changed and must include the simplifier:

goal = z3.Goal()
with open(sys.argv[1], 'rb') as file:
  goal.add(z3.parse_smt2_string(file.read()))
goal = z3.Then("simplify", "elim-and", "tseitin-cnf")(goal)[0] # use Then(...) instead of Tactic(...)
print(goal.dimacs())

besides this fix, i suggest to pin the z3 version in setup.py with z3-solver==4.12.1 to make sure the script does not break in the future (for now, i'll patch this manually with sed -i 's/z3-solver/z3-solver==4.12.1/' setup.py)

[paulgazz]

Thank you @ekuiter ! Will make the fixes this week.

[paulgazz]

Hi @ekuiter I'm having issues with using the simplier in 4.12.1. I still apparently get this operator not supported error. Maybe I'm making a mistake somewhere?

(env_kmax) paul@device:~/src/linux$ python3 ~/research/repos/kmax/scripts/kclause_to_dimacs.py .kmax/340d16735ccc/kclause/x86_64/kclause
detected binary pickle file
Traceback (most recent call last):
  File "/home/paul/research/repos/kmax/scripts/kclause_to_dimacs.py", line 34, in <module>
    goal = z3.Then("simplify", "elim-and", "tseitin-cnf")(goal)[0] # use Then(...) instead of Tactic(...)
  File "/home/paul/env_kmax/lib/python3.8/site-packages/z3_solver-4.12.1.0-py3.8-linux-x86_64.egg/z3/z3.py", line 8254, in __call__
    return self.apply(goal, *arguments, **keywords)
  File "/home/paul/env_kmax/lib/python3.8/site-packages/z3_solver-4.12.1.0-py3.8-linux-x86_64.egg/z3/z3.py", line 8244, in apply
    return ApplyResult(Z3_tactic_apply(self.ctx.ref(), self.tactic, goal.goal), self.ctx)
  File "/home/paul/env_kmax/lib/python3.8/site-packages/z3_solver-4.12.1.0-py3.8-linux-x86_64.egg/z3/z3core.py", line 3849, in Z3_tactic_app
ly
    _elems.Check(a0)
  File "/home/paul/env_kmax/lib/python3.8/site-packages/z3_solver-4.12.1.0-py3.8-linux-x86_64.egg/z3/z3core.py", line 1482, in Check
    raise self.Exception(self.get_error_message(ctx, err))
z3.z3types.Z3Exception: b'operator not supported, apply simplifier before invoking this strategy'

This is the updated script so far:

import pickle
import z3
import sys

def get_kclause_constraints(kclause_file):
  try:
    with open(kclause_file, 'r') as fp:
      kclause = pickle.load(fp)
  except UnicodeDecodeError as ex:
    sys.stderr.write("detected binary pickle file\n")
    with open(kclause_file, 'rb') as fp:
      kclause = pickle.load(fp)

  kclause_constraints = {}
  for var in list(kclause.keys()):
    kclause_constraints[var] = [ z3.parse_smt2_string(clause) for clause in kclause[var] ]

  constraints = []
  for var in list(kclause_constraints.keys()):
    for z3_clause in kclause_constraints[var]:
      constraints.extend(z3_clause)

  return constraints

if len(sys.argv) > 1:
  kclause_file = sys.argv[1]
else:
  kclause_file = ".kmax/kclause/x86_64/kclause"
  
constraints = get_kclause_constraints(kclause_file)

goal = z3.Goal()
goal.add(constraints)
goal = z3.Then("simplify", "elim-and", "tseitin-cnf")(goal)[0] # use Then(...) instead of Tactic(...)
print(goal.dimacs())

[ekuiter]

AFAICT, it should work.

i can't execute your code (pickle.load fails with TypeError: a bytes-like object is required, not 'str') on a Linux 2.6.32 kclause file like this

config CONFIG_LEDS_DA903X tristate
prompt CONFIG_LEDS_DA903X (CONFIG_NEW_LEDS and CONFIG_LEDS_CLASS and CONFIG_PMIC_DA903X)
config CONFIG_MMC_SDHCI_S3C_DMA bool
prompt CONFIG_MMC_SDHCI_S3C_DMA (CONFIG_MMC and CONFIG_MMC_SDHCI_S3C and CONFIG_EXPERIMENTAL)
config CONFIG_USB_SISUSBVGA tristate
...

maybe you can send me your kclause input file? i am working on an older kmax version (pinned to c6e83a0), so maybe my kclause files are not up to date.

[paulgazz]

Here's the kclause file I'm using: kclause.txt. I think Necip switched to using a binary pickled format at some point (though I called it .txt since github restricts by extension).

[ekuiter]

UnicodeDecodeError: 'ascii' codec can't decode byte 0x80 in position 0: ordinal not in range(128)
i think Github broke it somehow by assuming it's a txt 🤷 maybe as a zip file?

[paulgazz]

Good call. Try this: kclause.zip

[ekuiter]

I still can't get it to work, not sure what is going on:
UnicodeDecodeError: 'utf-8' codec can't decode byte 0x80 in position 0: invalid start byte
Here's my Docker script: docker-test.zip

[paulgazz]

Hi @ekuiter, apologies for the confusion. I have not yet merged the proposed fix. I've updated your Dockerfile to checkout the branch with your suggested fixes: docker-test-branch.zip. See if you get past the encoding issue now. Instead it should show the 'operator not supported' error:

detected binary pickle file
Traceback (most recent call last):
  File "/home/kmax/scripts/kclause_to_dimacs.py", line 34, in <module>
    goal = z3.Then("simplify", "elim-and", "tseitin-cnf")(goal)[0] # use Then(...) instead of Tactic(...)
  File "/usr/local/lib/python3.10/dist-packages/z3_solver-4.12.1.0-py3.10-linux-x86_64.egg/z3/z3.py", line 8254, in __call__
    return self.apply(goal, *arguments, **keywords)
  File "/usr/local/lib/python3.10/dist-packages/z3_solver-4.12.1.0-py3.10-linux-x86_64.egg/z3/z3.py", line 8244, in apply
    return ApplyResult(Z3_tactic_apply(self.ctx.ref(), self.tactic, goal.goal), self.ctx)
  File "/usr/local/lib/python3.10/dist-packages/z3_solver-4.12.1.0-py3.10-linux-x86_64.egg/z3/z3core.py", line 3849, in Z3_tactic_apply
    _elems.Check(a0)
  File "/usr/local/lib/python3.10/dist-packages/z3_solver-4.12.1.0-py3.10-linux-x86_64.egg/z3/z3core.py", line 1482, in Check
    raise self.Exception(self.get_error_message(ctx, err))
z3.z3types.Z3Exception: b'operator not supported, apply simplifier before invoking this strategy'

[paulgazz]

Hi @ekuiter I just remembered that we have supported generating dimacs in the klocalizer tool (#54). It uses solver.dimacs() to generate it. Does this suffer from the same problems or is that a fine way to do this? Here is an example using it:

klocalizer -a x86_64 --save-dimacs dimacs

[ekuiter]

I have looked at your file and can reproduce the issue. But I am still not able to find the problem. When I remove constraints from the file, at some point it works. But I've tried now for 2 hours to find the problematic constraint and still couldn't find it (bisection does not work, removing constraints randomly kind of works, but not always... maybe the error is non-deterministic). I'll see if I find another way.

Regarding klocalizer: solver.dimacs() has the same problem. The only way to reliably convert a formula into CNF is with the Tactic/Then API, which only exists for the goal class.

[ekuiter]

I tried another approach and now have a minimum failing example, although it still has over 2000 constraints: docker-test-branch.zip

I exported it into SMTLib and removed all non-boolean variability: min-bool.smt.txt
This gives the same error message as above with z3.Then("simplify", "elim-and", "tseitin-cnf")(goal)[0] in Z3 4.12.1.

This is either a bug in Z3 or I am using the API wrong. I'll contact the Z3 developers.

[ekuiter]

Until we have a better solution, my workaround is to use z3 4.11.2, where the above works fine.

[paulgazz]

Understood. Thanks @ekuiter !