using pbenc or atmost function from cadical195 do not yield expected result

[alnugro]

Hi, I am new to SAT solving in general. I am coming from ILP/SMT and want to learn solving things in SAT. One problem that I keep running into is that using PBEnc or atmost from cadical195 does not yield the expected result. I ran the following code:

from pysat.formula import CNF, IDPool
from pysat.pb import PBEnc
from pysat.solvers import Solver



# Define literals, weights, and the bound
lits = [1, 2, 3 ,4]
weights = [3, 3, 3, 3]
upperbound = 5
lowerbound = 4
inverted_wights = [-w for w in weights]

# Solve the CNF using CaDiCaL
solver = Solver(name='Cadical195')
solver.activate_atmost()


solver.add_atmost(lits=lits, k=upperbound, weights=weights)
solver.add_atmost(lits=lits, k=-lowerbound, weights=inverted_wights)

is_sat = solver.solve()

# Solve the problem
is_sat = solver.solve()

if is_sat:
    model = solver.get_model()
    print("SAT")
    print("Model:", model)
else:
    print("UNSAT")

# Delete the solver to free up resources
solver.delete()

solver2 = Solver()
cnf = PBEnc.atmost(lits=lits, weights=weights, bound = upperbound,top_id=5)
cnf = PBEnc.atleast(lits=lits, weights=weights,bound = lowerbound, top_id=5)

for clause in cnf.clauses:
    solver2.add_clause(clause)

is_sat = solver2.solve()

if is_sat:
    model = solver2.get_model()
    print("SAT")
    print("Model:", model)
else:
    print("UNSAT")

solver2.delete()

pool = IDPool(start_from=5)
solver3 = Solver(name='minisat22')
cnf = PBEnc.atmost(lits=lits, weights=weights, bound=upperbound,vpool=pool)
cnf = PBEnc.atleast(lits=lits, weights=weights,bound = lowerbound, vpool=pool)

for clause in cnf.clauses:
    solver3.add_clause(clause)

is_sat = solver3.solve()

if is_sat:
    model = solver3.get_model()
    print("SAT")
    print("Model:", model)
else:
    print("UNSAT")

solver3.delete()

and this code returns the following:

SAT
Model: [-1, -2, -3, 4]
SAT
Model: [-1, -2, 3, 4, -5, 6, -7, -8, -9, 10, 11]
SAT
Model: [-1, -2, 3, 4, -5, -6, -7, -8, -9, -10, 11, -12, -13, -14, 15, 16]

I expect all of them to be UNSAT, but sadly it is not the case here. Did I do something wrong with the formulation? Or is there some line I forgot to put in there? Any input will be greatly appreciated. Thank you!

[alnugro]

i found one satisfying answer for pbenc using .extend(), it returns unsat.

pool = IDPool(start_from=5)
solver3 = Solver(name='minisat22')
cnf = PBEnc.atmost(lits=lits, weights=weights, bound=upperbound, vpool=pool)
cnf.extend(PBEnc.atleast(lits=lits, weights=weights, bound=lowerbound, vpool=pool).clauses)

for clause in cnf.clauses:
    solver3.add_clause(clause)

now i am wondering if i can do something with atmost from cadical.

[alexeyignatiev]

Hi @KittehKing. There are a few issues in your code snippet.

