Appending CNF clauses and solving Using Cadical

savecancel

I have the following small example where i convert a boolean polynomial into CNF write it into a file and try to solve it using Cadical195. This code works when I remove cnf.append([1,2,3,4]) but I get an error when appending. The error is: NotImplementedError: Native atmost constraints are currently disabled. Can someone tell me why this happens and how to fix it? The goal is to solve a SAT problem and adding constraints that exclude the current solution iteratively to compute other solutions.

from pysat import *
from pysat.formula import CNF
from pysat.solvers import Cadical195, Solver
from sage.sat.converters.polybori import CNFEncoder
from sage.sat.solvers.dimacs import DIMACS

B.<x,y,z> = BooleanPolynomialRing()
fn = tmp_filename()
solver = DIMACS(filename=fn)
e = CNFEncoder(solver, B)
e.clauses_dense(x*y+z)
 _ = solver.write()

cnf = CNF(from_file=fn)
print(open(fn).read())
cnf.append([1,2,3,4])
solver= Cadical195()
with Cadical195(bootstrap_with=cnf,with_proof=True) as l:
    is_sat = l.solve()
    solution= l.get_model()