[UndefinedColumn Error] and How to Solve Non-Projected CNFs

[zhh-xu]

Hi,

First, thank you for your work on ⁠nesthdb – it looks like a very promising tool for parallel #SAT solving! I'm encountering two issues while trying to use ⁠nesthdb, and I'd appreciate any guidance you can offer.

Environment Details
I am using Python 3.10.12, psycopg2 2.9.10, and psql (PostgreSQL) 17.5. The OS is Ubuntu 22.04.3 LTS. The Branch is nesthdb.

Issue 1: psycopg2.errors.UndefinedColumn: column "td_root" of relation "problem" does not exist
When attempting to solve a simple CNF file using ⁠nesthdb.py with projected variables, I encounter an ⁠UndefinedColumn error.

cat f2.cnf
c ind 1 2 0
p cnf 2 1
1 2 0

And the Outputs

python3 nesthdb.py -f f2.cnf
[WARNING] dpdb.reader: Invalid content in preamble at line 0: c ind 1 2 0
[INFO] nestHDB: Original #vars: 2, #clauses: 1, #projected: 2, depth: 0
[INFO] nestHDB: Preprocessing #vars: 2, #clauses: 1, #projected: 2
[INFO] nestHDB: Primal graph #vertices: 2, #edges: 1
[INFO] nestHDB: Nested primal graph #vertices: 2, #edges: 1
[INFO] common: Tree decomposition #bags: 1 tree_width: 1 #vertices: 2 #leafs: 1 #edges: 0
Traceback (most recent call last):
  File "/home/x/workspace/dp_on_dbs/nesthdb.py", line 384, in <module>
    main()
  File "/home/x/workspace/dp_on_dbs/nesthdb.py", line 380, in main
    result = prob.solve()
  File "/home/x/workspace/dp_on_dbs/nesthdb.py", line 326, in solve
    return self.final_result(self.nestedpmc())
  File "/home/x/workspace/dp_on_dbs/nesthdb.py", line 270, in nestedpmc
    self.nested_problem.setup()
  File "/home/x/workspace/dp_on_dbs/dpdb/problem.py", line 337, in setup
    init_problem()
  File "/home/x/workspace/dp_on_dbs/dpdb/problem.py", line 253, in init_problem
    problem_id = self.db.insert("problem",
  File "/home/x/workspace/dp_on_dbs/dpdb/db.py", line 157, in insert
    return self.exec_and_fetch(q,values)
  File "/home/x/workspace/dp_on_dbs/dpdb/db.py", line 84, in exec_and_fetch
    cur.execute(q,p)
psycopg2.errors.UndefinedColumn: column "td_root" of relation "problem" does not exist
LINE 1: ..."type", "num_bags", "tree_width", "num_vertices", "td_root")...
                                                             ^

Issue 2: How to Solve Non-Projected CNFs

When attempting to solve a simple CNF file using ⁠nesthdb.py without projected variables, I can not turn it into normal #SAT version.

cat f.cnf
p cnf 2 1
1 2 0

And the Outputs

python3 nesthdb.py -f f2.cnf [\#sat]
[INFO] nestHDB: Original #vars: 2, #clauses: 1, #projected: 0, depth: 0
[INFO] nestHDB: Preprocessing #vars: 2, #clauses: 1, #projected: 0
[INFO] nestHDB: Intersection of vars and projected is empty
[INFO] nestHDB: Call solver: sat with #vars 2, #clauses 1, #projected 0
[INFO] nestHDB: Solver sat result: 1
[INFO] nestHDB: PMC: 1

Attempts Made:
I have tried specifying the problem type using ⁠SharpSat and ⁠#sat options, but they did not work. I also explored the ⁠configure_sharpsat.json and ⁠--sharpsat options mentioned in the dropbox, but these did not help either.

BTW, how can I set the number of threads for nestHDB in parallel mode? I tried "max_worker_threads" like dpdb, but I'm not sure it is work or not.

Thank you again for your time and assistance!

[zhh-xu]

I solved Issue 1: psycopg2.errors.UndefinedColumn: column "td_root" of relation "problem" does not exist, because I run both dpdb and nesthdb on same database. While I created a new database for nesthdb, the Error didn't cause.

[zhh-xu]

I merged nesthtd with the code in dropbox and solved the Issue 2: How to Solve Non-Projected CNFs.

I used most of the code and config.json in the pull request #9.

Thanks a lot.