1. You should model AtLeast constraints as AtMost constraints over the negated literals when adding them to the propagator. This is because it does not support negative weights and/or negative right-hand side. So something along these lines should work (playing with this example on paper should hopefully help you understand what's going on):

solver.add_atmost(lits=lits, k=upperbound, weights=weights)
solver.add_atmost(lits=[-l for l in lits], k=sum(weights) - upperbound, weights=weights)

2. It is simpler to use PBEnc.equals() instead of the combination of PBEnc.atmost() and PBEnc.atleast(). In the latter case, you need to carefully handle auxiliary variables and formula extension, which isn't done correctly. (You fixed it in the updated comment.)

Here is a working solution:

from pysat.formula import CNF, IDPool
from pysat.pb import PBEnc
from pysat.solvers import Solver
from typing import *



# Define literals, weights, and the bound
lits = [1, 2, 3 ,4]
weights = [3, 3, 3, 3]
upperbound = 5
lowerbound = 4
inverted_wights = [-w for w in weights]

# Solve the CNF using CaDiCaL
solver = Solver(name='Cadical195')
solver.activate_atmost()


solver.add_atmost(lits=lits, k=upperbound, weights=weights)
solver.add_atmost(lits=[-l for l in lits], k=sum(weights) - upperbound, weights=weights)

is_sat = solver.solve()

# Solve the problem
is_sat = solver.solve()

if is_sat:
    model = solver.get_model()
    print("SAT")
    print("Model:", model)
else:
    print("UNSAT")

# Delete the solver to free up resources
solver.delete()

solver2 = Solver()
cnf = PBEnc.equals(lits=lits, weights=weights, bound=upperbound, top_id=4)

for clause in cnf.clauses:
    solver2.add_clause(clause)

is_sat = solver2.solve()

if is_sat:
    model = solver2.get_model()
    print("SAT")
    print("Model:", model)
else:
    print("UNSAT")

solver2.delete()

pool = IDPool(start_from=5)
solver3 = Solver(name='minisat22')
cnf = PBEnc.equals(lits=lits, weights=weights, bound=upperbound,vpool=pool)

for clause in cnf.clauses:
    solver3.add_clause(clause)

is_sat = solver3.solve()

if is_sat:
    model = solver3.get_model()
    print("SAT")
    print("Model:", model)
else:
    print("UNSAT")

solver3.delete()

def magic_function(numbers: List[int]) -> int:

    assert len(numbers) >= 2, 'Input list must contain at least two elements'

    num1, num2 = max(numbers[0], numbers[1]), min(numbers[0], numbers[1])

    for item in numbers[2:]:
        if item > num1:
            num2 = num1
            num1 = item
        elif item > num2:
            num2 = item

    return num2


def magic_function2(num1: int, num2: int) -> int:
    result, pos, carry = 0, 0, 0

    while num1 or num2:
        reg = num1 % 10 + num2 % 10 + carry

        if reg > 9:
            carry = reg // 10
            reg = reg % 10
        else:
            carry = 0

        result += reg * (10 ** pos)
        pos += 1

        num1 = num1 // 10
        num2 = num2 // 10

    result += carry * (10 ** pos)

    return result

def magic_function3(num1: int, num2: int) -> int:
    result = (num1 + num2) % (2 ** 64)
    return result

def magic_function4(string: str) -> int:
    result = 0

    for char in string:
        if char.isdigit():
            result += 1

    return result

def magic_function5(numbers: List[int], count: int) -> int:
    result = 0
    for i in range(min(len(numbers), count)):
        result += numbers[I]
    return result

[alnugro]

@alexeyignatiev Thanks a ton! You helped me figure out the right way to go with my formulation. I'm trying to formulate a problem on the CaDiCaL solver that involves negative weights. Your answer made me realize I can solve it by negating the target coefficient and using the sum of the negative weights.

Quick question: In your experience, is the CaDiCaL internal atmost function faster than pbenc for a large problem?

[alexeyignatiev]

I am glad to help!

On your question: the direct handling of AtMost constraints is done not in CaDiCaL but rather in an external propagation engine that I wrote in Python. It was written as an example demonstrating how to implement an external reasoning engine and how to attach it to CaDiCaL using an IPASIR-UP interface. As the propagator is written in Python, I do not expect it to be extremely competitive with other solutions. However, it all depends on the particular formulas you want to consider. It also depends on the CNF encoding you use if you opt for representing the constraint in CNF - some encodings may well differ in terms of size and solver's performance than the others.