Search code examples
z3sat

3-SAT formulas as an SMT-LIB

I try to find whether there are such values of A-F that make the Boolean expression TRUE. I use online z3 solver (https://jfmc.github.io/z3-play/) It gives error

Error: (error "line 11 column 12: Wrong number of arguments (4) passed to function (declare-fun A () Bool)") sat

This is my code:

(set-logic QF_LIA)
(declare-const A Bool)
(declare-const B Bool)
(declare-const C Bool)
(declare-const D Bool)
(declare-const E Bool)
(declare-const F Bool)
(assert
(and
(A or B or C)
(D or E or F)
))
(check-sat)
(get-model)
(exit)
Solution

  • In SMTLib, functions are written in prefix-notation. So, instead of:

    (assert
(and
(A or B or C)
(D or E or F)
))

    you should use:

    (assert (and (or A B C)
             (or D E F)
        )
)

    This is similar to languages like Lisp/Scheme, where prefix-notation makes the syntax simple to parse/manipulate by programs.